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
• 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
• Combining Logics in Simple Type Theory
• Satallax: An Automatic Higher-Order Prover
• Computer-assisted analysis of the Anderson-Hájek ontological controversy
• The TPTP World – Infrastructure for Automated Reasoning
• Theorem Proving in Large Formal Mathematics as an Emerging AI Field
• HOL Based First-Order Modal Logic Provers
• Cut-elimination for quantified conditional logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automated Inference of Finite Unsatisfiability
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners
• 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
• Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners)
• 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
• A deontic logic reasoning infrastructure
• Reducing higher-order theorem proving to a sequence of SAT problems
• Theorem Provers For Every Normal Modal Logic
• GRUNGE: a grand unified ATP challenge
• Extending Sledgehammer with SMT Solvers
• Title not available (Why is that?)
• Quantified multimodal logics in simple type theory
• Limited second-order functionality in a first-order setting
• The QMLTP Problem Library for First-Order Modal Logics
• 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
• Effective Normalization Techniques for HOL
• Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
• Title not available (Why is that?)
• Extending SMT solvers to higher-order logic
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems
• Automating free logic in HOL, with an experimental application in category theory
• On Logic Embeddings and Gödel’s God
• Multimodal and intuitionistic logics in simple type theory
• Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
• Title not available (Why is that?)
• LEO-II and Satallax on the Sledgehammer test bench
• Detecting inconsistencies in large first-order knowledge bases
• A Foundational View on Integration Problems
• Interacting with Modal Logics in the Coq Proof Assistant
• Terminating Tableaux for the Basic Fragment of Simple Type Theory

This page was built for software: LEO-II