Prefixes encoding the Kripke semantics and an additional prefix unification can be used when performing proof search in some popular non-classical logics. The paper presents two techniques that optimize this approach for the first-order modal logics D and S5. The first one improves backtracking in the modal connection provers MleanCoP and nanoCoP-M, the second one provides an embedding from the modal logics D and S5 into classical first-order logic. Both techniques have been implemented. A practical evaluation on the QMLTP benchmark library shows a significant performance improvement.
This section introduces the basic concepts of prefixes and the modal matrix characterization of
logical validity for the modal logics D, T, S4 and S5. See [
A first-order modal formula F (or G, H ) is composed of atomic formulae, the standard connectives ¬, ∧, ∨, ⇒, the standard quantifiers ∀ and ∃, and the unary modal operators □ and ♢ . The Kripke semantics of the standard modal logics is defined by a set of worlds W and a binary accessibility relation R ⊆ W × W between these worlds. In each single world w ∈ W the classical semantics applies to the standard connectives and quantifiers. The modal operators are interpreted with respect to accessible worlds: □F /♢ F is true in a world w iff F is true in all/some world(s) w′ with (w, w′)∈R, i.e., accessible from w.
The properties of the accessibility relation R determine the specific modal logic. For example, the accessibility relation can be serial (modal logic D)1, reflexive (modal logic T), reflexive and transitive (modal logic S4), or an equivalence relation (modal logic S5). The standard semantics is considered with rigid term designation, i.e. every term denotes the same object in every world, and terms are local, i.e. any ground term denotes an existing object in every world.
A prefix is used to name a sequence of accessible worlds in which a formula holds and is assigned to each subformula of a given formula F . For example, the prefix w1 . . . wn of a modal formula
from a world w1. 2 Definition 1 (Modal prefix). A prefix (denoted by p) is a string (i.e. a sequence of characters) over an alphabet ν ∪ Π, in which ν is a set of prefix variables (V1, ...) and Π is a set of prefix constants (a1, ...). If a formula F with polarity pol ∈ {0, 1} has the prefix p, written F pol : p, then the prefixes (and polarities) of its subformulae G and H are defined inductively according to the table below. It is ⊙ ∈ {∧, ∨}, Q ∈ {∀, ∃}; V ∈ ν and a ∈ Π are new prefix characters that have not been used before. The (modal) prefix of a given (modal) formula F is the empty string ε, the prefixes of its subformulae are the prefixes of the corresponding formula F 0 : ε. The prefix pre(x) of a term variable x occurring in a (sub)formula Qx G is the prefix of the subformula G. 1A relation R ⊆ W × W is serial iff for all w1 ∈ W there is some w2 ∈ W with (w1, w2) ∈ R. 2The start world, e.g. w0, is omitted from all prefixes. Therefore, a prefix can also be empty.
F pol : p (G ⊙ H )pol : p (G ⇒ H )pol : p (¬G)pol : p (Q x G)pol : p
Gpol′ : p′ Gpol : p G1−pol : p G1−pol : p Gpol : p
F pol : p (□G)1 : p (♢ G)0 : p (□G)0 : p (♢ G)1 : p
Gpol′ : p′ G1 : pV G0 : pV G0 : pa
G1 : pa H pol′′ : p′′ H pol : p H pol : p Example 1. Consider the Barcan formula
The prefixes of FB and its subformulae are: FB0 : ε, (∀x □ p(x))1 : ε, (□ p(x))1 : ε, p(x)1 : V1, (□ ∀y p(y))0 : ε, (∀y p(y))0 : a1, and p(y)0 : a1, in which V1 is a new prefix variable and a1 is a new prefix constant. It is pre(x) = ε and pre(y) = a1.
Proof-theoretically, prefix variables and constants represent applications of the rules □-left/♢ right (ν-rules) and □-right/♢ -left (π-rules), respectively, in the modal sequent calculus. A prefix of a formula F specifies the sequence of modal rules that have to be applied (analytically or bottom-up) in order to obtain the formula F in the sequent.
In Fitting’s modal tableau calculus [
A more efficient proof search adds a prefix variable whenever a modal ν-rule is applied and delays choosing an appropriate sequence of constant characters until a branch is closed. This resembles the approach of using free variables in classical (tableau or sequent) calculi, i.e. using term variables instead of guessing an appropriate first-order term whenever a (nonEigenvariable) quantifier rule is applied and using term unification whenever a branch is closed in order to assign actual terms to these free term variables. Using prefix variables requires a prefix substitution in order to make prefixes of literals that close a branch identical. Definition 2 (Prefix substitution). A prefix substitution σP : ν → (ν ∪ Π)∗ maps elements of ν to strings over ν ∪ Π. In σP (p) prefix variables are replaced according to σP .
The accessibility condition and the domain condition ensure that the prefix substitution respects the accessibility relation and the domain variant of the considered modal logic.
Depending on the accessibility relation, variables may be substituted by exactly one prefix character (modal logic D), by at most one prefix character (modal logic T) or by an arbitrary string (modal logic S4). For the modal logic S5 only the last character of each prefix is considered (or the the empty string if the prefix is empty).
Definition 3 (Accessibility condition). For the modal logics D and T the accessibility condition is |σP (V )|=1 and |σP (V )|≤1 for all V ∈ ν, respectively.
Each first-order modal logic can have different domain conditions. If D(w) is the (firstorder) domain of a world w, then a modal logic has constant domains if D(w1) = D(w2) for all w1, w2 ∈ W and it has cumulative (or increasing) domains if D(w1) ⊆ D(w2) for all w1, w2 ∈ W with (w1, w2) ∈ R. A modal logic has varying domains if there are no restrictions on the domains of the worlds.
In case of varying domains, objects may only exists in the world in which they are introduced. For cumulative domains, Eigenvariables3 have to be introduced before the term variable they are assigned to. For constant domains, there is no such restriction as every object exists in all worlds. The domain condition captures these restrictions on prefixes of first-order variables. Definition 4 (Domain condition). Let σT be a term (or first-order) substitution and σP a prefix substitution. The domain condition for (a) varying and (b) cumulative domains states that for all term variables x and all Eigenvariables x¯ occurring in the term σ(x): (a) σP (pre(x¯)) = σP (pre(x)) and (b) σP (pre(x¯)) σP (pre(x)), respectively.4 For constant domains and S5 with cumulative domains the domain condition is always true.
Definition 5 (Admissible substitution). A combined substitution σ = (σT , σP ) is
admissible with respect to a specific modal logic iff the accessibility condition holds for σP and the domain
condition holds for σT /σP for that logic. Furthermore, the reduction ordering induced by σ has to
be irreflexive (see [
Example 2. Consider the formula FB from Example 1. The prefix substitution σP (V1) = a1 makes the prefixes of the two atomic formulae p(x) : V1 and p(y) : a1 identical. As |σP (V1)| = 1, σP fulfills the accessibility condition for D, T, S4 and S5. For the term substitution σT (x) = y it is σP (pre(y)) = a1 6 ε = σP (pre(x)), hence, σB = (σT , σP ) is only admissible for D, T, S4 and S5 with constant domains and for S5 with cumulative domains.
A modal formula can be translated into a prefixed clausal (disjunctive normal) form, where
prefixes are added to atomic formulae. This is called a prefixed matrix. It is a compact
representation of the proof search space. The clausal modal matrix characterization presented in the
following is derived from Wallen’s original non-clausal characterization of logical validity [
A path represents the set of all atomic formulae in a “final sequent” in the classical sequent
calculus [
A multiplicity µ : M → IN specifies the number of clause copies used in a proof. M μ denotes the matrix that includes clause copies according to µ . Clause copies correspond to applications of the contraction rule in the sequent calculus.
If (and only if) all paths through a matrix of a formula contain a σ-complementary connection
for some admissible substitution σ, the formula is valid. In this case every final sequent of the
corresponding derivation in the (free-variable) sequent calculus would contain an axiom (as
paths represent final sequents and complementary connections represent axioms).
Theorem 1 (Matrix characterization for modal logics). A modal formula F is valid in the
modal logic L iff there is
1. a multiplicity µ ,
2. a combined substitution σ = (σT , σP ) that is admissible with respect to L, and
3. a set S of σ-complementary connections,
such that every path through M μ(F ) contains a connection from S. (See [
A proof search based on the presented matrix characterization has to calculate an appropriate
combined substitution σ=(σT , σP ). Whereas the term substitution σT is calculated by one of
the known algorithms for term unification, calculating the prefix substitution σP has to be done
by a special prefix unification algorithm [
The prefix unification problem is a special case of string unification (the monoid problem for word equations) that takes the prefix property (or T-string property) of the modal prefixes into account: for all prefixes p1 = u1Xw1 and p2 = u2Xw2 it is u1 = u2 (with X ∈ ν ∪ Π and u1, u2, w1, w2 ∈ (ν ∪ Π)∗).
In contrast to term unification, which has only a single most general unifier (mgu), the number
of mgus for prefix unification might grow exponentially. More specifically, in the worst case the
number of mgus is 12 (n2!n)2)! ∈ O( 2√2nn ) when unifying the two prefixes V1 . . . Vn and a1 . . . an [
As the number of mgus for prefix unification can grow, in general, exponentially, it is in practice more efficient to first search for a classical proof, i.e. ignoring all prefixes, and perform the prefix unification and the check of the domain condition afterwards, as pictured below. 1. classical proof search: calculate (only) S and σT 2. check domain condition: calculate σ′
P
This approach is used by the modal connection provers MleanCoP [
To improve efficiency, the domain condition check and the prefix unification is integrated into the classical proof search, i.e. the prefix substitution σP is calculated directly after a connection is identified. This results in a (modal) proof search that consists of only one (major) step instead of three, as pictured below.
1. modal proof search: calculate S, σT and σP (simultaneously)
This approach ensures that the calculated set of connections is always σ-complementary and a failed check of the domain condition or prefix unification is quickly detected. Even though this also leads to some overhead, in general, this results in a more efficient proof search for the modal logics D and S5.
Example 4. Consider the formula ( ∀x ♢ p(x) ) ⇒ ( □ p(b1) ∨ . . . ∨ □ p(bn) ∨ ♢ p(c) ) with the matrix {{p(x)0: a}, {p(b1)1: a1}, . . . {p(bn)1: an}, {p(c)1: V1}}}. So far, MleanCoP and nanoCoP-M first perform a (purely) classical proof search by identifying the connection S = {p(x)0: a, p(b1)1: a1} with the term substitution σT (x) = b1. But the prefix unification of the two prefixes a and a1 fails (the domain condition is always true). Afterwards, backtracking within the classical proof search is done. This results in the next classical proof with S = {p(x)0: a, p(b2)1: a2} and σT (x) = b2. Again, the prefix unification of a and a2 fails. Backtracking within the classical proof continues and results in, altogether, n different classical proofs for which the subsequent prefix unification fails. Only for the last possible classical proof with S = {p(x)0: a, p(c)1: V1} and σT (x) = c the prefix unification of a and V1 succeeds with σP (V1) = a. An improved procedure that calculates the prefix substitution directly after a connection is identified would immediately identify the modal proof with S = {p(x)0: a, p1(c): V1}, σT (x) = c and σP (V1) = a, avoiding any backtracking within the classical proof search. That this approach is more efficient becomes clearer for slightly larger formulae with a larger classical proof (search) and, hence, more choices for backtracking.
As |σ(V )| = 1 for the modal logic D and |p| ≤ 1 for all prefixes p in S5, the prefixes of atomic formulae can be included in their arguments and unified by the standard term unification. This yields an embedding for these modal logics into classical logic. Definition 8 (Translation into classical logic). The translation T of a prefixed modal formula into a classical formula is defined according to Table 1. In this table, P (. . .) is an atomic formula, t1, . . . , tn are (first-order) terms, pol ∈ {0, 1} is a polarity, V is a set of term and prefix variables, p and c1 . . . cm are prefixes. fpmre is a new function symbol with arity m≥1, epspre is a unique constant, V ∈ ν is a new prefix variable, and c|sVk|(V ) is a new (skolemized) prefix constant parametrized with the variables in V . The translation of a modal formula F is T (F ) := T (F : ǫ, {}). T (P (t1, . . . , tn)pol : ε, V) = P (t1, . . . , tn, fp1re(epspre)) 1 T (P (t1, . . . , tn)pol : c1 . . . cm, V) = P (t1, . . . , tn, fpre(cm)) T (P (t1, . . . , tn)pol : c1 . . . cm, V) = P (t1, . . . , tn, fpmre(c1, . . . , cm)) T ((G ⊙ H)pol : p, V) = (T (Gpol : p, V) ⊙ T (Hpol : p, V)) T ((G ⇒ H)pol : p, V) = (T (G1−pol : p, V) ⇒ T (Hpol : p, V)) T ((¬G)pol : p, V) = (¬ T (G1−pol : p, V)) for D and S5 only for S5 only for D ⊙ ∈ {∧, ∨} T ((∀ x G)1 : p, V) = (∀ x T (G1 : p, V∪{x})) T ((∃ x G)0 : p, V) = (∃ x T (G0 : p, V∪{x})) T ((∀ x G)0 : p, V) = (∀ x T (G0 : p, V)) T ((∃ x G)1 : p, V) = (∃ x T (G1 : p, V))
T ((□ G)1 : p, V) = (∀ V T (G1 : p V, V∪{V })) T ((♢ G)0 : p, V) = (∃ V T (G0 : p V, V∪{V })) T ((□ G)0 : p, V) = T (G0 : p c|sVk|(V), V)
T ((♢ G)1 : p, V) = T (G1 : p c|sVk|(V), V)
The prefixes of atomic formulae are now part of the function fpre, which is added as last argument to each atomic formula. Skolemization is extended to the prefix constants (function csk) in order to check the irreflexivity of the reduction ordering by the occurs check of the term unification.5 This embedding works for the modal logics that do not have any domain condition, i.e., for D and S5 with constant domains (and, hence, also for S5 with cumulative domains). Theorem 2 (Correctness of translation T ). A modal formula F is valid in the modal logics D or S5 with constant domains iff its translated formula T (F ) is valid in classical logic.
This theorem follows from the matrix characterization (Theorem 1) and the restriction of the accessibility condition for D and S5. The translation T preserves the structure of the formula, only the modal operators are eliminated and one argument is added to all atomic formulae. Example 5. Consider again the Barcan formula
FB = (∀x □ p(x)) ⇒ (□ ∀y p(y)) .
Its translation (for both D and S5) is T (FB ) = (∀x ∀V p(x, fp1re(V ) ⇒ (∀y p(y, fp1re(csk))). As
T (FB ) is classically valid, FB is valid for the modal logics D and S5 with constant domains (and
also for the modal logic S5 with cumulative domains).
5This proof-theoretical view on Skolemization is crucial for its extension to prefixes, see also [
The optimization and embedding of Section 3 have been implemented within three systems for the first-order modal logics D and S5.
1. MleanCoP-DS5 is an optimized version of the clausal connection prover MleanCoP, 2. nanoCoP-M-DS5 is an optimized version of the non-clausal prover nanoCoP-M, 3. nano-M2C implements an embedding of modal logic into classical logic.
The optimization described in Section 3.1 was integrated into the provers MleanCoP 1.3 [
In the original MleanCoP and nanoCoP-M provers the (rigid) prefix substitution σP is calculated only after a classical proof (and an appropriate set of connections S) is found. In the optimized “DS5” versions, the prefix substitution σP is calculated/extended directly after a new connection is identified. This is done by unifying the prefixes of each new connection and checking the appropriate domain condition. Since there is only a single most general prefix unifier for D and S5, no backtracking over alternative prefix substitutions is necessary.
The optimized provers MleanCoP-DS5 and nanoCoP-M-DS5 support the first-order modal logics D and S5 with constant, cumulative and varying domains.6
The translation T introduced in Definition 8 of Section 3.2 was implemented by the compact
Prolog program nano-M2C. The translation takes a modal formula/problem in QMLTP syntax
as input and translates it into a validity preserving formula in classical first-order logic according
to Table 1. The translated formula is written into a file and can be further processed by any
classical first-order prover, such as leanCoP [
The translation nano-M2C supports the first-order modal logics D with constant domains
and S5 with constant and cumulative domains.7
Example 6. The Barcan formula (∀x □ p(x)) ⇒ (□ ∀y p(y)) from Example 1 is included in the
QMLTP library [
(( ! [X] : (#box : ( f(X) ) ) ) => (#box : ( ! [X] : ( f(X) ) )) ) ). It is translated by nano-M2C into the following classical formula (pr/c_sko are new symbols): fof(con, conjecture, ( ! [X] : ! [V] : f(X, pre(V)) => ! [X] : f(X, pre(c_sko(1))) ) ). 6MleanCoP-DS5/nanoCoP-M-DS5 are available at http://leancop.de/mleancop/ and http://leancop.de/nanocop-m/. 7nano-M2C is available at http://leancop.de/nano-m2c/.
The three new implementations MleanCoP-DS5, nanoCoP-M-DS5 and nano-M2Cdescribed in
Section 4 were evaluated on all 580 unimodal problems of the QMLTP library v1.1 [
All evaluations were conducted on a LIFEBOOK U9311 with a 4-core i7-1185G7 CPU and 16GB of RAM, running Linux 5.13.0. ECLiPSe Prolog version 5.108 was used for all Prolog provers and the E prover was compiled with GNU gcc version 9.4.0. The time limit for all test runs was set to 100 seconds.
Table 2 shows the results for the modal clausal connection prover MleanCoP 1.3 [
Compared to the non-optimized versions, the optimized “‘DS5” connection provers solve between 21 and 38 more problems for the modal logic D. For the modal logic S5 the improvement is less significant, the optimized versions solve between two and seven more problems. 8ECLiPSe Prolog 5.x is available at https://eclipseclp.org/Distribution/Builds/. All newer versions of ECLiPSe Prolog are missing important features and have a significantly lower performance. 9Surprisingly, the non-strategy-scheduling version of E proves less problems than the classical connection provers.
This paper presents two techniques for advancing automated theorem proving for the first-order modal logics D and S5. It introduces an optimization of the prefix unification for two of the fastest existing modal provers, MleanCoP and nanoCoP-M, and an embedding of the modal logics D and S5 into classical logic.
Experiences from the development of nanoCoP-M have shown that it is getting increasingly
difficult to improve the performance of modal theorem provers on the QMLTP libray [
Ohlbach uses so-called world path to deal with the Kripke semantics of different modal
logics [
Future work includes improvements of the prefix unification algorithm for some other modal logics, such as T and S4. This includes solving prefix equations in a more parallel way and using information about failed prefix unifications directly in the classical proof search carried out in the first step. For a restricted set of modal first-order formulae, the embedding and translation nano-M2C into classical logic can also be used for the non-constant domains. This set includes, e.g., formulae for which the proof does not assign Eigenvariables to term variables.
The author would like to thank Stephan Schulz for providing the E prover. 10Leo-III does not support the QMLTP syntax, but previous evaluations show that it solves fewer problems than MleanCoP and, hence, also fewer problems than nanoCoP-M.