Agent-based HOL reasoning. In the Leo-III project, a new agent-based deduction system for classical higher-order logic is developed. Leo-III combines its predecessor’s concept of cooperating external specialist systems with a novel agent-based proof procedure. Key goals of the system’s development involve parallelism on various levels of the proof search, adaptability for different external specialists, and native support for reasoning in expressive non-classical logics.

References in zbMATH (referenced in 16 articles , 1 standard article )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  2. Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert: Designing normative theories for ethical and legal reasoning: \textscLogiKEyframework, methodology, and tool support (2020)
  3. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  4. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2019)
  5. Bhayat, Ahmed; Reger, Giles: Restricted combinatory unification (2019)
  6. Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
  7. Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe: Superposition for (\lambda)-free higher-order logic (2018)
  8. Steen, Alexander: Extensional paramodulation for higher-order logic and its effective implementation Leo-III (2018)
  9. Steen, Alexander; Benzmüller, Christoph: The higher-order prover Leo-III (2018)
  10. Sutcliffe, Geoff: The CADE-26 automated theorem proving system competition -- CASC-26 (2017)
  11. Buchberger, Bruno; Jebelean, Tudor; Kutsia, Temur; Maletzky, Alexander; Windsteiger, Wolfgang: Theorema 2.0: computer-assisted natural-style mathematics (2016)
  12. Libal, Tomer; Miller, Dale: Functions-as-constructors higher-order unification (2016)
  13. Steen, Alexander; Benzmüller, Christoph: Sweet SIXTEEN: automation via embedding into classical higher-order logic (2016)
  14. Steen, Alexander; Wisniewski, Max; Benzmüller, Christoph: Agent-based HOL reasoning (2016)
  15. Wisniewski, Max; Steen, Alexander; Kern, Kim; Benzmüller, Christoph: Effective normalization techniques for HOL (2016)
  16. Wisniewski, Max; Steen, Alexander; Benzmüller, Christoph: \textscLeoPARD-- a generic platform for the implementation of higher-order reasoners (2015)