Combining and automating classical and non-classical logics in classical higher-order logics
From MaRDI portal
(Redirected from Publication:656826)
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)
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
Cites work
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 1341621 (Why is no real title available?)
- scientific article; zbMATH DE number 1028832 (Why is no real title available?)
- scientific article; zbMATH DE number 1950252 (Why is no real title available?)
- scientific article; zbMATH DE number 3271460 (Why is no real title available?)
- A Modal Deconstruction of Access Control Logics
- A compact representation of proofs
- A formulation of the simple theory of types
- An introduction to mathematical logic and type theory: To truth through proof.
- Analysis and synthesis of logics. How to cut and paste reasoning systems
- Analytic tableaux for higher-order logic with choice
- Automated reasoning in higher-order logic. Set comprehension and extensionality in Church's type theory
- Completeness in the theory of types
- Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}
- Fibred semantics and the weaving of logics. Part 1: Modal and intuitionistic logics
- General models and extensionality
- General models, descriptions, and choice in type theory
- Higher-order semantics and extensionality
- Interpolation for first order S5
- Isabelle/HOL. A proof assistant for higher-order logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Logic Programming
- Many-dimensional modal logics: theory and applications
- Modal logic programming revisited
- Multimodal and intuitionistic logics in simple type theory
- Multimodal logic programming
- Natural deduction for first-order hybrid logic
- Some theorems about the sentential calculi of Lewis and Heyting
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- TPS: A hybrid automatic-interactive system for developing proofs
- TPS: A theorem-proving system for classical type theory
- Terminating tableau systems for hybrid logic with difference and converse
- The TPTP World -- infrastructure for automated reasoning
- Theorem Proving via General Matings
- Two-dimensional modal logic
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Why combine logics?
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
Describes a project that uses
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)
