LEO-II

swMATH512MaRDI QIDQ13268FDOQ13268

Author name not available (Why is that?)

Described by source

• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)

Cited In (51)

• A logical framework combining model and proof theory
• Extending Sledgehammer with SMT solvers
• 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}
• 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
• HOL Based First-Order Modal Logic Provers
• Cut-elimination for quantified conditional logic
• Title not available (Why is that?)
• Automated Inference of Finite Unsatisfiability
• Progress in the Development of Automated Theorem Proving for Higher-Order 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
• 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
• Making higher-order superposition work
• Combining and automating classical and non-classical logics in classical higher-order logics
• A deontic logic reasoning infrastructure
• 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
• 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
• Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
• Quantified multimodal logics in simple type theory
• Limited second-order functionality in a first-order setting
• Logic-independent proof search in logical frameworks (short paper)
• An abstraction-refinement framework for reasoning with large theories
• Superposition for \(\lambda\)-free higher-order logic
• 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
• \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
• Title not available (Why is that?)
• LEO-II and Satallax on the Sledgehammer test bench
• 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