LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
From MaRDI portal
Publication:3541699
DOI10.1007/978-3-540-71070-7_14zbMath1165.68446OpenAlexW1955821421WikidataQ56020733 ScholiaQ56020733MaRDI QIDQ3541699
Christoph Benzmüller, Frank Theiß, Arnaud Fietzke, Lawrence Charles Paulson
Publication date: 27 November 2008
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_14
Related Items
MaLeS: a framework for automatic tuning of automated theorem provers, Semi-intelligible Isar proofs from machine-generated proofs, LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners, Regular Patterns in Second-Order Unification, Interacting with Modal Logics in the Coq Proof Assistant, The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0, Unnamed Item, A realizability interpretation of Church's simple theory of types, Superposition for higher-order logic, Proofs and Reconstructions, Quantified multimodal logics in simple type theory, Higher-Order Modal Logics: Automation and Applications, Automated inference of finite unsatisfiability, Analytic tableaux for higher-order logic with choice, Encoding Monomorphic and Polymorphic Types, Combining and automating classical and non-classical logics in classical higher-order logics, LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description), THF0 – The Core of the TPTP Language for Higher-Order Logic, Theorem Proving in Large Formal Mathematics as an Emerging AI Field, Analytic Tableaux for Higher-Order Logic with Choice, Progress in the Development of Automated Theorem Proving for Higher-Order Logic, Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners), Extending Sledgehammer with SMT Solvers, Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems, A Foundational View on Integration Problems, Superposition for full higher-order logic, GRUNGE: a grand unified ATP challenge, LEO-II, Logic-independent proof search in logical frameworks (short paper), Reducing higher-order theorem proving to a sequence of SAT problems, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
Cites Work
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- Mathematical induction in Otter-lambda
- TPS: A hybrid automatic-interactive system for developing proofs
- Computer supported mathematics with \(\Omega\)MEGA
- Combined reasoning by automated cooperation
- Isabelle/HOL. A proof assistant for higher-order logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- Logic Programming
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
