Resolution-Based Calculi for Modal and Temporal Logics

Andreas Nonnengart

Max-Planck-Institut für Informatik, Im Stadtwald, 66123 Saarbrücken, Germany, Tel.: (+49) 681 9325 221, Fax: (+49) 681 9325 299, Email: Andreas.Nonnengart@mpi-sb.mpg.de

Abstract. In this paper a technique is presented which provides us with a means to develop resolution-based calculi for (first-order) modal and temporal logics. The approach is based on three parts: A special translation technique from modal and temporal logic formulae into classical predicate logic, a certain kind of saturation technique which is to be applied to given background theories, and an extraction of either suitable “simpler” background theories or logic-specific inference rules. The former is interesting in case existing classical logic theorem provers are to be utilized; the latter gains importance if one is prepared to extend theorem provers that are already at hand.

1 Introduction

There are two possible directions to follow if one is interested in reasoning within modal and temporal logics: Either calculi are developed which can handle the special (extended) syntax directly [3], or, alternatively, translations into better known formalisms are defined. Typical examples are the relational (or standard) translation as well as the functional and – the approach used in this paper – the semi-functional translation, which all are translations into classical predicate logic [9, 10, 1, 6, 7, 8]. In these approaches the additional operators are translated with respect to a given semantics into first-order subformulae and the choice of the logic determines the background theory that is to be added to the translation result. Evidently, this already restricts the application of such approaches to cases where the induced theory is first-order. Particularly in the application of temporal logics to program verification this is quite a serious restriction indeed, since the well-known induction axioms for Next-operators cannot be completely specified. However, temporal logics are not only interesting in the area of program verification. They play an equally important role in many areas of artificial intelligence, in fact, whenever there is a need to represent the temporal order of events or situations. Therefore, the advantage of having the possibility to make use of many years, even decades, of experience in classical logic theorem proving often prevails over the disadvantage of not being able to handle the one or the other logic which might be interesting for some special applications.

The paper is structured as follows: First, there is a brief introduction to modal and temporal logic syntax and semantics. This can evidently not be done in detail here. The reader who is not familiar with the basics of modal and temporal logic is referred to [2, 4, 12, 11, 14]. Then the notion of a saturated theory is introduced. This forms the basis for the main recipe as described below which describes our main ideas about developing suitable calculi. Some examples then illustrate how this technique really works and a short comparison to other approaches finally concludes the paper. Now to the recipe whom we shall follow for each of the logics we are interested in:

1. Extract a theory.

2. Saturate this theory (with respect to resolution).

3. Consider the generated model assumption.

4. Find an alternative theory and/or

5. Determine logic-specific inference rules from the saturation.

Nothing yet is said about which theories are to be extracted and how this can be done. Neither it has been explained how such a theory can be saturated and how the result will look like. Also there is a need to explain what the generated model assumption is and what we can do with it. And, finally, it will have to be clarified what we mean by an alternative theory and how we can determine suitable inference rules. This all is what the following sections are about.

2 Some Preliminaries

2.1 Syntax and Semantics

First we have to fix the languages we are dealing with. In case of modal logics this is quite obvious: it is the classical predicate logic language extended by the modal operators □ and ◇. In case of temporal logics we consider additional operators like □^{F} , □^{F} _{r}, □^{P} , □^{P} _{r}, □^{A} _{r}, ◇^{F} , ◇^{F}_{r}, ◇^{P} , ◇^{P}_{r}, ◇^{A}_{r} with the intended meaning at all future times, from now on, at all past times, up to now, always, and their respective duals it will be the case etc. Moreover there are several Until and Since-operators with basic symbols U and S.

What the semantics is concerned, we consider the usual set of worlds (instants) and accessibility relations R_{i}, one for each operator □_{i}. For example, there is the “earlier-later”-relation R_{F} associated with the temporal operator □^{F} and the “later-earlier”-relation R_{P}^{∗} for □^{P} _{r}^{1}. A formula □_{i}Φ is then considered to be true at a world w if and only if Φ is true in every world w′ with R_{i}(w, w′). Analogously, we define ◇_{i}Φ to be true at w if Φ is true at some w′ with R_{i}(w, w′).

In the context of the (semi-)functional translation we additionally assume certain function sets F_{R_{i}} which are associated with the respective accessibility

1 The subscript “r” for operators indicates that the current instant, the Now, is to be included (“r” for “reflexivity). The associated accessibility relation R^{∗} is thus the reflexive (and transitive) closure of the base relation R.

relations R_{i} such that the following holds:

∀u, v ∃x ∈ F_{R_{i}} R_{i}(u, v) ⇔ u: x = v

This equivalence is a basic part of both the functional and the semi-functional translation approach. Essentially it states that the functions in F_{R_{i}} map worlds to R_{i}-accessible worlds (the “:” acts as an “apply”-function). We therefore call F_{R_{i}} a functional decomposition of the relation R_{i} and often write x_{i} to indicate that x is a term of the functional decomposition of R_{i}.

2.2 Saturation of Theories

The above was fairly standard. We now come to something completely different, the saturation of given theories.

Definition 1. Let P be a predicate symbol and let ℂ be a set of clauses such that P occurs positively^{2} in each clause of ℂ. We then call ℂ a positive P -theory^{3} and each clause in ℂ is said to be P -positive. A member of ℂ which contains no negative P -literal is called pure-P -positive.

Definition 2. Let ℂ be a positive P -theory. Then

Sat_{P} (ℂ) = {C | ℂ ⊢_{res} C and C is pure-P -positive}

Sat_{P} (ℂ) is called the saturation of ℂ with respect to the predicate symbol P and the standard resolution calculus.

Definition 3. Let ℂ be an arbitrary clause set. Then

Th_{P} (ℂ) = {C ∈ ℂ | C is P -positive}

Th_{P} (ℂ) is called the positive P -theory of ℂ.

Lemma 4. Let ℂ be a set of clauses and let P be a predicate symbol which occurs positively in ℂ. Moreover, let 𝔻 be a set of P -positive clauses such that Sat_{P} (𝔻) = Sat_{P} (Th_{P} (ℂ)). Then

ℂ is unsatisfiable iff (ℂ \ Th_{P} (ℂ)) ∪ 𝔻 is unsatisfiable

Proof. In general it holds that if ℂ_{1} contains P only negatively and ℂ_{2} is a positive P -theory then ℂ_{1} ∪ Sat_{P} (ℂ_{2}) is unsatisfiable if ℂ_{1} ∪ ℂ_{2} is unsatisfiable. For, suppose ℂ_{1} ∪ ℂ_{2} is unsatisfiable. Then there exists a finite unsatisfiable set of ground instances of ℂ_{1} ∪ ℂ_{2}. Now consider an arbitrary clause in the ground instances of ℂ_{2} which contains a negative P -literal, say ¬P (α)^{4}. We then perform

2 Note that the case where P occurs both positively and negatively in a clause is not

excluded. 3 Analogously we could define a negative P -theory as a set of clauses in which each

element contains at least one negative P -literal. 4 In case such a clause does not exist we know that Sat_{P} (ℂ_{2}) = ℂ_{2} and we are done.

every possible resolution step between the ¬P (α) and other clauses in the ground instance of ℂ_{2}^{5}. After this has been done, the clause containing ¬P (α) can be deleted without affecting unsatisfiability. This whole procedure can be performed for every negative P -literal in the ground instance of ℂ_{2} and so we obtain a finite unsatisfiable clause set which consists of the original instances from ℂ_{1} together with instances from Sat_{P} (ℂ_{2}), thus ℂ_{1} ∪ Sat_{P} (ℂ_{2}) is unsatisfiable as well. Now, in addition, suppose that ℂ_{3} is a positive P -theory such that Sat_{P} (ℂ_{2}) = Sat_{P} (ℂ_{3}). Then ℂ_{1} ∪ ℂ_{2} is unsatisfiable iff ℂ_{1} ∪ ℂ_{3} is unsatisfiable. The reason for this is: If ℂ_{1} ∪ℂ_{2} is unsatisfiable then (by the above argument) we know that ℂ_{1} ∪ Sat_{P} (ℂ_{2}) as well as ℂ_{1} ∪ Sat_{P} (ℂ_{3}) are unsatisfiable. Now, if ℂ_{1} ∪ ℂ_{3} were satisfiable, ℂ_{1} ∪ Sat_{P} (ℂ_{3}) would also be satisfiable and we had a contradiction (the other direction follows by a symmetric argument). Hence we know that

ℂ_{1} ∪ ℂ_{2} is unsatisfiable iff ℂ_{1} ∪ ℂ_{3} is unsatisfiable

provided ℂ_{1} contains P only negatively and ℂ_{2} and ℂ_{3} are positive P -theories with an identical saturation (with respect to P). However, from the above preliminaries we know that ℂ\Th_{P} (ℂ) contains P only negatively (and so may play the role of ℂ_{1} from above) and Th_{P} (ℂ) and 𝔻 may act as ℂ_{2} and ℂ_{3} respectively. Therefore

(ℂ \ Th_{P} (ℂ)) ∪ Th_{P} (ℂ) is unsatisfiable

iff (ℂ \ Th_{P} (ℂ)) ∪ 𝔻 is unsatisfiable

and we are done.

We thus may replace the positive P -theory of a given clause set by its saturation or any other positive P -theory which has an identical saturation. We illustrate this with a simple example.

Example 1. Let ℂ be a clause set with Th_{P} (ℂ) = {{P (a)}, {P (f(a))}, {P (x) ∧ P (f(x)) ⇒ P (f(f(x)))}}. By an easy induction over n it follows that

Sat_{P} (Th_{P} (ℂ)) = {P (f^{n}(a)) | n ≥ 0}.

An alternative positive P -theory would thus be 𝔻 = {{P (a)}, {P (x) ⇒ P (f(x))} and we may replace Th_{P} (ℂ) by 𝔻 without affecting (un-)satisfiablity. Note that this does not at all mean that Th_{P} (ℂ) and 𝔻 are logically equivalent. Rather it means that under the assumption that “nothing more is known about P ” both are equivalent. It is thus crucial for the whole approach that we consider not only something we know about P but all we know about P. Otherwise we would not be allowed to replace the given theory by the alternative just found.

5 Recall that such resolution steps with clauses from ℂ_{1} are not possible anyway, because ℂ_{1} contains P only negatively.

Up to this stage we know how to extract and to saturate theories. Moreover, we know how alternative theories are related to a given theory and its saturation. What we have not yet taken into account is the generated model assumption and the extraction of suitable new inference rules. The generated model assumption will play a role in the application to modal and temporal logics in later sections and although it can be applied and is significant in a more general setting, this is out of the scope of this paper. What the extraction of inference rules is concerned, we do already have almost all necessary preliminaries.

The main idea behind the development of theory-specific inference rules which are supposed to replace the whole (positive) P -theory lies in, say, “virtual” resolution steps with elements of the saturation. For the example from above this would mean to define the inference rule

\frac{¬P (f^{m}(γ)) ∨ C}{σC}

where m ≥ 0 and σ is the most general unifier (mgu) of the pair (γ, a). Observe that every application of this rule corresponds to a resolution step with an element of the theory’s saturation, but not the other way round. As a matter of fact, such inference rules represent certain resolution strategies and proving the soundness and completeness of the inference system obtained this way, actually means to prove the soundness and completeness of this very resolution strategy. We shall not do this for the above rule since this example is fairly trivial anyway.

2.3 Translation of Modal and Temporal Logic Formulae

The translation of modal and temporal logic formulae is now performed according to the underlying (semi-)functional semantics.

Definition 5. The semi-functional translation ⌈ ⌉ is defined as follows^{6}. Let Φ be a formula in negation normal form^{7}

\begin{matrix}⌈□^{F} Φ⌉^{u} & ⟶ & ∀v R_{F} (u, v) ⇒ ⌈Φ⌉^{v} \\ ⌈◇^{F} Φ⌉^{u} & ⟶ & ∃x_{F} ⌈Φ⌉^{u: x_{F}} \\ ⌈□^{P} Φ⌉^{u} & ⟶ & ∀v R_{P} (u, v) ⇒ ⌈Φ⌉^{v} \\ ⌈◇^{P} Φ⌉^{u} & ⟶ & ∃x_{P} ⌈Φ⌉^{u: x_{P}} \end{matrix}

where R_{F} (R_{P}) represents the earlier-later relation (the later-earlier relation respectively) and x_{F} (x_{P}) is a variable in the sort of the functional decomposition of R_{F} (R_{P}). The other temporal □- and ◇-operators are to be translated similarly. In case of modal logics there is evidently only one □ and one ◇-operator to be considered.

6 See also [6, 7, 8]. 7 Recall that a formula is in negation normal form if it contains no implication or

equivalence symbol and all negations immediately precede atoms. Evidently, for every formula there is an equivalence preserving transformation into negation normal form.

Note that in the semi-functional translation the unit clause R_{i}(u, u: x_{i}) has to be added to the translation result for each serial accessibility relation R_{i} (in case of non-serial relations this looks a bit different; but the temporal logics we are dealing with all have a serial earlier-later relation anyway; see also [6, 8]).

Lemma 6. Let MML be a multi-modal logic (note that we view temporal logics as multi-modal logics), let Ax_{MML} be the set of formulae which correspond to the axiomatization of MML and let Φ be some arbitrary multi-modal logic formula. Then Φ is MML-satisfiable^{8} iff ∀w⌈Φ⌉^{w} holds in every classical model satisfying Ax_{MML} ∧ R_{i}(u, u: x_{i}).

Observe that the background theory we get for the logic under consideration is relational (rather than equational as in the functional translation approach), yet there is a strict separation between the theorem to be proved and the background theory we get in addition to the translation result. This is caused by the fact that the translation of a formula will result in a set of clauses that do not contain any positive occurrence of an R-literal. This is extremely helpful for the extraction of a positive R-theory. Moreover, the semi-functional translation provides us with a syntactic means to detect the non-axiomatizability of certain accessibility relation properties (see [8]); this is not further examined in this paper, though.

Most of the steps required in our general recipe are performed now. Extraction of a theory is essentially done by the semi-functional translation: we just choose the theory which corresponds to the given axiomatization. The other steps – saturating such a theory, finding alternative theories and determining suitable inference rules – have been described in the earlier sections. We thus arrived at a stage where we can apply all this to some interesting example logics.

3 Application to Modal and Temporal Logics

Although the approach presented in this paper works for the propositional as well as for the first-order cases, the examples to follow will emphasize on propositional logics. For first-order modal or temporal logics, possible domain restrictions in the semantics have to be taken into account, too, so that we get a new translation (semi-functional) of quantifiers

\begin{aligned}⌈∀x Φ⌉^{u} & = & ∀x E(u, x) ⇒ ⌈Φ⌉^{u} \\ ⌈∃x Φ⌉^{u} & = & ∃y_{E} ⌈Φ_{u: y_{E}}^{x}⌉^{u} \end{aligned}

where E denotes the “existence”-predicate between worlds and domain elements^{9}. For instance, the case of decreasing domains (Barcan formula ∀x□Φ ⇒ □∀xΦ)

8 In a resolution calculus we actually show the unsatisfiability of ∃w⌈¬Φ⌉^{w} which gets

skolemized to ⌈¬Φ⌉^{o}. 9 In the semi-functional translation there is also a functional decomposition F_{E} of E.

The y_{E} in the translation of existential quantifiers ranges over F_{E}. Notice that, just as in case of the accessibility relations, we have to add the unit clause E(u, u: x_{E}) then.

is then represented by ∀u, v, x R(u, v) ∧ E(v, x) ⇒ R(u, x). Evidently, we may proceed with the E-predicate just as we did with the respective R-predicates, i.e., we can extract a positive E-theory and determine suitable inference rules for its saturation. We shall not go into further details on this here; the interested reader is referred to [5].

3.1 The Modal Logic S4

As a simple starting example let us consider the propositional modal logic S4 which is axiomatized by

\begin{matrix}□Φ ⇒ Φ \\ □Φ ⇒ □□Φ \end{matrix}

in addition to the standard K-axiom, necessitation rule and propositional (firstorder) Hilbert-axiomatization. The corresponding background theory then consists of

R(u, u)
R(u, u: x)
R(u, v) ∧ R(v, w) ⇒ R(u, w)

Now, saturating this background theory results in all unit clauses of the form

R(u, u: x_{1} : x_{2} : ⋯: x_{n})

(with n ≥ 0), or, in a more readable representation:

R(u, u: \overline{x})

where \overline{x} denotes an arbitrary sequence of functional decomposition variables. Quite evidently, we may take the clause set

\begin{matrix}R(u, u) \\ R(u, v) ⇒ R(u, v: x) \end{matrix}

as an alternative background theory which indeed is simpler than the original one. Also, it is not very hard to imagine a suitable inference rule which covers the responsibilities of the (alternative) background theory:

Definition 7. The following rule of inference together with the standard resolution calculus and the semi-functional translation is called the S4 Inference System.

\frac{¬R(α, β: γ) ∨ C}{σC}

where σ denotes the most general unifier of α and β and the term β: γ is meant to represent that the right-hand argument of this R-literal consists of a prefix β and a suffix γ^{10}.

10 This notation is mainly used for better readability. Formally, β denotes a world and γ a finite “sequence” γ_{1} : ⋯: γ_{n} of elements taken from the functional decomposition of the accessibility relation. β and γ therefore are of different sorts, actually.

Lemma 8. The S4 Inference System is sound and refutation complete.

Proof. Soundness follows immediately from the fact that any application of the new inference rule corresponds to a resolution step with an element of the saturation of S4’s background theory.

For the completeness proof first note that it suffices to show that any single S4-unsatisfiable pure-R-negative clause can be refuted (such a clause can always be derived already with the standard resolution calculus). Also note that in the ground case refutation completeness is ensured simply because there is a one-to-one correspondence between S4 Inference Rule applications and resolution steps with S4’s background theory then. There is a problem, however, and that with the lifting to the non-ground level. To illustrate this, let us consider the following example: Let C = ¬R(o, u) ∨ ¬R(o, u: f(u)) and let σC = ¬R(o, o: a) ∨ ¬R(o, o: a: f(o: a)) be a corresponding unsatisfiable ground instance of C. Then σC can very easily be refuted but neither of the two possible inference steps on σC can be lifted to C. The problem is that the variable u is overestimated by σ, i.e., a prefix of σ(u) would have sufficed as a suitable ground instance of u. And indeed, if we choose σ′(u) = o instead we would obtain the ground instance σ′C = ¬R(o, o) ∨ ¬R(o, o: f(o)) and either step can be lifted. Formally: Given an S4-unsatisfiable set of clauses C we define an ordering ≤_{C} on ground substitutions by: σ ≤_{C} λ iff σ(u) is a prefix of λ(u) for each world variable u in C and σ <_{C} λ iff σ ≤_{C} λ and σ ≠ λ. A ground instance σC is called minimally S4-unsatisfiable with respect to C if there is no λ with λ <_{C} σ and λC is S4-unsatisfiable. We may always assume that the ground substitution we have at hand is minimal in this sense. Now let C be an S4-unsatisfiable pure-R-negative clause and let σC be minimally S4-unsatisfiable. What we know is that the S4 Inference Rule can be applied to every literal of σC. What we want to show is that there is a sequence of such S4 Inference Rule applications on σC which can be lifted. To this end it suffices to show that there is at least one literal in σC which can be processed this way. Assume otherwise. Then no step on the ground level can be lifted and this means that each literal of C must be of the form ¬R(α_{i}, u_{i}: β_{i}) with σ(u_{i}) is a proper prefix of σ(α_{i}). Now suppose that each such u_{i} also occurs in one of the α_{j}. Then we can find for each u_{i} a variable u_{i+1} where σ(u_{i}) is a proper subterm of σ(u_{i+1}). But this is impossible. Hence, at least one of the variables u_{i} occurs only on right-hand arguments of the R-literals in C. However, since σC is minimal, u_{i} cannot be overestimated in all of its occurrences which contradicts the fact that σ(u_{i}) is a proper prefix of σ(α_{i}). It is thus not possible that for no literal of σC the S4 Inference Rule application can be lifted and we are done.

Example 2. Prove: ◇□◇□P ⇒ ◇□P, i.e., refute ◇□◇□P ∧ □◇¬P

¬R(o: a, u) ∨ ¬R(u: f(u), v) ∨ P (v)
¬R(o, w) ∨ ¬P (w: g(w))
¬R(o: a, u) ∨ ¬R(u: f(u), w: g(w)) ∨ ¬R(o, w)

and the final clause can easily be refuted with the help of the S4 Inference Rule by σ = {(u, o: a), (w, o: a: f(o: a))}

Evidently, the above example could easily be solved by the functional translation approach and that even in a single step involving some special kind of (S4) theory unification. As a matter of fact, in case we are only interested in modal logics which have a Horn background theory^{11} (as it is the case for S4), it might very well be questionable whether the above inference system is to be preferred over the pure functional translation approach^{12}. However, if the background theory is not in Horn form (and this is the case for all linear temporal logics) there is no chance to find suitable unification algorithms, unless we are prepared to introduce equations as residues of a unification process. This, however, would jeopardize the whole technique, for the main reason to introduce theory unification algorithms was to avoid such equations in the clause set. The above development of the S4 Inference Rule should thus be viewed as an exemplification for the whole idea rather than as an “enhancement” of the functional translation idea. In later application examples we shall consider more complicated logics for which complete theory unification algorithms (in a functional translation approach) cannot exists.

3.2 Exploiting the Generated Model Assumption

A multi-modal frame (W, R_{i}) is called generated from world o if for every w ∈ W we know that the pair (o, w) lies in the reflexive and transitive closure of ⋃_{i} R_{i}. The generated model assumption states that for a (multi-)modal (temporal) interpretation which is based on a frame (W, R_{i}) and initial world (instant) o, this very frame is generated from o.

Viewed from the semi-functional translation perspective, this can be reformulated as: For every w ∈ W there exist some x_{1}, …, x_{k} such that w = o: x_{1} : ⋯: x_{k}, or, in vector notation: For every w ∈ W there exists a (possibly empty) \overline{x}, i.e., a sequence of functional decomposition variables such that w = o: \overline{x}.

The generated model assumption can often be used to simplify the saturation of a given background theory (see [6]). For example, saturating the background theories of the modal logics S5 and KD45 after semi-functional translation results in all unit clauses of the form R(u: \overline{x}, u: \overline{y}), where in case of KD45 the sequence \overline{y} is non-empty. Now, given the generated model assumption, these units can be simplified (essentially by paramodulation steps) to R(u, v) for S5 and R(u, v: x) for KD45. Evidently, it is of no use to define inference rules which take over the responsibilities of such simple background theories. These unit clauses should in fact be directly incorporated into the translation. Usually, however, the generated model assumption does not lead to such more

11 I.e., all the formulae in the theory are Horn formulae. 12 Viewed from this perspective, the above S4 Inference Rule essentially acts as a “lazy

S4 theory unifier”.

or less trivial alternative theories. Nevertheless, it still can often be used to significantly simplify the given background theory. As an example consider

R(u, u)
R(u, u: x)
R(u, v) ∧ R(v, w) ⇒ R(u, w)
R(u, v) ∧ R(u, w) ⇒ R(v, w) ∨ R(w, v)

which we get from the axiomatization of the modal logic S4.3. From this theory it is possible to show that all clauses of the form

R(u: \overline{x}, u: \overline{y}) ∨ R(u: \overline{y}, u: \overline{x})

are derivable. Under the generated model assumption this can be simplified to

R(u, v) ∨ R(v, u)

i.e., we may replace right-linearity by general linearity. From this even another alternative theory can be found in

R(u, u)
R(u, v) ⇒ R(u, v: x)
R(u, v) ⇒ R(w, v) ∨ R(u, w)

which is definitely to be preferred over the original theory.

However, we are interested in suitable inference rules which are supposed to replace the whole theory. Again, these can be “extracted” from the saturation of the background theory which consists of all clauses of the form

R(u_{1}, u_{2} : \overline{x_{2}}) ∨ R(u_{2}, u_{3} : \overline{x_{3}}) ∨ … ∨ R(u_{n}, u_{1} : \overline{x_{1}})

(proof by induction on n). This immediately leads to the following:

Definition 9. The S4.3 Inference System (under semi-functional translation) consists of the S4 Inference System together with the S4.3 Inference Rule

¬R(α, β_{1} : β_{2}) ∨ C_{1}
¬R(γ, δ) ∨ C_{2}
¬R(σα, σδ) ∨ σC_{1} ∨ σC_{2}

where σ is the most general unifier of γ and β_{1}.

Lemma 10. The S4.3 Inference System is sound and refutation complete.

Proof. Every step with one of the new rules cooresponds to a special sequence of resolution steps with the background theory, whence the inference system is sound. For the refutation completeness it again suffices to show that any derivable set of pure-R-negative clauses that is inconsistent with the S4.3 background theory can be refuted. This works in full analogy to the corresponding proof for the S4 Inference System (for details see [8]).

Example 3. As a little example consider the modal formulae

\begin{matrix}◇(◇P ∧ □¬Q) \\ ◇(◇Q ∧ □¬P) \end{matrix}

whose combination is S4.3–unsatisfiable. This translates into P (o: a: b)

¬R(o: a, u) ∨ ¬Q(u)
Q(o: c: d)
¬R(o: c, v) ∨ ¬P (v)

After performing the standard resolution steps we end up with

\begin{matrix}¬R(o: a, o: c: d) \\ ¬R(o: c, o: a: b) \end{matrix}

from which we obtain ¬R(o: a, o: a: b) by the S4.3 Inference Rule. The empty clause gets finally derived by an application of the S4 Inference Rule.

3.3 A Simple Linear Temporal Logic

Now let us consider the simple linear temporal logic K_{t}T 4.3 which is obtained by combining two S4.3 fragments, one for the future and one for the past.

Φ ⇒ □^{F} _{r}◇^{P}_{r} Φ
□^{F} _{r}Φ ⇒ Φ
□^{F} _{r}Φ ⇒ □^{F} _{r}□^{F} _{r}Φ
◇^{P}_{r} ◇^{F}_{r} Φ ⇒ ◇^{P}_{r} Φ ∨ ◇^{F}_{r} Φ

Φ ⇒ □^{P} _{r}◇^{F}_{r} Φ
□^{P} _{r}Φ ⇒ Φ
□^{P} _{r}Φ ⇒ □^{P} _{r}□^{P} _{r}Φ
◇^{F}_{r} ◇^{P}_{r} Φ ⇒ ◇^{P}_{r} Φ ∨ ◇^{F}_{r} Φ

These axioms correspond to the following background theory^{13}:

R(u, u)
R(u, u: x_{F})
R(u: x_{P} , u)
R(u, v) ∧ R(v, w) ⇒ R(u, w)
R(u, v) ∧ R(u, w) ⇒ R(v, w) ∨ R(w, v)
R(v, u) ∧ R(w, u) ⇒ R(v, w) ∨ R(w, v)

The generated model assumption then allows us to replace left- and rightlinearity by general linearity so that we finally end up with the following theory:

R(u, u)
R(u, u: x_{F})
R(u: x_{P} , u)
R(u, v) ∧ R(u, w) ⇒ R(v, w)
R(u, v) ∨ R(v, u)

Following our general recipe we are now about to extract a suitable inference rule for this temporal logic. To this end we again derive the saturation of its background theory and determine the rule from this saturation.

13 Some equivalence-preserving simplifications, e.g., writing R for R_{F} and translating “past-formulae” accordingly, are already performed.

Lemma 11. The saturation of the background theory for K_{t}T 4.3 consists of all clauses of the form

R(u_{1} : \overline{x_{1}}, u_{2} : \overline{y_{2}}) ∨ R(u_{2} : \overline{x_{2}}, u_{3} : \overline{y_{3}}) ∨ … ∨ R(u_{n}: \overline{x_{n}}, u_{1} : \overline{y_{1}})

where the \overline{x_{i}} (\overline{y_{i}}) denote sequences of variables of the functional decomposition for R_{P} (R_{F} respectively).

The alternative theory and its saturation are very similar to the ones for the modal logic S4.3. It is thus not surprising that the inference rule we determine for this temporal logic is very similar as well.

Definition 12. The Inference System for K_{t}T 4.3 (under semi-functional translation) consists of the classical resolution calculus together with

\begin{matrix}¬R(α, β_{1} : β_{2}) ∨ C_{1} \\ ¬R(γ_{1} : γ_{2}, δ) ∨ C_{2} \\ ¬R(σα, σδ) ∨ σC_{1} ∨ σC_{2} \end{matrix}  \frac{¬R(γ_{1} : γ_{2}, β_{1} : β_{2}) ∨ C}{σC}

provided β_{2} (γ_{2}) is a sequence of elements taken from the functional decomposition of R_{F} (R_{P}) and σ is the most general unifier of γ_{1} and β_{1}.

Lemma 13. The Inference System for K_{t}T 4.3 is sound and refutation complete.

Proof. In analogy to the corresponding proof for the S4.3 Inference System (for details see [8]).

3.4 Another Temporal Logic

As another temporal logic we consider T L which incorporates S4 fragments as well as KD4 fragments for both the past and the future. Its axiomatization – at least the propositional part – is then as follows (in addition to the usual K-axioms and necessitation rules):

□^{F} _{r}Φ ⇒ Φ
□^{F} _{r}Φ ⇒ □^{F} _{r}□^{F} _{r}Φ
□^{F} Φ ⇒ ◇^{F} Φ
□^{F} Φ ⇒ □^{F} □^{F} Φ
□^{F} _{r}Φ ⇔ □^{F} Φ ∧ Φ
□^{P} _{r}Φ ⇒ Φ
□^{P} _{r}Φ ⇒ □^{P} _{r}□^{P} _{r}Φ

□^{P} Φ ⇒ ◇^{P} Φ
□^{P} Φ ⇒ □^{P} □^{P} Φ
□^{P} _{r}Φ ⇔ □^{P} Φ ∧ Φ
Φ ⇒ □^{F} _{r}◇^{P}_{r} Φ
Φ ⇒ □^{F} ◇^{P} Φ
Φ ⇒ □^{P} _{r}◇^{F}_{r} Φ
Φ ⇒ □^{P} ◇^{F} Φ

From this we get (after some simplifications) the following background theory^{14}:

\begin{matrix}R^{∗}(u, u) \\ R^{∗}(u, u: x_{F}^{∗}) \\ R^{∗}(u: x_{P}^{∗} , u) \\ R^{∗}(u, v) ⇒ R(u, v) ∨ u = v \end{matrix}  \begin{matrix}R(u, u: x_{F}) \\ R(u: x_{P} , u) \\ R(u, v) ∧ R(v, w) ⇒ R(u, w) \\ R(u, v) ⇒ R^{∗}(u, v) \end{matrix}

14 Recall that R^{∗} denotes the reflexive (transitive) closure of R.

Its saturation then consists of

R^{∗}(u: \overline{x_{1}}, u: \overline{y_{1}})
R(u: \overline{x_{2}}, u: \overline{y_{2}})
where \overline{x_{2}} ∉ (F_{R_{P}^{∗}})^{∗} or \overline{y_{2}} ∉ (F_{R_{F}^{∗}})^{∗}
R(u: \overline{x_{3}} : \overline{x_{4}}, u: \overline{y_{3}} : \overline{y_{4}}) ∨ u: \overline{x_{3}} = u: \overline{y_{3}}
where \overline{x_{3}}, \overline{x_{4}} ∈ (F_{R_{P}^{∗}})^{∗} and \overline{y_{3}}, \overline{y_{4}} ∈ (F_{R_{F}^{∗}})^{∗}

where \overline{x_{i}} ∈ (F_{R_{P}} ∪ F_{R_{P}^{∗}})^{∗} and \overline{y_{i}} ∈ (F_{R_{F}} ∪ F_{R_{F}^{∗}})^{∗}.

Again, we can quite easily extract some suitable inference rules from this saturation, namely:

Definition 14. The inference system for T L consists of the classical resolution calculus together with the following inference rules:

\frac{¬R^{∗}(α: γ, β: δ) ∨ C}{σC}  \frac{¬R(α: γ, β: δ) ∨ C}{σC}

\frac{¬R(α: γ_{1} : γ_{2}, β: δ_{1} : δ_{2}) ∨ C}{σC ∨ σ(α: γ_{1}) = σ(β: δ_{1})}

\frac{¬R(α, u) ∨ C}{C_{α: x_{F}}^{u}}  \frac{¬R(u, α) ∨ C}{C_{α: x_{P}}^{u}}

where σ is the most general unifier of α and β and the same syntactic restrictions as in the above saturation apply.

The last two rules might require a little explanation for they seem to be not directly taken from the saturation of the background theory. In fact they are, although this is probably not very obvious at the first glance. Consider the second unit clause schema of the saturation. The syntactic restrictions require that at least either \overline{x_{2}} or \overline{y_{2}} must be non-empty. But now consider the single unsatisfiable (for this logic) unit clause ¬R(o, u). None of the above rules would help to refute this unit clause and the reason for this is that we are not able to “split” the variable u such that the second new inference rule is applicable. One solution to this problem could be to allow an arbitrary variable splitting. This, however, is much stronger than really needed. It suffices to allow only a splitting of such a variable u into u: x with an immediately following application of the second inference rule. And in fact this is just what the last two inference rules do.

Lemma 15. The inference system for T L is sound and refutation complete.

Proof. By the above observations and in analogy to the proof of Lemma 10.

4 Summary

The main steps of the approach presented in this paper can be briefly summarized as follows: Given a theory which is characteristic for some logic in the sense that it tells us all what is to be known about some distinguished predicate symbols, such a theory can be saturated and the saturation result can be used to either derive a somewhat simpler theory or some appropriate inference rules which may replace the whole theory. Usually, translation methods from modal and temporal logics into first-order predicate logic do not produce such theories. The semi-functional translation approach however does, for it guarantees that the translation of an arbitrary formula contains no positive accessibility relation literals. Hence the only positive such literals can only occur in the theory induced by the axiomatization of the logic in question and the corresponding formulae indeed are of the form required for the saturation approach. Determining the saturation and extracting alternative theories with an identical saturation, or even inference rules which cover the whole saturation, is usually not too complicated and soundness and completeness proofs are more or less straightforward.

The whole approach has been applied in [8] to various modal and temporal logics. The most complicated logic considered there takes into account all the operators mentioned at the beginning of this paper, and that regardless of whether we assume linearity or not. In fact, the resulting inference system for this logic consists of only three extra rules (in addition to the inference system for the slightly more complex temporal logic described in this paper) and the alternative background theory reduces from 13 clauses (34 literals) to 8 clauses (14 literals).

Moreover, this technique has not only been applied to point oriented temporal logics but also successfully to interval logics in the sense of [14]. In fact, it seems general enough to be applicable to any logic for which a suitable theory separation can be defined (for instance via the semi-functional translation).

A comparison with other approaches is a rather difficult task. From the translational point of view this approach is certainly closely related to the functional translation method as defined in [9, 10, 1]. It has the advantage over the functional translation that in case the accessibility relation properties are not Horn there is no need to explicitly reason within equational theories (in Horn theories an implicit reasoning is often possible by developing suitable theory unification algorithms).

A comparison with totally different formalisms, as for instance the tableau method, is even more complicated. What can be said, however, is that under linearity (without Nexts) tableau systems behave fairly cumbersome. This is mainly due to the fact that the linearity rule has to check n! (n faculty) branches if it gets or derives n ◇-formulae. Consider the set of modal formulae

◇(P_{1} ∧ □¬P_{2})
…
◇(P_{n−1} ∧ □¬P_{n})
◇(P_{n} ∧ □¬P_{1})

which is S4.3-unsatisfiable. With the tableau calculus n! branches have to be closed. In the approach presented here just n applications of the linearity rules have to be applied and we are done.

References

1. Yves Auffray and Patrice Enjalbert. Modal theorem proving: An equational viewpoint. Journal of Logic and Computation, 2(3):247 – 295, 1992.

2. Brian F. Chellas. Modal Logic, an introduction. Cambridge University Press, 1980.

3. Rajeev Goré. Cut-free Sequent and Tableau Systems for Propositional Normal Modal Logics. Technical Report 257, Computer Laboratory, University of Cambridge, Cambridge, England, May 1992.

4. G. Hughes and M. Cresswell. An Introduction to Modal Logic. Menthuen, London, 1968.

5. Erik Mohr. Resolution-based calculi for modal logics. Master’s thesis, University of Saarbrücken, Germany, 1995.

6. Andreas Nonnengart. First-order modal logic theorem proving and functional simulation. In Ruzena Bajcsy, editor, Proceedings of the 13th IJCAI, volume 1, pages 80 – 85. Morgan Kaufmann Publishers, 1993.

7. Andreas Nonnengart. How to use modalities and sorts in prolog. In Craig MacNish, David Pearce, and Luís Moniz Pereira, editors, Logics in Artificial Intelligence, volume LNAI 838, pages 365 – 378. Springer Verlag, 1994.

8. Andreas Nonnengart. A Resolution-Based Calculus for Temporal Logics. PhD thesis, Universität des Saarlandes, Saarbrücken, Germany, December 1995.

9. Hans Jürgen Ohlbach. A resolution calculus for modal logics. In Ewing Lusk and Ross Overbeek, editors, Proc. of 9^{th} International Conference on Automated Deduction, CADE-88 Argonne, IL, volume 310 of LNCS, pages 500–516, Berlin, Heidelberg, New York, 1988. Springer-Verlag. extended version: SEKI Report SR-88-08, FB Informatik, Universität Kaiserslautern, 1988.

10. Hans Jürgen Ohlbach. Semantics-based translation methods for modal logics. Journal of Logic and Computation, 1(5):691–746, 1991.

11. Arthur Prior. Past, Present and Future. Clarendon Press, Oxford, 1967.

12. N. Rescher and A. Urquhart. Temporal Logic. Springer, Berlin, 1971.

13. Krister Segerberg. An essay in classical modal logic. Technical Report 13, University of Uppsala, Filosofiska Studier, 1971. Volume 1-3.

14. Johan van Benthem. The Logic of Time. Reidel, Dordrecht, 1990.

This article was processed using the L^{A}TEX macro package with LLNCS style