Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}
From MaRDI portal
Publication:3086787
zbMATH Open1227.03017MaRDI QIDQ3086787FDOQ3086787
Authors: Christoph Benzmüller, Lawrence C. Paulson 
Publication date: 30 March 2011
Recommendations
- Multimodal and intuitionistic logics in simple type theory
- Multimodal logic programming using equational and order-sorted logic
- Quantified multimodal logics in simple type theory
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Theorem provers for every normal modal logic
embedding of multimodal logics in simple type theoryfirst-order automated theorem prover \texttt{E}higher-order theorem prover \texttt{LEO-II}
Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)
Cited In (11)
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Cut-elimination for quantified conditional logic
- The MET: The Art of Flexible Reasoning with Modalities
- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- Combining and automating classical and non-classical logics in classical higher-order logics
- Quantified multimodal logics in simple type theory
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- Multimodal and intuitionistic logics in simple type theory
- Interacting with Modal Logics in the Coq Proof Assistant
Uses Software
This page was built for publication: Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3086787)
