The higher-order prover \textsc{Leo}-II
From MaRDI portal
Publication:287283
DOI10.1007/S10817-015-9348-YzbMATH Open1356.68176DBLPjournals/jar/BenzmullerSPT15OpenAlexW1909465604WikidataQ59402111 ScholiaQ59402111MaRDI QIDQ287283FDOQ287283
Authors: Christoph Benzmüller, Nik Sultana, Frank Theiß, Lawrence C. Paulson 
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-015-9348-y
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
- An introduction to mathematical logic and type theory: To truth through proof.
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Satallax: An Automatic Higher-Order Prover
- The TPTP World -- infrastructure for automated reasoning
- Title not available (Why is that?)
- Analytic tableaux for higher-order logic with choice
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Comparing approaches to resolution based higher-order theorem proving
- TPS: A theorem-proving system for classical type theory
- Quantified multimodal logics in simple type theory
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Higher-order modal logics: automation and applications
- Multimodal and intuitionistic logics in simple type theory
- Title not available (Why is that?)
- HOL Light: An Overview
- Cut-Simulation and Impredicativity
- Cut-elimination for simple type theory with an axiom of choice
- Title not available (Why is that?)
- Title not available (Why is that?)
- Logic Programming
- Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
- Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
- Higher-order semantics and extensionality
- Encoding monomorphic and polymorphic types
- Title not available (Why is that?)
- Theorem Proving in Higher Order Logics
- Title not available (Why is that?)
- Combining and automating classical and non-classical logics in classical higher-order logics
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- Computer supported mathematics with \(\Omega\)MEGA
- On connections and higher-order logic
- Computer science -- theory and applications. Second international symposium on computer science in Russia, CSR 2007, Ekaterinburg, Russia, September 3--7, 2007. Proceedings
- Combined reasoning by automated cooperation
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
- Superposition with lambdas
- A combinator-based superposition calculus for higher-order logic
- 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
- 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
- \((\alpha, \beta)\)-ordered linear resolution of intuitionistic fuzzy propositional logic
- 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
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- AUTO2, a saturation-based heuristic prover for higher-order logic
- LEO-II and Satallax on the Sledgehammer test bench
- The higher-order prover Leo-III
- A Knuth-Bendix-like ordering for orienting combinator equations
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)
