The higher-order prover \textsc{Leo}-II
From MaRDI portal
Publication:287283
Recommendations
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- The higher-order prover Leo-III
- Extensional higher-order paramodulation in Leo-III
- LEO-II and Satallax on the Sledgehammer test bench
- AUTO2, a saturation-based heuristic prover for higher-order logic
Cites work
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 1341621 (Why is no real title available?)
- scientific article; zbMATH DE number 1765674 (Why is no real title available?)
- scientific article; zbMATH DE number 2090305 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 6780833 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- A unification algorithm for typed \(\bar\lambda\)-calculus
- An introduction to mathematical logic and type theory: To truth through proof.
- Analytic tableaux for higher-order logic with choice
- Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
- Combined reasoning by automated cooperation
- Combining and automating classical and non-classical logics in classical higher-order logics
- Comparing approaches to resolution based higher-order theorem proving
- Computer science -- theory and applications. Second international symposium on computer science in Russia, CSR 2007, Ekaterinburg, Russia, September 3--7, 2007. Proceedings
- Computer supported mathematics with MEGA
- Cut-Simulation and Impredicativity
- Cut-elimination for simple type theory with an axiom of choice
- Encoding monomorphic and polymorphic types
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- HOL Light: An Overview
- Higher-order modal logics: automation and applications
- Higher-order semantics and extensionality
- Isabelle/HOL. A proof assistant for higher-order logic
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Logic Programming
- Multimodal and intuitionistic logics in simple type theory
- On connections and higher-order logic
- Quantified multimodal logics in simple type theory
- Satallax: An Automatic Higher-Order Prover
- Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
- TPS: A theorem-proving system for classical type theory
- The TPTP World -- infrastructure for automated reasoning
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Theorem Proving in Higher Order Logics
Cited in
(29)- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Superposition with lambdas
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Cut-elimination for quantified conditional logic
- Extensional higher-order paramodulation in Leo-III
- The MET: The Art of Flexible Reasoning with Modalities
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments
- A combinator-based superposition calculus for higher-order logic
- Superposition with lambdas
- Effective normalization techniques for HOL
- Complexity of translations from resolution to sequent calculus
- Limited second-order functionality in a first-order setting
- Extensional paramodulation for higher-order logic and its effective implementation Leo-III
- \((\alpha, \beta)\)-ordered linear resolution of intuitionistic fuzzy propositional logic
- Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel's ontological argument
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- Superposition with Delayed Unification
- Extending SMT solvers to higher-order logic
- Automating free logic in HOL, with an experimental application in category theory
- Extending a high-performance prover to higher-order logic
- Agent-based HOL reasoning
- LEO-II and Satallax on the Sledgehammer test bench
- AUTO2, a saturation-based heuristic prover for higher-order logic
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- The higher-order prover Leo-III
- A Knuth-Bendix-like ordering for orienting combinator equations
Describes a project that uses
Uses Software
This page was built for publication: The higher-order prover \textsc{Leo}-II
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q287283)
