The higher-order prover \textsc{Leo}-II
From MaRDI portal
Publication:287283
DOI10.1007/s10817-015-9348-yzbMath1356.68176OpenAlexW1909465604WikidataQ59402111 ScholiaQ59402111MaRDI QIDQ287283
Nik Sultana, Frank Theiß, Christoph Benzmüller, Lawrence Charles 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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (20)
Cut-elimination for quantified conditional logic ⋮ Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics ⋮ Extensional higher-order paramodulation in Leo-III ⋮ The MET: The Art of Flexible Reasoning with Modalities ⋮ Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument ⋮ Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support ⋮ Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments ⋮ Computer-assisted analysis of the Anderson-Hájek ontological controversy ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ Limited second-order functionality in a first-order setting ⋮ Extracting Higher-Order Goals from the Mizar Mathematical Library ⋮ Effective Normalization Techniques for HOL ⋮ Agent-Based HOL Reasoning ⋮ Extending SMT solvers to higher-order logic ⋮ Complexity of translations from resolution to sequent calculus ⋮ \((\alpha, \beta)\)-ordered linear resolution of intuitionistic fuzzy propositional logic ⋮ A Knuth-Bendix-like ordering for orienting combinator equations ⋮ A combinator-based superposition calculus for higher-order logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Analytic tableaux for higher-order logic with choice
- 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
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Isabelle/HOL. A proof assistant for higher-order logic
- An introduction to mathematical logic and type theory: To truth through proof.
- 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}\)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Satallax: An Automatic Higher-Order Prover
- Higher-Order Modal Logics: Automation and Applications
- Multimodal and intuitionistic logics in simple type theory
- The TPTP World – Infrastructure for Automated Reasoning
- HOL Light: An Overview
- Cut-Simulation and Impredicativity
- Cut-elimination for simple type theory with an axiom of choice
- Logic Programming
- Sort It Out with Monotonicity
- Higher-order semantics and extensionality
- Encoding Monomorphic and Polymorphic Types
- Theorem Proving in Higher Order Logics
This page was built for publication: The higher-order prover \textsc{Leo}-II
