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