LEO-II
From MaRDI portal
Cited in
(71)- A logical framework combining model and proof theory
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}
- Extending Sledgehammer with SMT solvers
- On the fine-structure of regular algebra
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Satallax: An Automatic Higher-Order Prover
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Cut-elimination for quantified conditional logic
- HOL Based First-Order Modal Logic Provers
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- 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
- Automated Inference of Finite Unsatisfiability
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Analytic tableaux for higher-order logic with choice
- A foundational view on integration problems
- Reducing higher-order theorem proving to a sequence of SAT problems
- Combining and automating classical and non-classical logics in classical higher-order logics
- A deontic logic reasoning infrastructure
- Making higher-order superposition work
- The QMLTP problem library for first-order modal logics
- Effective normalization techniques for HOL
- Reducing higher-order theorem proving to a sequence of SAT problems
- ILTP
- Nitpick
- TPS
- Paradox
- THF0
- TPTP
- ETPS
- Satallax
- SystemOnTPTP
- AgsyHOL
- SigmaKEE
- Leo-III
- Leo
- SRASS
- Robbins Conjecture
- AxiomaticCategoryTheory
- GoedelGod
- Regular_Algebras
- Zipperposition
- PLM
- GRUNGE: a grand unified ATP challenge
- Terminating tableaux for the basic fragment of simple type theory
- Theorem proving in large formal mathematics as an emerging AI field
- Quantified multimodal logics in simple type theory
- Limited second-order functionality in a first-order setting
- Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
- An abstraction-refinement framework for reasoning with large theories
- Superposition for -free higher-order logic
- Logic-independent proof search in logical frameworks (short paper)
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- Extending SMT solvers to higher-order logic
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Combining logics in simple type theory
- Automating free logic in HOL, with an experimental application in category theory
- The TPTP World -- infrastructure for automated reasoning
- Multimodal and intuitionistic logics in simple type theory
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- LEO-II and Satallax on the Sledgehammer test bench
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- scientific article; zbMATH DE number 7178360 (Why is no real title available?)
- Detecting inconsistencies in large first-order knowledge bases
- On logic embeddings and Gödel's God
- An object-logic explanation for the inconsistency in Gödel's ontological theory
- Theorem provers for every normal modal logic
- Interacting with Modal Logics in the Coq Proof Assistant
This page was built for software: LEO-II
