Implementing Different Proof Calculi for First-order Modal Logics

Modal logics extend classical logic with the modalities ”it is necessarily true that” and ”it is possibly true that” represented by the unary operators 2 and 3, respectively. First-order modal logics (FMLs) extend propositional modal logics by domains specifying sets of objects that are associated with each world, and the standard universal and existential quantifiers [7]. FMLs have many applications, e.g., in planning, natural language processing, program verification, querying knowledge bases, and modeling communication. These applications motivate the use of automated theorem proving (ATP) systems for FMLs. Whereas there are some ATP systems available for propositional modal logics, e.g., MSPASS [9] and modleanTAP [1], there were — until recently — no (correct) ATP systems that can deal with the full first-order fragment of modal logics. This abstract presents several new ATP systems for FML and sketches their calculi and working principles. The abstract also summarizes the results of a recent comparative evaluation of these new provers (see [4] for further details). The syntax of first-order modal logic adopted here is: F,G ::= P (t1, . . . , tn) | ¬F | F ∧ G | F ∨G | F ⇒ G | 2F | 3F | ∀xF | ∃xF . The symbols P are n-ary (n ≥ 0) relation constants which are applied to terms t1, . . . , tn. The ti (0 ≤ i ≤ n) are ordinary first-order terms and they may contain function symbols. The usual precedence rules for logical constants are assumed. Regarding semantics a well accepted and straightforward notion of Kripke style semantics for FML is adopted [7]. In particular, it is assumed that constants and terms are denoting and rigid, i.e. they always pick an object and this pick is the same object in all worlds. Regarding the universe of discourse constant domain, cumulative domain and varying domain semantics are considered. The following new ATP systems for FML were developed by the authors (partly as extensions of other systems); they support different combinations of modal logics and domain semantics (GQMLProver [19] has not been included since it returned incorrect results in our experiments for several formulae):