Combining and automating classical and non-classical logics in classical higher-order logics

DOI10.1007/s10472-011-9249-7zbMath1252.03025OpenAlexW2090076725MaRDI QIDQ656826

Christoph Benzmüller

Publication date: 13 January 2012

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-011-9249-7

zbMATH Keywords

knowledge representationclassical logicnonclassical logicssimple type theoryclassical higher-order logichigher-order automated theorem provingautomated reasoning of rational agentslogic combinationsquantified multimodal logicssemantic embeddings

Mathematics Subject Classification ID

Related Items (4)

Cut-elimination for quantified conditional logic ⋮ The higher-order prover \textsc{Leo}-II ⋮ Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics ⋮ Extensional higher-order paramodulation in Leo-III

Uses Software

• LEO-II
• TPS
• Isabelle/HOL
• THF0
• TPTP
• Metis_
• ETPS
• Satallax
• E Theorem Prover
• Leo

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• TPS: A hybrid automatic-interactive system for developing proofs
• Terminating tableau systems for hybrid logic with difference and converse
• A compact representation of proofs
• Why combine logics?
• Many-dimensional modal logics: theory and applications
• Isabelle/HOL. A proof assistant for higher-order logic
• Natural deduction for first-order hybrid logic
• An introduction to mathematical logic and type theory: To truth through proof.
• TPS: A theorem-proving system for classical type theory
• Analysis and synthesis of logics. How to cut and paste reasoning systems
• Multimodal logic programming
• 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
• Fibred semantics and the weaving of logics. Part 1: Modal and intuitionistic logics
• Interpolation for first order S5
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• THF0 – The Core of the TPTP Language for Higher-Order Logic
• Modal logic programming revisited
• Theorem Proving via General Matings
• Higher-order semantics and extensionality
• Logic Programming
• A Modal Deconstruction of Access Control Logics
• General models, descriptions, and choice in type theory
• General models and extensionality
• Analytic Tableaux for Higher-Order Logic with Choice
• A formulation of the simple theory of types
• Some theorems about the sentential calculi of Lewis and Heyting
• Completeness in the theory of types
• Two-dimensional modal logic

This page was built for publication: Combining and automating classical and non-classical logics in classical higher-order logics