Abstract Modal logics extend classical first-order logic with the modalities of necessity ( $$\Box $$ □ ) and possibility ( $$\Diamond $$ ◊ ). A model of a set of modal logic formulae can be represented by a Kripke structure. This paper describes a method and implementation for finding finite Kripke models for formulae in first-order modal logics. The approach relies on translating the modal logic formulae to classical logic formulae, using an SMT solver to generate a finite model of the classical logic formulae, then translating the classical model to a finite Kripke model. This process has been implemented in the new model finding system MoMo which produces TPTP-compliant Kripke model representations. An evaluation on the modal logic problems in the TPTP problem library confirms the practicality of this approach. Up to the authors’ knowledge, MoMo is the first model finder for first-order modal logics.

Abstract An approach for encoding abstract dialectical frameworks and their semantics into classical higher-order logic is presented. Important properties and semantic relationships are formally encoded and proven using the proof assistant Isabelle/HOL. This approach allows for the computer-assisted analysis of abstract dialectical frameworks using automated and interactive reasoning tools within a uniform logic environment. Exemplary applications include the formal analysis and verification of meta-theoretical properties, and the generation of interpretations and extensions under specific semantic constraints.

This paper describes a new format for representing Tarskian-style interpretations for formulae in typed first-order logic, using the TPTP TF0 language. It further describes a technique and an implemented tool for verifying models using this representation, and a tool for visualizing interpretations. The research contributes to the advancement of au- tomated reasoning technology for model finding, which has several applications, including verification.

peer reviewed

No abstract available.

peer reviewed

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 the- orem 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 for- mat 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.