Implementing Connection Calculi for First-order Modal Logics

Jens Otten

Institut für Informatik, University of Potsdam August-Bebel-Str. 89, 14482 Potsdam-Babelsberg, Germany

                         jeotten@cs.uni-potsdam.de

Abstract This paper presents an implementation of an automated theorem prover for first-order modal logic that works for the constant, cumulative, and varying domain of the modal logics D, T, S4, and S5. It is based on the connection calculus for classical logic and uses prefixes representing world paths and a prefix unification algorithm to capture the restrictions given by the Kripke semantics of the standard modal logics. This permits a modular and elegant treatment of the considered modal logics and yields an efficient implementation. Details of the calculus, the implementation and performance results on the QMLTP problem library are presented.

1 Introduction

Modal logics add the unary modal operators □ and ◇ to classical logic. They are used to represent the modalities ”it is necessarily true that” and ”it is possibly true that”, respectively. The Kripke semantics of the standard modal logics is defined by a set of worlds and a binary accessibility relation between these worlds. In each single world the classical semantics applies to the standard connectives ¬, ∧, ∨, ⇒, and the modal operators are interpreted with respect to accessible worlds. The properties of the accessibility relation specify the particular modal logic. In first-order modal logics domains of objects are associated with each world, and the standard universal and existential quantifiers are added. Firstorder modal logics have many applications, e.g. in planning, natural language processing, and program verification. Many of these application require tools for automated reasoning in order to automate the proof search. Whereas there exist a few automated theorem proving systems for some propositional modal logics, e.g. modleanTAP [1] and MSPASS [9], the availability of even basic implementations for full first-order modal logics is very limited.

Connection calculi are a well-known basis to automate formal reasoning in classical first-order logic [4, 11]. In connection calculi the proof search is guided by connections, i.e. sets of the form {P, ¬P } that contain literals with the same predicate symbol but different polarities. This yields a goaloriented and, therefore, more efficient proof search. Connections correspond to closed branches in the tableau framework [8] or axioms in the sequent calculus [7]. The matrix characterisation for classical logic can be seen as the underlying notion of connection calculi for classical logic. This characterization of logical validity can be extended to modal logic by using prefixes, which encode the additional non-permutabilities of rule applications in the modal sequent calculus [16, 17].

In this paper an implementation of a connection calculus for the first-order modal logics D, S4, S5, and T is presented. It is based on the leanCoP system for classical first-order logic extended by an algorithm for prefix unification. This paper is structured as follows. In Section 2 the use of prefixes is motivated and the basic definitions required for the matrix characterization for modal logic are introduced. Section 3 presents the algorithm for prefix unification and the connection calculus used for the proof search. Details about the implementation based on this modal connection calculus are given in Section 4. Section 5 presents performance results of the implementation on the QMLTP problem library, before Section 6 concludes with a short summary and some remarks on future work.

Implementing Connection Calculi for First-order Modal Logics  J. Otten

2 Preliminaries

The reader is assumed to be familiar with the syntax and semantics of first-order modal logic, see, e.g., [6]. In the following we consider the standard semantics with rigid term designation, i.e. terms denote the same object in every world, and terms are local, i.e. any ground term denotes an existing object in every world. In this paper the letters P, Q are used to denote predicate symbols, f denotes a function symbol, and x, y, z are used to denote (term) variables. Terms are denoted by s, t and are built from functions, constants, and variables. Atomic formulae, denoted by A, are built from predicate symbols and terms. The connectives ¬, ∧, ∨, ⇒ denote negation, conjunction, disjunction and implication, respectively. A (first-order modal) formula, denoted by F, G, H, consists of atomic formulae, the connectives, the modal operators □ and ◇, and the existential and universal quantifiers ∀x and ∃x. A literal, denoted by L, has the form A or ¬A. The complement \overline{L} of a literal L is A if L is of the form ¬A, and ¬A otherwise.

2.1 Using Prefixes

In order to adapt the matrix characterization of classical validity to modal logic, the notion of prefixes and a modal substitution are introduced.

While the standard connectives and quantifiers are interpreted as in classical logic, the semantics of the modal operators □ and ◇ is defined with respect to a set of worlds. Then, □F or ◇F are true in a world w, if F is true in all worlds accessible from w or some world accessible from w, respectively. The properties of the accessibility relation determine the particular modal logic. In the following the modal logics D, T, S4, and S5 are considered. Their accessibility relation is serial (D)^{1}, reflexive (T), reflexive and transitive (S4), or an equivalence relation (S5), respectively.

The modal sequent calculus extends the classical sequent calculus by the modal rules □-left, □-right, ◇-left and ◇-right, which are used to introduce the modal operators □ and ◇ into the antecedent (left side) or the succedent (right side) of the sequent, respectively.

Definition 1 (Modal sequent calculus). The sequent calculus for the modal logics D, T, and S4 consists of the axiom and rules of the classical sequent calculus and the four additional inference rules shown in Figure 1 [17].^{2} It is Γ_{□} := {□G | □G ∈ Γ}, Δ_{◇} := {◇G | ◇G ∈ Δ}, Γ_{(□)} := {G | □G ∈ Γ}, and Δ_{(◇)} := {G |◇G ∈ Δ}.

{Γ^{+}, F ⊢ Δ^{+} \atop Γ, □F ⊢ Δ} □-left

{Γ^{+} ⊢ F, Δ^{+} \atop Γ ⊢ ◇F, Δ} ◇-right

{Γ^{∗} ⊢ F, Δ^{∗} \atop Γ ⊢ □F, Δ} □-right

{Γ^{∗}, F ⊢ Δ^{∗} \atop Γ, ◇F ⊢ Δ} ◇-left

logic  Γ^{+} Δ^{+} Γ^{∗}  Δ^{∗}
D  Γ_{(□)} Δ_{(◇)} Γ_{(□)} Δ_{(◇)}
T  Γ  Δ  Γ_{(□)} Δ_{(◇)}
S4  Γ  Δ  Γ_{□}  Δ_{◇}

Figure 1: The four additional rules of the modal sequent calculus

For the proof search the modal rules are applied upwards, i.e., in an analytic way. In that case formulae in the sets Γ^{∗}, Δ^{∗}, Γ^{+} and Δ^{+} are deleted from the premise. To avoid deleting formulae that are required for a proof the application order of the modal rules need to be controlled.

1 A relation R ⊆ W × W is serial iff for all w_{1} ∈ W there is some w_{2} ∈ W with (w_{1}, w_{2}) ∈ R.

2 The modal sequent calculus captures the cumulative domain condition (see Section 2.2). There are no similar cut-free sequent calculi (that have the subformula property) for the logics with constant or varying domain or for the modal logic S5.

Example 1 (Application of modal rules). Let F_{1} be the formula □P ⇒ □□P. The left side of Figure 2 shows a sequent derivation of F_{1} in the modal sequent calculus for S4. When the rule □-left is applied first (in an analytic way), the following application of the rule □-right deletes the formula P from the antecedent and the derivation cannot be turned into a proof. In the derivation of F_{1} in the middle of Figure 2 the two rules □-right are applied before rule □-left, and the resulting derivation is a proof.

{⊢ P \atop ⊢ □P} □-right P ⊢ □□P □-right

□P ⊢ □□P □-left

⊢ □P ⇒ □□P

{w_{2} P ⊢ P \atop w_{2} □P ⊢ P} □-left w_{1} □P ⊢ □P □-right

w_{0} □P ⊢ □□P □-right

w_{0} ⊢ □P ⇒ □□P

{P : a_{0}A_{1} ⊢ P : a_{0}a_{1}a_{2} \atop □P : a_{0} ⊢ P : a_{0}a_{1}a_{2}} □-left □P : a_{0} ⊢ □P : a_{0}a_{1} □-right

□P : a_{0} ⊢ □□P : a_{0} □-right

⊢ □P ⇒ □□P : a_{0}

Figure 2: Sequent derivations of □P ⇒ □□P for the modal logic S4

Semantically, every application of the rule □-right introduces a new world accessible from the previous one. Starting with w_{0} the derivation in the middle of Figure 2 is labelled with the worlds in which the sequent is forced. □P is forced in w_{0}, w_{1} is accessible from w_{0} and w_{2} is accessible from w_{1}. As the accessibility relation of S4 is transitive, w_{2} is also accessible from w_{0}. Hence, the formula □P on the left side of the sequent is preserved. For the modal logic D, whose accessibility relation is neither reflexive nor transitive, the applications of the rules □-left(or □-right) and □-right would yield the upper sequent ⊢ P. The □P on the left side of the sequent does not survive more than one world transition as the accessibility relation for the modal logic D is not transitive. In the following the notion of prefixes is used in order to name sequences of accessible worlds.

Definition 2 (Prefix). A prefix, denoted by p or q, is a string (sequence of characters) over an alphabet ν ∪ Π, in which ν is a set of prefix variables and Π is a set of prefix constants.

To distinguish between elements of ν and elements of Π within a prefix, elements of ν are written in capitals, denoted by V or V_{i}, whereas small letters, denoted by a or a_{i}, are used to represent elements of Π. u, w denote strings, ε denotes the empty string, u∘w denotes the concatenation of u and w. u ⪯ w holds if, and only if, u is an initial substring of w or u = w.

Example 2 (Prefixes for worlds). In the right derivation of F_{1} in Figure 2 each formula is labelled with a prefix encoding the world in which the formula is forced. Starting with a_{0} each application of a modal rule extends the prefix by one character. In the logic S4, A_{1} could denote any world accessible from a_{0}. To ensure that the propositions P on both sides of the sequent are forced in the same world, their two prefixes a_{0}A_{1} and a_{0}a_{1}a_{2} need to refer to the same world. This is achieved by assigning the string a_{1}a_{2} to A_{1}. In the logic D, A_{1} can only denote a world directly accessible from a_{0}. Hence, only the string a_{1} can be assigned to A_{1} and the two prefixes a_{0}A_{1} and a_{0}a_{1}a_{2} cannot denote the same world.

Semantically, a prefix denotes a specific world in a model [5, 17]. Prefixes of literals that form an axiom in the sequent calculus need to denote the same world. Proof-theoretically, a prefix of a formula F captures the modal context of F and specifies the sequence of modal rules that have to be applied (analytically) in order to obtain F in the sequent. Prefix variables and constants represent applications of the modal rules □-left/◇-right and □-right/◇-left, respectively. When a modal rule that corresponds to an element in Π (and ν for the modal logic D) is applied, only formulae whose prefix ends with an element of ν are preserved in the premise of the sequent. Hence, the application of the modal rules represented by elements of ν and Π need to be controlled. In order to preserve two atomic formulae that form an axiom in the sequent calculus their prefixes need to be made identical. This is done by a modal substitution that maps elements of ν to strings over ν ∪ Π.

Definition 3 (Modal substitution). A modal substitution is a mapping σ_{M} : ν → (ν ∪ Π)^{∗} that assigns a string over the alphabet ν ∪ Π to every element in ν. For the modal logics D and T the accessibility condition |σ_{M}(V)| = 1 or |σ_{M}(V)| ≤ 1 has to hold for all V ∈ν, respectively. σ_{M}(p) denotes the string p in which each prefix variable V is replaced by its image σ_{M}(V).

Substitutions σ_{M} are assumed to be idempotent, i.e. σ_{M} ∘ σ_{M} = σ_{M} holds. They are represented by the set {V \p | σ_{M}(V) = p and p ≠ V }. The accessibility condition encodes the characteristics of the different modal rules for each logic. For the modal logic D a formula that corresponds to a prefix variable will only survive one application of the modal rules. Hence, only strings of length one can be assigned to prefix variables. For the modal logic T a formula that corresponds to a prefix variable will only survive one application of the modal rules □-right or ◇-left, but any number of applications of the rules □-leftand ◇-right. Therefore, strings of length one or ε can be assigned to prefix variables. For the modal logic S4 a formula that corresponds to a prefix variable will survive any number of applications of modal rules. Hence, there is no restriction on strings that can be assigned to prefix variables.

Example 3 (Modal substitution). Consider the prefixes a_{0}A_{1} and a_{0}a_{1}a_{2} of the two literals occurring in the upper sequent of the right derivation in Figure 2. σ_{M}_{1} = {A_{1}\a_{1}a_{2}} is a modal substitution for the logic S4 (but not for D or T) with σ_{M}_{1}(a_{0}A_{1}) = a_{0}a_{1}a_{2} = σ_{M}_{1}(a_{0}a_{1}a_{2}).

2.2 Matrix Characterization

The matrix characterization of validity for modal logic can be seen as the basis of the connection calculus presented in Section 3.2. As the core implementation of the connection calculus (introduced in Section 4.2) uses a clausal form, the original (non-clausal) matrix characterization [17] is slightly modified. Matrices use a clausal form and the definitions of prefixes and paths are simplified by using the formal definition of a prefixed matrix and an extended Skolemization technique.

A polarity pol ∈ {0, 1} is used to represent negation in a matrix, i.e. literals of the form A and ¬A are represented by A^{0} and A^{1}, respectively. A prefixed formula F^{pol}:p is a formula F marked with a polarity pol and a prefix p. A (prefixed) clause, denoted by C, is a set {L_{1} : p_{1}, …, L_{n}: p_{n}} with literals L_{i} and prefixes p_{i}. F [x\t] denotes the formula F in which all free occurrences of x are replaced by t.

Definition 4 (Prefixed matrix). The prefixed matrix M(F^{pol}:p) of a prefixed formula F^{pol}:p is a set of prefixed clauses. It is defined inductively according to Table 1. The following abbreviation is used: M_{G} ∪_{β} M_{H} := {C_{G} ∪ C_{H} | C_{G} ∈ M_{G}, C_{H} ∈ M_{H}}. x^{∗} is a new term variable, t^{∗} is the Skolem term f^{∗}(x_{1}, …, x_{n}) in which f^{∗} is a new function symbol and x_{1}, …, x_{n} are all free term and prefix variables in ∀xG or ∃xG. V^{∗} is a new prefix variable, a^{∗} is a prefix constant of the form f^{∗}(x_{1}, …, x_{n}) in which f^{∗} is a new function symbol and x_{1}, …, x_{n} are all free term and prefix variables in □G or ◇G. The prefix of x^{∗} and t^{∗}, denoted pre(x^{∗}) and pre(t^{∗}), is p. The (prefixed) matrix M(F) of a (first-order modal) formula F is the prefixed matrix M(F^{0} : ε).

In the graphical representation of a matrix, its clauses are arranged horizontally, while the literals of each clause are arranged vertically. In order to simplify the implementation Skolemization is not only used for Eigenvariables but also for prefix constants. A similar approach is already used for intuitionistic logic [10]. Thus, the irreflexivity test of the reduction ordering [17] is realized by the occur check of the term and prefix unification procedures. The same Skolem function symbol is used for instances of the same subformula, a technique that is similar to the liberalized δ^{+}-rule in classical tableau calculi [8].

Example 4 (Prefixed matrix). Let F_{1} be the modal formula (◇∃xP x∧□∀y(◇P y ⇒ Qy)) ⇒ ◇∃zQz. The prefixed matrix of F_{1} is M_{1}:=M(F_{1}) = {{P^{1}d: a_{1}}, {P^{0}y: V_{1}V_{2}, Q^{1}y: V_{1}}, {Q^{0}z: V_{3}}}. x is an Eigenvariable, y, z are free term variables, a_{1} ∈ Π is a prefix constant, V_{1}, V_{2}, V_{3} ∈ ν are prefix variables. d, a_{1} are Skolem functions/constants. The graphical representation of M_{1} is shown in Figure 3.

Table 1: Matrix M(F^{pol}: p) of a first-order modal formula F^{pol}: p

type F^{pol} : p  M(F^{pol} : p)
atomic A^{0} : p  {{A^{0} : p}}
A^{1} : p  {{A^{1} : p}}
α (¬G)^{0} : p M(G^{1} : p)
(¬G)^{1} : p  M(G^{0} : p)
(G ∧ H)^{1} : p M(G^{1}:p) ∪ M(H^{1}:p)
(G ∨ H)^{0} : p M(G^{0}:p) ∪ M(H^{0}:p)
(G ⇒ H)^{0}: p M(G^{1}:p) ∪ M(H^{0}:p)
ν (□G)^{1} : p M(G^{1} : p ∘ V^{∗})
(◇G)^{0} : p  M(G^{0} : p ∘ V^{∗})

type F^{pol} : p  M(F^{pol} : p)_{β  (G ∧ H)^{0} : p M(G^{0}:p) ∪_{β} M(H^{0}:p)}_{(G ∨ H)^{1} : p M(G^{1}:p) ∪_{β} M(H^{1}:p)}_{(G ⇒ H)^{1}: p M(G^{0}:p) ∪_{β} M(H^{1}:p)}_{γ  (∀xG)^{1} : p M(G[x\x^{∗}]^{1} : p)}_{(∃xG)^{0} : p M(G[x\x^{∗}]^{0} : p)}_{δ  (∀xG)^{0} : p M(G[x\t^{∗}]^{0} : p)}_{(∃xG)^{1} : p M(G[x\t^{∗}]^{1} : p)}_{π  (□G)^{0} : p  M(G^{0} : p ∘ a^{∗})}_{(◇G)^{1} : p  M(G^{1} : p ∘ a^{∗})}

Connections and paths are the basic concepts of the matrix characterization. They correspond to axioms and atomic sequents (that cannot be reduced anymore) in the sequent calculus, respectively.

Definition 5 (Connection, path, term substitution). The set {P^{1}(s_{1}, …, s_{n}) : p_{1}, P^{0}(t_{1}, …, t_{n}) : p_{2}} is a connection. It consists of a pair of literals with the same predicate symbol but different polarities. A path pt through a matrix M = {C_{1}, …, C_{n}} is a set of literals that contains one literal from each clause, i.e. pt := ∪_{i=1}^{n}{L_{i}} with L_{i} ∈ C_{i}. A term substitution σ_{Q} is a mapping from the set of term variables to the set of terms. In σ_{Q}(L) all term variables x in L are substituted by their image σ_{Q}(x).

Example 5 (Connection, path, term substitution). Consider the matrix M_{1} of Example 4 and its graphical representation in Figure 3. Then, {P^{1}d: a_{1}, P^{0}y: V_{1}V_{2}} and {Q^{1}y: V_{1}, Q^{0}z: V_{3}} are connections. {P^{1}d: a_{1}, P^{0}y: V_{1}V_{2}, Q^{0}z: V_{3}} and {P^{1}d: a_{1}, Q^{1}y: V_{1}, Q^{0}z: V_{3}} are (the only) paths through M_{1}. σ_{Q}_{1} with σ_{Q}_{1}(y) = d and σ_{Q}_{1}(z) = d is a term substitution.

To ensure that a connection represents an axiom in the sequent calculus, the atomic formulae in the connection have to unify under a term substitution. Furthermore, their prefixes have to unify under a prefix substitution. This ensures that these formulae are not deleted by applications of modal rules.

Definition 6 (Admissible substitution, complementarity). Let L ∈ {D, T, S4, S5} be a modal logic, D ∈ {constant, cumulative, varying} be a domain, σ_{M} be a modal substitution for L and σ_{Q} be a term substitution. The (combined) substitution σ := (σ_{Q}, σ_{M}) is admissible iff the domain condition in Table 2 holds for all term variables x and (I) for cumulative domain for all Skolem terms t in σ_{Q}(x), or (II) for varying domain for all term variables/Skolem terms s in σ_{Q}(x). A connection {L_{1} : p_{1}, L_{2} : p_{2}} is σ-complementary for a substitution σ = (σ_{Q}, σ_{M}) iff σ_{Q}(σ_{M}(L_{1} : p_{1})) = σ_{Q}(σ_{M}(\overline{L_{2}} : p_{2})). For the modal logic S5 only the last character of all prefixes, i.e. of pre(x), pre(s), p_{1} and p_{2}, is considered.

Table 2: Domain condition for the substitution σ = (σ_{Q}, σ_{M})

logic L
domain D  D, T, S4  S5
constant  –  –
cumulative σ_{M}(pre(t)) ⪯ σ_{M}(pre(x))  –
varying σ_{M}(pre(s)) = σ_{M}(pre(x)) σ_{M}(pre(s)) = σ_{M}(pre(x))

[ ^{[ P^{1}d : a_{1} ]} [ \begin{matrix}P^{0}y : V_{1}V_{2} \\ Q^{1}y : V_{1} \end{matrix} ] _{[ Q^{0}z : V_{3} ]} ]

Figure 3: Graphical representation of the matrix M_{1}

The constant domain variants place no restriction on the modal substitution as the same objects exist in every world. For the cumulative domain variants any Skolem term t introduced by a quantifier rule in a world w_{1} exists in a world w_{2} that is directly or indirectly accessible from w_{1}. Hence, if t occurs in σ_{Q}(x) then the prefix w_{1} = σ_{M}(pre(t)) has to be an initial string of w_{2} = σ_{M}(pre(x)).^{3} In case of the varying domain variants objects may only exists in the world in which they are introduced. Hence, if s occurs in σ_{Q}(x) then the prefixes w_{1} = σ_{M}(pre(s)) and w_{2} = σ_{M}(pre(x)) need to be identical.

Example 6 (Admissible substitution, complementarity). Consider the matrix M_{1} of Example 4 with σ_{Q}_{1}(y) = σ_{Q}_{1}(z) = d, σ_{M}_{1}(V_{1}) = σ_{M}_{1}(V_{3}) = a_{1}, and σ_{M}_{1}(V_{2}) = ε (for T, S4) or σ_{M}_{1}(V_{2}) = a_{1} (for S5). Then, σ_{M}_{1} is a modal substitution for the modal logics T, S4, and S5, but not for D. The substitution σ_{1} = (σ_{Q}_{1}, σ_{M}_{1}) is admissible for the constant, cumulative, and varying domain as pre(y) = pre(z) = pre(d) = a_{1}. The connections {P^{1}d: a_{1}, P^{0}y: V_{1}V_{2}} and {Q^{1}y: V_{1}, Q^{0}z: V_{3}} are σ_{1}-complementary.

The notion of multiplicity is used to encode the number of clause copies used in a proof. It is a function μ: M → IN that assigns a natural number to each clause in M specifying how many copies of this clause are considered in a proof. In the copy of a clause C every (term and prefix) variable in C is replaced by a unique new variable. M^{μ} denotes the matrix that includes these clause copies. Clause copies correspond to applications of the contraction rule in the sequent calculus.

Theorem 1 (Matrix characterisation for modal logic). Let L ∈ {D,T,S4,S5} be a modal logic and D ∈ {constant,cumulative,varying} be a domain. A formula F is valid in the logic L with domain D iff there is a multiplicity μ, an admissible substitution σ = (σ_{Q}, σ_{M}) for L/D, and a set of σ-complementary connections such that every path through M(F)^{μ} contains a connection from this set.

Example 7 (Matrix characterisation for modal logic). Consider the formula F_{1} of Example 4 and the graphical representation of its matrix M_{1} in Figure 3. Let μ ≡ 1, σ_{Q}_{1}(y) = σ_{Q}_{1}(z) = d, σ_{M}_{1}(V_{1}) = σ_{M}_{1}(V_{3}) = a_{1}, and σ_{M}_{1}(V_{2}) = ε (for T, S4) or σ_{M}_{1}(V_{2}) = a_{1} (for S5). σ_{1} = (σ_{Q}_{1}, σ_{M}_{1}) is admissible for all domains, and every path through M_{1}^{μ} contains a σ_{1}-complementary connection. Hence, F_{1} is valid in the modal logics T, S4, and S5 with constant, cumulative, and varying domain.

3 Proof Search

An effective way to carry out proof search that is based on the matrix characterization is done with a connection-driven search strategy. For this purpose the connection calculus is extended by additional prefixes. Furthermore, a prefix unification algorithm is required in order to calculate the modal substitution by unifying the prefixes of the literals in each connection.

3.1 Prefix Unification

Formally, prefix unification is the problem to find a modal substitution or unifier σ_{M} for a set of prefix equations E = {p_{1} = q_{1}, …, p_{n} = q_{n}} such that σ_{M}(p_{i}) = σ_{M}(q_{i}) for all 1 ≤ i ≤ n. A set of unifiers Σ is a set of most general unifiers for E if, and only if, every unifier τ is an instance of some σ ∈ Σ (completeness) and no unifier σ ∈ Σ is an instance of another unifier τ ∈ Σ (minimality).

3This condition — as well as the (non-applicable) accessibility condition for S5 — are slightly corrected conditions of [17].

As prefixes are strings, general algorithms for string unification^{4} could be used for unifying prefixes. But for general string unification the number of most general unifiers might not be finite. A more efficient unification takes the prefix property of all prefixes p_{1}, p_{2}, … into account: for all prefixes p_{i} = u_{1}Xw_{1} and p_{j} = u_{2}Xw_{2} with X ∈ ν ∪ Π the property u_{1} = u_{2} holds. The prefix property reflects the fact that the order in which modal rules are applied corresponds to a (formula) tree structure.

Depending on the modal logic the accessibility condition (see Definition 3) has to be respected when calculating the modal substitution σ_{M}, i.e. for all V ∈ ν: |σ_{M}(V)| = 1 for the modal logic D, |σ_{M}(V)| ≤ 1 for the modal logic T and no restriction for the modal logics S4 and S5. The prefix unification for D is a simple pattern matching, i.e. the standard term unification can be used. For S4 the prefix unification for intuitionistic logic can be used; see [10] for details. For S5 only the last character of each prefix (or ε if the prefix is ε) has to be unified. The prefix unification for T is specified by a set of rewriting rules. Given a prefix equation E = {p = q} it calculates a set of most general unifiers for E. For an equation of the form V_{1}u = V_{2}w the substitution {V_{1}\ε, V_{2}\ε} would not be minimal (but an instance of {V_{1}\V_{2}}). To prevent the calculation of such substitutions, the right side of each equation is split by a bar. Then, V_{2} is moved to the left side of the bar, i.e., u = V_{2}|w, when ε is assigned to V_{1}.

Definition 7 (Prefix unification). The prefix unification of two prefixes p and q for the modal logic T is done by applying the rewriting rules in Table 4; it is V ∈ν, a ∈ Π, X ∈ν ∪ Π, u, w ∈ (ν ∪ Π)^{∗}. The application of a rewriting rule replaces a tuple (E, σ_{M}) by a tuple (E′, σ_{M}′). E and E′ are prefix equations, σ_{M} and σ_{M}′ are modal substitutions. The unification starts with the tuple ({p = ε|q}, {}) and terminates when the tuple ({}, σ_{M}) is derived. In this case σ_{M} represents a most general unifier. Rules can be applied non-deterministically as there might be more than one most general unifier.

R1. {ε = ε|ε}, σ_{M}  → {}, σ_{M}
R2. {ε = ε|Xw}, σ_{M}  → {Xw = ε|ε}, σ_{M}
R3. {V u = ε|ε}, σ_{M}  → {u = ε|ε}, σ_{M} ∪ {V \ε}
R4. {Xu = ε|Xw}, σ_{M} → {u = ε|w}, σ_{M}
R5. {V u = ε|Xw}, σ_{M} → {V u = X|w}, σ_{M}  (X ≠ V)
R6. {au = ε|V w}, σ_{M} → {V w = a|u}, σ_{M}
R7. {V_{1}u = ε|V_{2}w}, σ_{M} → {w = V_{1}|u}, σ_{M} ∪ {V_{2}\ε}  (V_{1} ≠ V_{2})
R8. {V u = X|w}, σ_{M} → {u = X|w}, σ_{M} ∪ {V \ε}
R9. {V u = X|w}, σ_{M} → {u = ε|w}, σ_{M} ∪ {V \X}
R10. {au = V |w}, σ_{M}  → {u = ε|w}, σ_{M} ∪ {V \a}

Figure 4: Prefix unification for the modal logic T

To solve a set of prefix equations E = {p_{1} = p_{1}, …, q_{n} = t_{q}} the equations in E are solved one after the other. The modal substitution σ_{M} calculated for the first equation is applied to E and the next equation in E is considered and so on. Different substitutions σ_{M} are calculated on backtracking.

Example 8 (Prefix unification). Consider the connection {P^{1}d: a_{1}, P^{0}y: V_{1}V_{2}} from Example 5 and 6. The most general unifiers for its two prefixes a_{1} and V_{1}V_{2} are calculated as follows: {a_{1} = ε|V_{1}V_{2}}, {}

⟶^{R6} {V_{1}V_{2} = a_{1}|ε}, {}⟶^{R8} {V_{2} = a_{1}|ε}, {V_{1}\ε} ⟶^{R9} {ε = ε|ε}, {V_{1}\ε, V_{2}\a_{1}} ⟶^{R1} {}, {V_{1}\ε, V_{2}\a_{1}}

and {a_{1} = ε|V_{1}V_{2}}, {} ⟶^{R6} {V_{1}V_{2} = a_{1}|ε}, {} ⟶^{R9} {V_{2} = ε|ε}, {V_{1}\a_{1}} ⟶^{R3} {ε = ε|ε}, {V_{1}\a_{1}, V_{2}\ε}

⟶^{R1} {}, {V_{1}\a_{1}, V_{2}\ε}. Hence, the two most general unifiers are {V_{1}\ε, V_{2}\a_{1}} and {V_{1}\a_{1}, V_{2}\ε}.

4This is also called the monoid problem; it is the equation theory in which there is a neutral element ε and the associativity of the string concatenation operator ∘ holds.

3.2 The Connection Calculus

The matrix characterization of Theorem 1 can serve as the basis for a proof calculus. Checking that all paths contain a σ-complementary connection can be done by, e.g., sequent or tableau calculi. The connection calculus uses a connection-driven search strategy in order to determine an appropriate set of connections. It is already successfully used for automated theorem proving in classical and intuitionistic logic [11, 12]. Proof search in the connection calculus starts by selecting a start clause. Afterwards, connections are successively identified in order to make sure that all paths through the matrix contain a σ-complementary connection for some combined substitution σ = (σ_{Q}, σ_{M}). This process is guided by an active path, a subset of a path through the matrix. The multiplicity μ is increased dynamically during the path checking process. The connection calculus is adapted to modal logic by simply adding prefixes to all literals and using the prefix unification algorithm presented in Section 3.1.

Definition 8 (Modal connection calculus). The axiom and the rules of the modal connection calculus are given in Figure 5. The words of the calculus are tuples of the form “C, M, P ath”, where M is a (prefixed) matrix, C and P ath are sets of (prefixed) literals or ε. C is called the subgoal clause and P ath is called the active path. C_{1} and C_{2} are clauses, σ = (σ_{Q}, σ_{M}) is an admissible substitution, {L_{1} : p_{1}, L_{2} : p_{2}} is a σ-complementary connection. The substitutions σ_{Q} and σ_{M} are global (or rigid), i.e. they are applied to the whole derivation.

Axiom (A) \overline{\{\}, M, P ath}

Start (S) \frac{C_{2}, M, \{\}}{ε, M, ε} and C_{2} is copy of C_{1}∈M

Reduction (R) \frac{C, M, P ath∪\{L_{2}: p_{2}\}}{C∪\{L_{1}: p_{1}\}, M, P ath∪\{L_{2}: p_{2}\}} and \{L_{1}: p_{1}, L_{2}: p_{2}\} is σ-complementary

Extension (E) \frac{C_{2}\\{L_{2}: p_{2}\}, M, P ath∪\{L_{1}: p_{1}\} C, M, P ath}{C∪\{L_{1}: p_{1}\}, M, P ath} and C_{2} is a copy of C_{1}∈M, L_{2}:p_{2} ∈C_{2}, {L_{1}: p_{1}, L_{2}: p_{2}}

is σ-complementary

Figure 5: The connection calculus for modal logic

A derivation for C, M, P ath with the admissible substitution σ = (σ_{Q}, σ_{M}) for the logic L and the domain D in which all leaves are axioms is called a modal connection proof for C, M, P ath. A modal connection proof for the matrix M is a modal connection proof for ε, M, ε.

Theorem 2 (Correctness and completeness). Let L ∈ {D, T, S4, S5} be a modal logic and D ∈ {constant, cumulative, varying} be a domain. A modal first-order formula F is valid in the modal logic L with domain D iff there is a modal connection proof for M(F) for the logic/domain L/D.

The proof of Theorem 2 is based on the the matrix characterization for modal logic (see Theorem 1) and the correctness and completeness of the connection calculus [4]. Proof search in the clausal connection calculus is carried out by applying the rules of the calculus in an analytic way, i.e. from bottom to top. During the proof search backtracking might be required, i.e. alternative rules need to be considered if the chosen rule (instance) does not lead to a proof. Alternative applications of rules occur whenever more than one rule or more than one instance of a rule can be applied, i.e. when choosing the clause C_{1} in the start and extension rule or the literal L_{2} : p_{2} in the reduction and extension rule. No backtracking is required when choosing the literal L_{1} : p_{1} in the reduction or extension rule as all literals in C are considered in subsequent proof steps anyway. The term substitution σ_{Q} and the modal substitution σ_{M} are calculated by algorithms for term unification and prefix unification (see Section 3.1), respectively, whenever a reduction or extension rule is applied.

Example 9 (Modal connection calculus). Consider the formula F_{1} and its matrix M_{1} = {{P^{1}d: a_{1}}, {P^{0}y: V_{1}V_{2}, Q^{1}y: V_{1}}, {Q^{0}z: V_{3}}} of Example 4. A derivation for M_{1} in the modal connection calculus with σ_{Q}(z′) = σ_{Q}(z′) = d, σ_{M}(V′_{1}) = σ_{M}(V′_{3}) = a_{1} and σ_{M}(V′_{2}) = ε (for T, S4) or σ_{M}(V′_{2}) = a_{1} (for S5) is shown in Figure 6. y′, z′ and V′_{1}, V′_{2}, V′_{3} are new term and prefix variables. The two extension steps use the connections {P^{1}d: a_{1}, P^{0}y′: V′_{1}V′_{2}} and {Q^{1}y′: V′_{1}, Q^{0}z′: V′_{3}}. As all leaves are axioms and the substitution σ_{1} = (σ_{Q}, σ_{M}) is admissible the derivation is also a proof for M_{1}. Hence, the

\begin{matrix}\begin{matrix}\{\}, M_{1}, \{P^{1}d: a_{1}, Q^{1}y′: V′_{1}\} A & \{\}, M_{1}, \{P^{1}d: a_{1}\} A \\ \{Q^{1}y′: V′_{1}\}, \{\{P^{1}d: a_{1}\}, \{P^{0}y: V_{1}V_{2}, Q^{1}y: V_{1}\}, \{Q^{0}z: V_{3}\}\}, \{P^{1}d: a_{1}\} \end{matrix} E & \{\}, M_{1}, \{\} A \\ \{P^{1}d: a_{1}\}, \{\{P^{1}d: a_{1}\}, \{P^{0}y: V_{1}V_{2}, Q^{1}y: V_{1}\}, \{Q^{0}z: V_{3}\}\}, \{\} \end{matrix} ; E ; ε, \{\{P^{1}d: a_{1}\}, \{P^{0}y: V_{1}V_{2}, Q^{1}y: V_{1}\}, \{Q^{0}z: V_{3}\}\}, ε ; S

Figure 6: A proof for M_{1} in the modal connection calculus

formula F_{1} is valid in the modal logics T, S4, and S5 (with constant, cumulative, and varying domain). The proof of F_{1} using the graphical matrix representation is depicted in Figure 7. The literals of each connection are connected with a line. The literals of the active path are boxed. In the first step the first clause {P^{1}d: a_{1}} is selected as start clause. The second step is an extension step to the first literal of the second clause. The second step is an extension step to the third clause. Variables in clauses that are used in a proof step are renamed.

[ ^{[ P^{1}d : a_{1} ]} [ P^{0}y′ : V′_{1}V′_{2} ; Q^{1}y′ : V′_{1} ] _{[ Q^{0}z′ : V′_{3} ]} ]
1. 2.  3.

Figure 7: The modal connection proof for M_{1} using the graphical matrix representation

Additional techniques to prune the search space in the connection calculus are regularity, lemmata, restricted backtracking, and the use of a definition clausal form translation; see [12] for details. All these techniques can be integrated into the modal connection calculus as well.

4 An Implementation

The connection calculus for modal logic presented in Section 3.2was implemented in Prolog. The main components are the connection-driven proof search procedure and the prefix unification algorithm. The complete source code can be obtained at http://www.leancop.de/mleancop/ .

4.1 Prefix Unification

In the Prolog implementation strings are represented by Prolog lists, e.g. the prefix a_{0}a_{1}V_{2} is represented by the list [a0,a1,V2]. Prefix variables are Prolog variables, i.e. they start with a capital, prefix constants are Prolog atoms, i.e. they start with a small letter.

The source code of the prefix unification for the modal logic T is shown in line R1 to R10 of Figure 8. Each Prolog clause corresponds exactly to one of the rewrite rules defined in Figure 4. The predicate tuni_t(S,[],T) succeeds if the two prefixes S and T can be unified with respect to the accessibility condition for the modal logic T given in Definition 3. In this case the prefix variables are instantiated with a most general unifier for S and T. Alternative unifiers are calculated via backtracking. According to the accessibility condition for the modal logic T, prefix variables may only be instantiated with the empty string or a single prefix constant or variable. As the Skolemization technique is applied to prefix constants as well, a term unification with the Prolog predicate unify_with_occurs_check is required (line R4, R9 and R10) whenever a prefix constant needs to be unified with another prefix constant or variable.

(a) (b) (c) (d) (e) (f) (g) (h)

(R1) (R2) (R3) (R4)

(R5) (R6) (R7) (R8) (R9)

(R10)

          prefix_unify([]).
          prefix_unify([S=T|G]) :-
               ( -S2=S -> T2=T ; -S2=T, T2=S ), flatten(S2,S1), flatten(T2,T1),
               ( logic(s5) -> tuni_s5(S1,T1) ;
                 logic(d)  -> tuni_d(S1,T1) ;
                 logic(t)  -> tuni_t(S1,[],T1) ;
                 logic(s4) -> tunify(S1,[],T1) ),
               prefix_unify(G).
          tuni_t([],[],[]).
          tuni_t([],[],[X|T])       :- tuni_t([X|T],[],[]).
          tuni_t([V|S],[],[])       :- V=[], tuni_t(S,[],[]).
          tuni_t([X1|S],[],[X2|T]) :- (var(X1) -> (var(X2), X1==X2);
                                          (\+var(X2), unify_with_occurs_check(X1,X2))),
                                          !, tuni_t(S,[],T).
          tuni_t([V|S],[],[X|T])   :- var(V), tuni_t([V|S],[X],T).
          tuni_t([C|S],[],[V|T])   :- \+var(C), var(V), tuni_t([V|T],[C],S).
          tuni_t([V1|S],[],[V2|T]) :- var(V1), V2=[], tuni_t(T,[V1],S).
          tuni_t([V|S],[X],T)       :- V=[], tuni_t(S,[X],T).
          tuni_t([V|S],[X],T)       :- var(V), unify_with_occurs_check(V,X),
                                          tuni_t(S,[],T).
          tuni_t([C|S],[V],T)       :- \+var(C), var(V), unify_with_occurs_check(V,C),
                                          tuni_t(S,[],T).

Figure 8: Source code of the prefix unification for the modal logic T

The predicate prefix_unify(G) is used to solve a set of prefix equations. Its code is shown in the upper part of Figure 8. The set of prefix equations G is presented by a Prolog list of equations of the form S=T. In each step one prefix equation is selected (line b) and the appropriate prefix unification is invoked depending on the logic specified by the logic predicate (line d to g). The remaining equations are considered afterwards (line h). If all equations are solved (line a) the predicate prefix_unify succeeds. A minus sign in front of a prefix (used for technical reasons) is deleted and prefixes are flattened (as they may contain nested lists) before the unification starts (line c).

The predicates tuni_s5 and tuni_d implementing the prefix unification for the modal logics S5 and D, respectively, are straightforward. Details about the predicate tunify implementing the prefix unification for the modal logic S4 can be found in [10].

4.2 The Connection Calculus

The implementation of the connection calculus for first-order modal logic, called MleanCoP, is based on leanCoP 2.0, an automated theorem prover for first-order classical logic [11]. To adapt the implementation to the modal connection calculus of Section 3.2 the leanCoP prover is extended by (a) prefixes that are added to literals and collected during the proof search and (b) an additional list that contains term variables together with their prefixes in order to check the domain condition. First, MleanCoP performs a classical proof search. After a proof is found, the prefixes of the literals in each connection are unified and the domain condition is checked. If the prefix unification fails the (classical) search for alternative connections continues via backtracking. The Prolog source code of the MleanCoP core prover is shown in Figure 9. The underlined code was added to leanCoP; no other modifications were done. In ECLiPSe Prolog sound unification has to be switched on with set_flag(occur_check,on).

(a) (b) (c) (d) (e) (f) (g) (h) (i) (j) (k)

(1) (2) (3) (4) (5) (6) (7) (8) (9) (10) (11) (12) (13) (14) (15) (16) (17) (18) (19)

             prove(PathLim,Set) :-
                 ( \+member(scut,Set) ->
                   prove([(-(#))\underline{:(-[])} ],[],PathLim,[],\underline{[PreSet,FreeV1],}  Set) ;
                   lit((#)\underline{:_},\underline{FV:}C,_) ->
                   prove(C,[(-(#))\underline{:(-[])} ],PathLim,[],\underline{[PreSet,FreeV],}  Set)\underline{,}
                   \underline{append(FreeV,FV,FreeV1)}    )\underline{,}
                   \underline{domain_cond(FreeV1), prefix_unify(PreSet)}      .
             prove(PathLim,Set) :-
                 member(comp(Limit),Set), PathLim=Limit -> prove(1,[]) ;
                 (member(comp(_),Set);retract(pathlim)) ->
                 PathLim1 is PathLim+1, prove(PathLim1,Set).

             prove([],_,_,_,\underline{[[],[]],} _).
             prove([Lit\underline{:Pre} |Cla],Path,PathLim,Lem,\underline{[PreSet,FreeV],}  Set) :-

                 \+ (member(LitC,[Lit\underline{:Pre} |Cla]), member(LitP,Path), LitC==LitP),
                 (-NegLit=Lit;-Lit=NegLit) ->
                     ( member(LitL,Lem), Lit\underline{:Pre} ==LitL\underline{, PreSet3=[], FreeV3=[]}
                       ;
                       member(NegL\underline{:PreN} ,Path), unify_with_occurs_check(NegL,NegLit)\underline{,}
                       \+ \+ prefix_unify([Pre=PreN]), PreSet3=[Pre=PreN], FreeV3=[]
                       ;
                       lit(NegLit\underline{:PreN} ,\underline{FV:}Cla1,Grnd1),
                       \+ \+ prefix_unify([Pre=PreN]),
                       ( Grnd1=g -> true ; length(Path,K), K<PathLim -> true ;
                         \+ pathlim -> assert(pathlim), fail ),
                       prove(Cla1,[Lit\underline{:Pre} |Path],PathLim,Lem,\underline{[PreSet1,FreeV1],}  Set)\underline{,}
                       PreSet3=[Pre=PreN|PreSet1], append(FreeV1,FV,FreeV3)
                     ),
                     ( member(cut,Set) -> ! ; true ),
                     prove(Cla,Path,PathLim,[Lit\underline{:Pre} |Lem],\underline{[PreSet2,FreeV2],}  Set)\underline{,}
                     \underline{append(PreSet3,PreSet2,PreSet), append(FreeV2,FreeV3,FreeV)}        .

Figure 9: Source code of the MleanCoP core prover

The open subgoal C and the active path P ath in the modal connection calculus of Figure 5 are represented by the Prolog lists Cla and Path, respectively. The matrix M is written into Prolog’s database in a preprocessing step. For every clause C∈M and for every literal Lit:Pre∈C the fact lit(Lit:Pre,FV:C1,Grnd) is stored where FV is a list of elements of the form [V,Pre1] in which V is a term variable in C and Pre1 is its prefix, C1=C\{Lit:Pre} and Grnd is g if C is ground, otherwise Grnd is n. Atoms are represented by Prolog atoms, term variables by Prolog variables and negation by “-”. The substitutions σ_{Q} and σ_{M} are stored implicitly by Prolog.

   The predicate prove(Cla,Path,PathLim,Lem,[PreSet,FreeV],Set) in line 1 to 19

implements the axiom, the reduction rule and the extension rule of the modal connection calculus of Figure 5. PathLim is the maximum size of the active path used for iterative deepening, Lem is a set of literals used as lemmata, and Set is a list of options used to control the proof search (see [12] for details). For modal logic the lists PreSet and FreeV were added. They contain a list of prefix equations and a list of term variables with their prefixes that are collected during the proof search.

Line 1 implements the axiom, line 4 calculates the complement of the first literal Lit:Pre in the list of open subgoals, which is is used for the following reduction step (line 7/8 and 18/19) or extension step (line 10/11, 14/15 and 18/19). In line 7 it is checked whether the active path Path contains a literal NegL:PreN that unifies with the complement NegLit:Pre of the literal Lit:Pre. In Line 8 a weak prefix unification of the prefix equation Pre=PreN is carried out (double negation prevents any variable bindings). Line 18 and 19 continue the proof search for the premise of the reduction rule.

In line 10 the predicate lit(NegLit:PreN,FV:Cla1,Grnd1) is used to find a clause that contains the complement of the literal Lit:Pre. FV is the list of term variables occuring in Cla1, Cla1 is the remaining set of literals of the selected clause. Again, weak prefix unification in line 11 ensures that the prefixes of the new connection are unifiable. In line 14 the proof search for the left premise of the extension rule is invoked with the new open subgoal Cla1 and the active path Path extended by the literal Lit:Pre. Afterwards the proof search for the right premise is invoked in line 18. The lists of prefix equations and term variables are collected in line 8, 15 and 19.

The predicate prove(PathLim,Set) in line a to k implements the start rule of the modal connection calculus in Figure 5. When the matrix M is written into Prolog’s database the distinct literal #:[] is added to all positive clauses. In line c the proof search starts with the open subgoal [(-(#)):(-[])] and the empty active path [], i.e. only positive clauses are used as start clause. After the classical proof search succeeds the domain condition is checked and the prefixes of each connection are unified. To this end the two predicates domain_cond (see the complete source code on the MleanCoP web site) and prefix_unify (see Section 4.1) are invoked in line g.

Prolog uses a depth-first search strategy resulting in an incomplete proof search. In order to regain completeness MleanCoP performs an iterative deepening on the size of the active path. When the extension rule is applied and the new clause is not ground, i.e. it contains a (term or prefix) variable, it is checked whether the size K of the active path exceeds the current path limit PathLim (line 12). In this case the predicate pathlim is written into Prolog’s database (line 13) indicating the need to increase the path limit. If the proof search for the current path limit fails and the predicate pathlim was written into the database (line j), then PathLim is increased and the proof search starts again (line k).

leanCoP uses a few additional techniques, which are integrated into MleanCoP as well; see [12] for details. Regularity ensures that no literal occurs more than once in the active path. It is integrated into the modal connection calculus in Figure 5 by imposing the following restriction on the reduction and the extension rule: ∀ L′: p′ ∈ C ∪{L_{1}: p_{1}} : σ_{Q}(σ_{M}(L′: p′)) ∉ σ_{Q}(σ_{M}(P ath)). Line 3 implements a ground version of the regularity condition in MleanCoP. The idea of Lemmata or factorization is to reuse subproofs during the proof search. To this end an additional argument Lem is added to the prove predicate and line 5 is added to the MleanCoP source code. Restricted backtracking [12] is a very effective technique to restrict backtracking in the connection calculus. It is implemented in line b, d, e, f , and 17. A definition clausal form translation reduces the number of possible connections and, hence, the search space. Furthermore, MleanCoP uses a fixed strategy scheduling, i.e. the core prover is invoked repeatedly by a shell script with different prover options given in the list Set.

Example 10 (MleanCoP). Consider the modal formula F_{1} and its matrix M_{1} of Example 4. The goal

prove(((* ex X:p(X) , # all Y:(* p(Y) => q(Y)) ) => * ex Z:q(Z))) succeeds; hence, F_{1} is

valid. The (internal) representation of M_{1} (with added variable/prefix lists) is [[]:[-(p(d^[]^[a1])):

-([a1])], [[Y,[V1]]]:  [p(Y): [V1,V2], -(q(Y)): -([V1])], [[Z,[V3]]]:  [q(Z): [V3]]].

5 Performance

The MleanCoP implementation of Section 4.2 was tested on all 580 uni-modal problems of version 1.1 of the QMLTP library [14]. All problems were converted into the MleanCoP syntax using the TPTP2X tool [15] together with the format file included in the QMLTP library. All tests were conducted on a 3.4 GHz Xeon system with 4 GB of RAM running Linux 2.6.24 and ECLiPSe Prolog 5.10. The CPU time limit for all proof attempts was 600 seconds. Table 3 gives a summary of the test result. It shows the number of solved problems for the varying, cumulative, and constant domain of the modal logics D, T, S4, and S5 for the provers MleanCoP 1.2 (CoP), MleanTAP1.3 (TAP), and MleanSeP 1.2 (SeP).^{5}

Table 3: Number of solved problems from the QMLTP library v1.1

varying domain  cumulative domain  constant domain
logic  CoP TAP SeP  CoP TAP SeP  CoP TAP SeP
D  422 104  –  424 124 134  426 139 135
T  369 142  –  374 164 167  381 179 167
S4  393 173  –  432 209 201  434 224 198
S5  447 223  –  479 276  –  479 276  –

MleanSeP implements the standard modal sequent calculus (see Definition 1) for several modal logics. Proof search is carried out in an analytic way and free term variables are used together with a dynamic Skolemization to ensure the Eigenvariable condition. For the constant domain variants the Barcan formula (scheme) is added in a preprocessing step. The prover does not deal with the modal logic S5 and the varying domain variants as they do not have (cut-free) sequent calculi [17].

MleanTAPis a compact implementation of a prefixed tableau calculus for several modal logics. Similar to the modal connection calculus presented in Section 3.2 it is based on the modal matrix characterization of validity given in Theorem 1. Like MleanCoP it first performs a purely classical proof search. After a classical tableau proof is found the prefixes of those literals that closed the tableau branches are unified. The existence of a unifier ensures that the given formula is valid in modal logic. MleanCoP and MleanTAPuse the same source code for the prefix unification and for checking the domain condition.

Table 4 presents detailed performance results of the three theorem provers on the QMLTP library. It shows for each considered modal logic and domain the number of solved problems, the number of proved (i.e. valid) problems, the number of refuted (i.e. invalid) problems, and the number of problems that are proved within specific time intervals. In general, MleanCoP proves and refutes significantly more problems than MleanTAPand MleanSeP . The number of proved problems by MleanTAPand MleanSeP is similar, but MleanSeP has a better time complexity behaviour; MleanTAPsolves only two problems (for S4) in a time of more than 10 seconds. As MleanCoP uses a fixed strategy scheduling, many problems are solved in a time of more than one second. In general, the fewest problems are proved for the modal logic D with varying domain and the highest problems are proved for S5 with cumulative or constant domain. This behaviour is in line with the following fact:

If Theorem(L, D) is the set of theorems in the modal logic L with the domain D, then for all logics L ∈ {D,T,S4} and all domains D it is: Theorem(D, D) ⊂ Theorem(T, D) ⊂ Theorem(S4, D) ⊂ Theorem(S5, D) and Theorem(L,varying) ⊂ Theorem(L,cumulative) ⊂ Theorem(L,constant); furthermore, it is Theorem(S5,varying) ⊂ Theorem(S5,cumulative) = Theorem(S5,constant).

5 None of these provers were tuned towards the problems in the QMLTP library. MleanSeP and MleanTAPcan be obtained at http://www.leancop.de/mleansep/ and http://www.leancop.de/mleantap/ .

Table 4: Detailed performance results for the modal logics D, T, S4, and S5

varying domain  cumulative domain  constant domain
logic  CoP TAP SeP  CoP TAP SeP  CoP TAP SeP
D  solved  422 104  –  424 124 134  426 139 135
proved  179 100  –  200 120 130  217 135 134
refuted  243  4  –  224  4  4  209  4  1
proved 0s to 1s  149 97  –  169 117 126  187 132 101
1s to 10s  11  3  –  12  3  4  11  3 28
10s to 100s  7  0  –  7  0  0  7  0  3
100s to 600s  12  0  –  12  0  0  12  0  2
T  solved  369 142  –  374 164 167  381 179 167
proved  224 138  –  249 160 163  269 175 166
refuted  145  4  –  125  4  4  112  4  1
proved 0s to 1s  199 133  –  223 157 156  238 172 148
1s to 10s  10  5  –  11  3  6  12  3 10
10s to 100s  9  0  –  9  0  1  10  0  7
100s to 600s  6  0  –  6  0  0  9  0  1
S4  solved  393 173  –  432 209 201  434 224 198
proved  274 169  –  338 205 197  352 220 197
refuted  119  4  –  94  4  4  82  4  1
proved 0s to 1s  245 167  –  286 202 152  301 217 146
1s to 10s  11  2  –  18  2 32  18  2 13
10s to 100s  11  0  –  21  1  6  18  1 30
100s to 600s  7  0  –  13  0  7  15  0  8
S5  solved  447 223  –  479 276  –  479 276  –
proved  359 219  –  438 272  –  438 272  –
refuted  88  4  –  41  4  –  41  4  –
proved 0s to 1s  307 215  –  372 269  –  372 269  –
1s to 10s  23  4  –  24  3  –  24  3  –
10s to 100s  16  0  –  25  0  –  25  0  –
100s to 600s  33  0  –  17  0  –  17  0  –

6 Conclusion

An implementation of a modal connection calculus for various first-order modal logics was presented. The modal connection calculus extends the classical calculus by prefixes and an additional prefix unification procedure. The specific modal logic and domain variant is selected through different prefix unification algorithms and different domain conditions, respectively. The Skolemization technique is extended to prefix variables. This makes an explicit reflexivity test of the reduction ordering redundant and simplifies the implementation. The implementation itself is based on the classical leanCoP prover. Optimization techniques used in leanCoP, such as regularity, lemmata, restricted backtracking and a definitional clausal form translation, are adapted and integrated into the modal prover MleanCoP as well.

Experimental results on the QMLTP library indicate that the performance of MleanCoP is significantly higher than the performance of provers based on analytic sequent calculi or prefixed tableau calculi. Hence, a connection-driven strategy seems to be essential for an efficient proof search based on approaches that use prefixes and a prefix unification procedure. A similar effect was already observed for first-order intuitionistic logic [10].

The development of automated theorem proving systems for first-order modal logic is still in its early stages. Only few other implementations exist so far. Another promising approach is the embedding of first-order modal logic into simple type theory [2, 3]. Future work includes the comparison with implementations of this and other approaches.

While a clausal form technically simplifies the proof search procedure, the translation into clausal form has a negative effect on the number of (possible) connections and, thus, on the size of the resulting search space. A non-clausal connection calculus [13] avoids any translation steps and preserves the structure of the original formula. Future work also includes the improvement of the prefix unification algorithm as this is the component that captures the main part of the additional search required for (first-order) modal logics.

Acknowledgements. The author would like to thank Thomas Raths for testing all implementations on the QMLTP library and providing the presented performance statistics.

References

[1] G. Beckert, R. Goré. Free Variable Tableaux for Propositional Modal Logics. In D. Galmiche, Ed., TABLEAUX 1997, LNAI 1227, pp. 91–106. Springer, Heidelberg, 1997.

[2] C. Benzmüller, L. Paulson. Quantified Multimodal Logics in Simple Type Theory. SEKI Report SR–2009–02 (ISSN 1437–4447), Saarland University, 2009.

[3] C. Benzmüller, L. Paulson. Multimodal and Intuitionistic Logics in Simple Type Theory. The Logic Journal of the IGPL, 18(6):881–892, 2010.

[4] W. Bibel. Automated Theorem Proving. Vieweg, Wiesbaden, 1987.

[5] M. Fitting. Proof Methods for Modal and Intuitionistic Logic. D. Reidel, Dordrecht, 1983.

[6] M. Fitting, R. L. Mendelsohn. First-Order Modal Logic. Kluwer, Dordrecht, 1998.

[7] G. Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39:176–210, 405–431, 1935.

[8] R. Hähnle. Tableaux and Related Methods. In A. Robinson, A. Voronkov, Eds., Handbook of Automated Reasoning, pp. 100–178. Elsevier, Amsterdam, 2001.

[9] U. Hustadt, R. A. Schmidt. MSPASS: Modal Reasoning by Translation and First-Order Resolution. R. Dyckhoff, Ed., TABLEAUX 2000, LNAI 1847, pp. 67–81. Springer, Heidelberg, 2000.

[10] J. Otten. Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic. In B. Beckert, Ed., TABLEAUX 2005, LNAI 3702, pp. 245–261. Springer, Heidelberg, 2005.

[11] J. Otten. leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic. In A. Armando, P. Baumgartner, G. Dowek, Eds., IJCAR 2008, LNCS 5195, pp. 283–291. Springer, Heidelberg, 2008.

[12] J. Otten. Restricting Backtracking in Connection Calculi. AI Communications 23:159–182, 2010.

[13] J. Otten. A Non-clausal Connection Calculus. In K. Brünnler, G. Metcalfe, Eds., TABLEAUX 2011, LNAI 6793, pp. 226–241. Springer, Heidelberg, 2011.

[14] T. Raths, J. Otten. The QMLTP Problem Library for First-order Modal Logics. 2012. Submitted.

[15] G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning, 43(4):337–362, 2009.

[16] A. Waaler. Connections in Nonclassical Logics. In A. Robinson, A. Voronkov, Eds., Handbook of Automated Reasoning, pp. 1487–1578. Elsevier, Amsterdam, 2001.

[17] L. Wallen. Automated deduction in nonclassical logic. MIT Press, Cambridge, 1990.