Combining and automating classical and non-classical logics in classical higher-order logics
DOI10.1007/S10472-011-9249-7zbMATH Open1252.03025OpenAlexW2090076725MaRDI QIDQ656826FDOQ656826
Authors: 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
Recommendations
- Embedding and automating conditional logics in classical higher-order logic
- Automated deduction in classical and non-classical logics. Selected papers
- scientific article; zbMATH DE number 4117898
- Higher-order modal logics: automation and applications
- scientific article; zbMATH DE number 2038177
- Automatic checking properties of non-classical logics
- On the Correspondence Between Modal and Classical Logic: an Automated Approach
- Automated theorem proving by resolution in non-classical logics
- scientific article; zbMATH DE number 2042611
- scientific article; zbMATH DE number 1538011
nonclassical logicsknowledge representationclassical logicsimple type theoryclassical higher-order logichigher-order automated theorem provingautomated reasoning of rational agentslogic combinationsquantified multimodal logicssemantic embeddings
Knowledge representation (68T30) Logics of knowledge and belief (including belief change) (03B42) Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27) Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Combined logics (03B62)
Cites Work
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- An introduction to mathematical logic and type theory: To truth through proof.
- The TPTP World -- infrastructure for automated reasoning
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- TPS: A hybrid automatic-interactive system for developing proofs
- Title not available (Why is that?)
- Many-dimensional modal logics: theory and applications
- Isabelle/HOL. A proof assistant for higher-order logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Analysis and synthesis of logics. How to cut and paste reasoning systems
- A formulation of the simple theory of types
- Some theorems about the sentential calculi of Lewis and Heyting
- TPS: A theorem-proving system for classical type theory
- Multimodal and intuitionistic logics in simple type theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- Higher-order semantics and extensionality
- Completeness in the theory of types
- Two-dimensional modal logic
- Natural deduction for first-order hybrid logic
- Title not available (Why is that?)
- A compact representation of proofs
- Automated reasoning in higher-order logic. Set comprehension and extensionality in Church's type theory
- Fibred semantics and the weaving of logics. Part 1: Modal and intuitionistic logics
- Why combine logics?
- General models and extensionality
- Analytic tableaux for higher-order logic with choice
- Interpolation for first order S5
- Terminating tableau systems for hybrid logic with difference and converse
- Theorem Proving via General Matings
- A Modal Deconstruction of Access Control Logics
- Multimodal logic programming
- 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}
- Modal logic programming revisited
- Logic Programming
- General models, descriptions, and choice in type theory
Cited In (8)
- Embedding and automating conditional logics in classical higher-order logic
- Cut-elimination for quantified conditional logic
- Extensional higher-order paramodulation in Leo-III
- The higher-order prover \textsc{Leo}-II
- Quantified multimodal logics in simple type theory
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- Mechanised assessment of complex natural-language arguments using expressive logic combinations
- Combining logics in simple type theory
Uses Software
This page was built for publication: Combining and automating classical and non-classical logics in classical higher-order logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q656826)
