Recommendations
- The higher-order prover \textsc{Leo}-II
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Extensional paramodulation for higher-order logic and its effective implementation Leo-III
- A verified proof checker for higher-order logic
- Higher-order quantification and proof search
- Proof-theoretic and higher-order extensions of logic programming
- scientific article; zbMATH DE number 1552534
- scientific article; zbMATH DE number 638309
Cited in
(32)- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Restricted combinatory unification
- Local reductions for the modal cube
- Improving automation for higher-order proof steps
- Superposition with lambdas
- SAT-Inspired Higher-Order Eliminations
- Solving modal logic problems by translation to higher-order logic
- Extensional higher-order paramodulation in Leo-III
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- The MET: The Art of Flexible Reasoning with Modalities
- The higher-order prover \textsc{Leo}-II
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- A combinator-based superposition calculus for higher-order logic
- Making higher-order superposition work
- Superposition with lambdas
- The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
- Superposition for higher-order logic
- scientific article; zbMATH DE number 7471678 (Why is no real title available?)
- Leo-III
- GRUNGE: a grand unified ATP challenge
- Efficient local reductions to basic modal logic
- Superposition for full higher-order logic
- The Lean 4 theorem prover and programming language
- Extensional paramodulation for higher-order logic and its effective implementation Leo-III
- Superposition with Delayed Unification
- Extending SMT solvers to higher-order logic
- The Higher-Order Prover Leo-III (Extended Version)
- Practical Proof Search for Coq by Type Inhabitation
- Translating SUMO-K to Higher-Order Set Theory
- A Polymorphic Vampire
- Extending a high-performance prover to higher-order logic
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
Describes a project that uses
Uses Software
This page was built for publication: The higher-order prover Leo-III
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1799072)
