Exploring properties of normal multimodal logics in simple type theory with \texttt{Leo-II}

MaRDI QIDQ3086787zbMATH OpenFDO

Authors Christoph Benzmüller, Lawrence C. Paulson

Publication date 30 March 2011

zbMATH Keywords

embedding of multimodal logics in simple type theoryfirst-order automated theorem prover \texttt{E}higher-order theorem prover \texttt{LEO-II}

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

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

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

Describes a project that uses

Uses Software

• E Theorem Prover
• ETPS
• TPS
• LEO-II

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)