Theorem provers for every normal modal logic. (English) Zbl 1403.68225

Gleißner, Tobias; Steen, Alexander; Benzmüller, Christoph

Eiter, Thomas (ed.) et al., LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8–12, 2017. Selected papers. Manchester: EasyChair. EPiC Series in Computing 46, 14-30 (2017).

Summary: We present a procedure for algorithmically embedding problems formulated in higher-order modal logic into classical higher-order logic. The procedure was implemented as a stand-alone tool and can be used as a preprocessor for turning TPTP THF-compliant theorem provers into provers for various modal logics. The choice of the concrete modal logic is thereby specified within the problem as a meta-logical statement. This specification format as well as the underlying semantics parameters are discussed, and the implementation and the operation of the tool are outlined.
By combining our tool with one or more THF-compliant theorem provers we accomplish the most widely applicable modal logic theorem prover available to date, i.e. no other available prover covers more variants of propositional and quantified modal logics. Despite this generality, our approach remains competitive, at least for quantified modal logics, as our experiments demonstrate.
For the entire collection see [Zbl 1398.68026].

MSC:

68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35	Mechanization of proofs and logical operations
03B45	Modal logic (including the logic of norms)

Keywords:

automated theorem proving; higher-order logic; higher-order modal logic; semantical embedding

Software:

embed_modal; Isabelle/HOL; LEO-II; MetTeL; MleanCoP; QMLTP; RuleML; Satallax