LEO-II
From MaRDI portal
Software:13268
No author found.
Related Items (51)
Cut-elimination for quantified conditional logic ⋮ MaLeS: a framework for automatic tuning of automated theorem provers ⋮ The higher-order prover \textsc{Leo}-II ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners ⋮ Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics ⋮ Satallax: An Automatic Higher-Order Prover ⋮ The QMLTP Problem Library for First-Order Modal Logics ⋮ Unnamed Item ⋮ 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 ⋮ Detecting inconsistencies in large first-order knowledge bases ⋮ A deontic logic reasoning infrastructure ⋮ Quantified multimodal logics in simple type theory ⋮ LEO-II and Satallax on the Sledgehammer test bench ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Combining and automating classical and non-classical logics in classical higher-order logics ⋮ Unnamed Item ⋮ Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas ⋮ A logical framework combining model and proof theory ⋮ Theorem Provers For Every Normal Modal Logic ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ Computer-assisted analysis of the Anderson-Hájek ontological controversy ⋮ Combining Logics in Simple Type Theory ⋮ Analytic Tableaux for Higher-Order Logic with Choice ⋮ Progress in the Development of Automated Theorem Proving for Higher-Order Logic ⋮ Automated Inference of Finite Unsatisfiability ⋮ On Logic Embeddings and Gödel’s God ⋮ Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners) ⋮ Multimodal and intuitionistic logics in simple type theory ⋮ Extending Sledgehammer with SMT Solvers ⋮ Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems ⋮ A Foundational View on Integration Problems ⋮ The TPTP World – Infrastructure for Automated Reasoning ⋮ Unnamed Item ⋮ Superposition for \(\lambda\)-free higher-order logic ⋮ An abstraction-refinement framework for reasoning with large theories ⋮ Making higher-order superposition work ⋮ 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 ⋮ Extending SMT solvers to higher-order logic ⋮ GRUNGE: a grand unified ATP challenge ⋮ Terminating Tableaux for the Basic Fragment of Simple Type Theory ⋮ Logic-independent proof search in logical frameworks (short paper) ⋮ HOL Based First-Order Modal Logic Provers ⋮ Reducing higher-order theorem proving to a sequence of SAT problems ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ On the fine-structure of regular algebra
This page was built for software: LEO-II
