The elimination of redundant clauses is an essential part of resolution-based theorem proving in order to reduce the size of the search space. In this paper we focus on ordered fine-grained resolution with selection, a sound and complete resolution-based calculus for monodic first-order temporal logic. We define a subsumption relation on temporal clauses, show how the calculus can be extended with reduction rules that eliminate redundant clauses, and we illustrate the effectiveness of redundancy elimination with some experiments.
Monodic first-order temporal logic [9] is a fragment of first-order temporal logic (without equality) which, in contrast to first-order temporal logic itself, has a semi-decidable validity and satisfiability problem. Besides semi-decidability, monodic first-order temporal logic enjoys a number of other beneficial properties, e.g. the existence of non-trivial decidable subclasses, complete reasoning procedures, etc.
In addition to a tableaux-based calculus [13] for monodic first-order temporal logic, several resolution-based calculi have been proposed for the logic, starting with (monodic) temporal resolution [3]. A more machine-oriented version, the fine-grained first-order temporal resolution calculus, was described in [12]. Subsequently, a refinement of fine-grained temporal resolution, the ordered finegrained temporal resolution with selection calculus, was presented in [10].
Essentially, the inference rules of ordered fine-grained resolution with selection can be classified into two different categories. The majority of the rules are based on standard first-order resolution between different types of temporal clauses. The remaining inference rules, the so-called eventuality resolution rules, reflect the induction principle that holds for monodic temporal logic over a flow of time isomorphic to the natural numbers. The applicability of the rules in this second category is only semi-decidable, making the construction of fair derivations, that is, derivations in which every non-redundant clause that is derivable from a given clause set is eventually derived, a non-trivial problem. A new inference procedure solving this problem has been recently been described in [15] and is implemented in the theorem prover TSPASS [14].
In this paper we focus on a different aspect of ordered fine-grained temporal resolution with selection, namely, redundancy elimination. The use of an ordering and a selection function which restricts inferences to literals which are selected or, in the absence of selected literals, to (strictly) maximal literals, already reduces the possible inferences considerably. However, it cannot prevent the derivation of redundant clauses, e.g. tautological clauses or clauses which are subsumed by other, simpler, clauses. Redundancy elimination is therefore an important ingredient for practical resolution calculi and for theorem provers based on such calculi.
The paper is organised as follows. In Section 2 we briefly recall the syntax and semantics of monodic first-order temporal logic. The ordered fine-grained resolution with selection calculus is presented in Section 3. In Sections 4 and 5 we show how redundancy elimination can be added to the calculus. Finally, in Section 6 we briefly discuss how redundancy elimination fits with our implementation of the calculus and present some experimental results which show the effectiveness of redundancy elimination. 2
We assume the reader to be familiar with first-order logic and associated notions, including, for example, terms and substitutions.
Then, the language of First-Order (Linear Time) Temporal Logic, FOTL, is an extension of classical first-order logic by temporal operators for a discrete linear model of time (i.e. isomorphic to N). The vocabulary of FOTL (without equality and function symbols) is composed of a countably infinite set X of variables x0, x1, . . . , a countably infinite set of constants c0, c1, . . . , a nonempty set of predicate symbols P , P0, . . . , each with a fixed arity ≥ 0, the propositional operators ⊤ (true), ¬, ∨, the quantifiers ∃xi and ∀xi, and the temporal operators (‘always in the future’), ♦ (‘eventually in the future’), (‘at the next moment’), U (‘until’) and W (‘weak until’) (see e.g. [7]). We also use ⊥ (false), ∧, and ⇒ as additional operators, defined using ⊤, ¬, and ∨ in the usual way. The set of FOTL formulae is defined as follows: ⊤ is a FOTL formula; if P is an n-ary predicate symbol and t1, . . . , tn are variables or constants, then P (t1, . . . , tn) is an atomic FOTL formula; if ϕ and ψ are FOTL formulae, then so are ¬ϕ, ϕ ∨ ψ, ∃xϕ, ∀xϕ, ϕ, ♦ϕ, ϕ, ϕ U ψ, and ϕ W ψ. Free and bound variables of a formula are defined in the standard way, as well as the notions of open and closed formulae. For a given formula ϕ, we write ϕ(x1, . . . , xn) to indicate that all the free variables of ϕ are among x1, . . . , xn. As usual, a literal is either an atomic formula or its negation, and a proposition is a predicate of arity 0.
Formulae of this logic are interpreted over structures M = (Dn, In)n∈N that associate with each element n of N, representing a moment in time, a first-order structure Mn = (Dn, In) with its own non-empty domain Dn and interpretation In. An assignment a is a function from the set of variables to Sn∈N Dn. The application of an assignment to formulae, predicates, constants and variables is defined in the standard way, in particular, a(c) = c for every constant c. The Mn |=a ⊤ Mn |=a P (t1, . . . , tn) iff (In(a(t1)), . . . , In(a(tn))) ∈ In(P ) Mn |=a ¬ϕ iff not Mn |=a ϕ Mn |=a ϕ ∨ ψ iff Mn |=a ϕ or Mn |=a ψ Mn |=a ∃xϕ iff Mn |=b ϕ for some assignment b that may differ from a only in x and such that b(x) ∈ Dn Mn |=a ∀xϕ iff Mn |=b ϕ for every assignment b that may differ from a only in x and such that b(x) ∈ Dn Mn |=a ϕ iff Mn+1 |=a ϕ Mn |=a ♦ϕ iff there exists m ≥ n such that Mm |=a ϕ Mn |=a ϕ iff for all m ≥ n, Mm |=a ϕ Mn |=a ϕ U ψ iff there exists m ≥ n such that Mm |=a ψ and
Mi |=a ϕ for every i, n ≤ i < m Mn |=a ϕ W ψ iff Mn |=a ϕ U ψ or Mn |=a ϕ definition of the truth relation Mn |=a ϕ (only for those a such that a(x) ∈ Dn for every variable x) is given in Fig. 1.
In this paper we make the expanding domain assumption, that is, Dn ⊆ Dm if n < m, and we assume that the interpretation of constants is rigid, that is, In(c) = Im(c) for all n, m ∈ N.
A structure M = (Dn, In)n∈N is said to be a model for a formula ϕ if and only if for every assignment a with a(x) ∈ D0 for every variable x it holds that M0 |=a ϕ. A formula is satisfiable if and only there exists a model for ϕ. A formula ϕ is valid if and only if every temporal structure M = (Dn, In)n∈N is a model for ϕ.
The set of valid formulae of this logic is not recursively enumerable. However, the set of valid monodic formulae is known to be finitely axiomatisable [19]. A formula ϕ of FOTL is called monodic if any subformula of ϕ of the form ψ, ψ, ♦ψ, ψ1 U ψ2, or ψ1 W ψ2 contains at most one free variable. For example, the formulae ∃x ∀yP (x, y) and ∀x P (c, x) are monodic, whereas the formula ∀x∃y(Q(x, y) ⇒ Q(x, y)) is not monodic.
Every monodic temporal formula can be transformed into an equi-satisfiable normal form, called divided separated normal form (DSNF) [12]. Definition 1. A monodic temporal problem P in divided separated normal form (DSNF) is a quadruple hU , I, S, E i, where the universal part U and the initial part I are finite sets of first-order formulae; the step part S is a finite set of step clauses of the form p ⇒ q, where p and q are propositions, and P (x) ⇒
Q(x), where P and Q are unary predicate symbols and x is a variable; and the eventuality part E is a finite set of formulae of the form ♦L(x) (a nonground eventuality clause) and ♦l (a ground eventuality clause), where l is a propositional literal and L(x) is a unary non-ground literal with the variable x as its only argument.
We associate with each monodic temporal problem P = hU , I, S, E i the monodic FOTL formula I∧ U ∧ ∀xS∧ ∀xE . When we talk about particular properties of a temporal problem (e.g., satisfiability, validity, logical consequences, etc) we refer to properties of this associated formula.
The transformation to DSNF is based on a renaming and unwinding technique which substitutes non-atomic subformulae by atomic formulae with new predicate symbols and replaces temporal operators by their fixed point definitions as described, for example, in [8].
Theorem 1 (see [4], Theorem 3.4). Any monodic formula in first-order temporal logic can be transformed into an equi-satisfiable monodic temporal problem in DSNF with at most a linear increase in the size of the problem.
The main purpose of the divided separated normal form is to cleanly separate different temporal aspects of a FOTL formula from each other. For the resolution calculus in this paper we will need to go one step further by transforming the universal and initial part of a monodic temporal problem into clause normal form.
Definition 2. Let P = hU , I, S, E i be a monodic temporal problem. With every eventuality ♦L(x) ∈ E and constant c occurring in P we uniquely associate a propositional symbol pcL. Then the clausification Cls(P) of P is a quadruple hU ′, I′, S′, E ′i such that U ′ is a set of clauses1, called universal clauses, consisting of the clausification of U and clauses ¬pcL ∨ L(c) for every ♦L(x) ∈ E and constant c occurring in P; I′ is a set of clauses, called initial clauses, obtained by clausification of I; S′ is the smallest set of step clauses such that all step clauses from S are in S′ and for every non-ground step clause P (x) ⇒ L(x) in S and every constant c occurring in P, the clause P (c) ⇒ L(c) is in S′; E ′ is the smallest set of eventuality clauses such that all eventuality clauses from E are in E ′ and for every non-ground eventuality clause ♦L(x) in E and every constant c occurring in P, the eventuality clause ♦pcL is in E ′.
One has to note that new constants and, especially, function symbols of an arbitrary arity can be introduced during the Skolemization process. As a consequence it is not possible in general to instantiate every variable that occurs in the original problem with all the constants and function symbols. On the other hand, the variables occurring in the step and eventuality clauses have to be instantiated with the constants that are present in the original problem (before Skolemization) in order to ensure the completeness of the calculus presented in Section 3.
Note further that more general step clauses with more than one atom on the left-hand side and more than one literal on the right-hand side can be derived by the calculus introduced in Section 3. In what follows U denotes the (current) universal part of a monodic temporal problem P. 3
We assume that we are given an atom ordering ≻, that is, a strict partial ordering on ground atoms which is well-founded and total, and a selection function S 1 Clauses, as well as disjunctions and conjunctions, will be considered as multisets. which maps any first-order clause C to a (possibly empty) subset of its negative literals and which is instance compatible: Definition 3. We say that a selection function S is instance compatible if and only if for every clause C, for every substitution σ and for every literal l ∈ Cσ it holds that ∈ S(Cσ) iff there exists a literal l′ ∈ S(C) such that l′σ = l.
The atom ordering ≻ is extended to ground literals by ¬A ≻ A and (¬)A ≻ (¬)B if and only if A ≻ B. The ordering is extended on the non-ground level as follows: for two arbitrary literals L and L′, L ≻ L′ if and only if Lσ ≻ L σ for ′ every grounding substitution σ. A literal L is called (strictly) maximal w.r.t. a clause C if and only if there is no literal L′ ∈ C with L′ ≻ L (L′ L). A literal L is eligible in a clause L ∨ C for a substitution σ if either it is selected in L ∨ C, or otherwise no literal is selected in C and Lσ is maximal w.r.t. Cσ.
The atom ordering ≻ and the selection function S are used to restrict the
applicability of the deduction rules of fine-grained resolution as follows.
(
(C1 ∨ C2)σ
if σ is a most general unifier of the atoms A and B, A is eligible in (C1 ∨ A)
for σ, and ¬B is eligible in (¬B ∨ C2) for σ. The result is a universal clause.
(
C1 ∨ A ∨ B
(C1 ∨ A)σ
if σ is a most general unifier of the atoms A and B, and A is eligible in
(C1 ∨ A ∨ B) for σ. The result is again a universal clause.
(
C1 ⇒ (D1 ∨ A) C2 ⇒ (D2 ∨ ¬B) (C1 ∧ C2)σ ⇒ (D1 ∨ D2)σ where C1 ⇒ (D1 ∨ A) and C2 ⇒ (D2 ∨ ¬B) are step clauses, σ is a most general unifier of the atoms A and B such that σ does not map variables from C1 or C2 into a constant or a functional term, A is eligible in (D1 ∨ A) for σ, and ¬B is eligible in (D2 ∨ ¬B) for σ.
C1 ⇒ (D1 ∨ A) D2 ∨ ¬B
C1σ ⇒
(D1 ∨ D2)σ
where C1 ⇒ (D1 ∨ A) is a step clause, D2 ∨ ¬B is a universal clause,
and σ is a most general unifier of the atoms A and B such that σ does not
map variables from C1 into a constant or a functional term, A is eligible in
(D1 ∨ A) for σ, and ¬B is eligible in (D2 ∨ ¬B) for σ. There also exists an
analogous rule where the positive literal A is contained in a universal clause
and the negative literal ¬B in a step clause.
(
C ⇒ (D ∨ A ∨ B)
Cσ ⇒ (D ∨ A)σ
where σ is a most general unifier of the atoms A and B such that σ does not
map variables from C into a constant or a functional term, and A is eligible
in (D ∨ A ∨ B) for σ.
(
Step clauses of the form C ⇒ ⊥ will also be called terminating or final
step clauses.
(
A clause of the form (C ∧ A ∧ A) ⇒ ⊥ yields the clause (C ∧ A) ⇒ ⊥.
(
n ∀x Vi=1 ¬Ai(x) (♦rUes ) , where ∀x(Ai(x) ⇒ Bi(x)) are formulae computed from the set of step clauses such that for every i, 1 ≤ i ≤ n, the loop side conditions ∀x(U ∧ n Bi(x) ⇒ ¬L(x)) and ∀x(U ∧ Bi(x) ⇒ Wj=1(Aj (x))) are valid.2 The set of full merged step clauses, satisfying the loop side conditions, is n called a loop in ♦L(x) and the formula Wj=1 Aj (x) is called a loop formula.
More details can be found in [10].
(
A1 ⇒ B1 · · · An ⇒ Bn ♦l
n (♦rUes ) ,
Vi=1 ¬Ai where Ai ⇒ Bi are ground formulae computed from the set of step clauses such that for every i, 1 ≤ i ≤ n, the loop side conditions U ∧ Bi |= ¬l and n U ∧ Bi |= Wj=1 Aj are valid. The notions of ground loop and ground loop formula are defined similarly to the case above.
Rules (
Loop formulae, which are required for applications of the rules (
Output: A loop formula H(x) with at most one free variable.
Method: (
Otherwise let Mi+1 = {Cj ⇒ ⊥}jn=1 be the set of all new
terminating step clauses in the saturation of Ni+1.
(
(
Note: The constant cl is a fresh constant used for loop search only Fig. 2. Breadth-First Search Algorithm Using Fine-Grained Step Resolution.
Let ordered fine-grained resolution with selection be the calculus consisting of
the rules (
Definition 4 (Derivation). A (linear) derivation Δ (in IFSG,≻) from the clausification Cls(P) = hU1, I1, S1, E i of a monodic temporal problem P is a sequence of tuples Δ = hU1, I1, S1, E i, hU2, I2, S2, E i, . . . such that each tuple at an index i + 1 is obtained from the tuple at the index i by adding the conclusion of an application of one of the inference rules of IFSG,≻ to premises from one of the sets Ui, Ii, Si to that set, with the other sets as well as E remaining unchanged3.
A derivation Δ such that the empty clause is an element of a Ui ∪ Ii is called a (IFSG,≻-)refutation of hU1, I1, S1, E i.
A derivation Δ is fair if and only if for each clause C which can be derived from premises in hSi≥1 Ui, Si≥1 Ii, Si≥1 Si, E i there exists an index j such that C occurs in hUj , Ij , Sj , E i.
Ordered fine-grained resolution with selection is sound and complete for constant flooded monodic temporal problems over expanding domains as stated in the following theorem.
Theorem 2 (see [10], Theorem 5). Let P be a monodic temporal problem.
Let ≻ be an atom ordering and S an instance compatible selection function.
Then P is unsatisfiable iff there exists a IFSG,≻-refutation of Cls(P). Moreover, P
is unsatisfiable iff any fair IFSG,≻-derivation is a refutation of Cls(P).
3 In an application of ground eventuality or eventuality resolution rule, the set U in
the definition of the rule refers to Ui.
To prove Theorem 2, we show that any refutation of a temporal problem by the
Ie calculus of [12] there is a corresponding refutation by IFSG,≻. Rule (
Given that our calculus uses an ordering refinement, it seems natural to establish that the calculus admits redundancy elimination by using the approach in [1, Section 4.2]. To do so, we would first need to define a model functor I that maps any (not necessarily satisfiable) temporal problem P not containing the empty clause to an interpretation MP and then show that IFSG,≻ has the reduction property for counterexamples with respect to the model functor I and the ordering ≻, that is, for every temporal problem P and minimal clause C in P which is false in MP, there exists an inference with (main) premise C and conclusion D that is also false in P but smaller than C wrt. ≻. We could then define a clause C to be redundant wrt. P if there exists clauses C1, . . . , Ck in P such that C1, . . . , Ck |= C and C ≻ Ci for all i, 1 ≤ i ≤ k, and it would be straightforward to show that IFSG,≻ remains complete if redundant clauses are eliminated from derivations.
However, due to the presence of eventualities in temporal problems, defining an appropriate model functor is a non-trivial and open problem. For example, consider the satisfiable propositional temporal problem P = h{p ∨ q}, ∅, {p ⇒ ¬l}, {♦l}i and an ordering ≻ such that p ≻ q. Applying the standard model functor defined in [1] to the clause p ∨ q results in a model in which p is true. Given that p ∨ q is a universal clause, it would be natural to define MP in such way that p is true at every moment of time. However, due to the step clause p ⇒ ¬l, ♦l is not true in MP which means that MP is not a model of P. Thus, this simplistic approach to defining a model functor is not correct for temporal problems containing eventualities.
We have recently introduced a model functor I for propositional temporal problems [16], which is able to associate a model M of P with every satisfiable temporal problem P, but IFSG,≻ is not reductive wrt. I. Thus, this model functor is not suitable for establishing that IFSG,≻ admits redundancy elimination.
Thus, we have to follow a different approach in order to show how ordered fine-grained resolution with selection can be extended with redundancy elimination rules. In the following we will define the notions of a tautological clause and of a subsumed clause. In order to show that IFSG,≻ is still complete if such clauses are eliminated during a derivation, we need to show that for every refutation without redundancy elimination there exists a refutation with redundancy elimination. It turns out that in order to be able to do so, we need to add two inference rules to our calculus and impose a restriction on the selection function.
First of all, we consider tautological clauses. As a tautological clause is defined to be a clause that is true in every structure M = (Dn, In)n∈N, we obtain the following lemma: Lemma 1. Let C be a initial, universal or step clause. Then: (i) If C is an initial or universal clause, then C is a tautology iff C = ¬L∨L∨C′, for some possibly empty disjunction of literals C′. (ii) If C = C1 ⇒ C2 is a step clause, then C is a tautology iff C2 = ¬L∨L∨C2′, for some possibly empty disjunction of literals C2′.
It has be noted that for point (ii) of the lemma above C1 is assumed to be true or a non-empty conjunction of atoms.
Thus, just as in the non-temporal first-order case, there is again a syntactic criterion for characterising tautologies, namely the presence of complementary literals. For a set of clauses N (or a temporal problem) we denote by taut(N ) the set of all the tautological clauses contained in the set N .
The subsumption relation on initial, universal and step clauses is now defined as follows.
Definition 5. We define a subsumption relation ≤s on initial, universal and step clauses as follows: (i) For two initial clauses C and D, two universal clauses C and D, or a universal clause C and an initial clause D we define
C ≤s D iff there exists a substitution σ with Cσ ⊆ D. (ii) For two step clauses C = C1 ⇒ C2 and D = D1 ⇒ D2 we define C ≤s D iff there exists a substitution σ with C1σ ⊆ D1, C2σ ⊆ D2 and for every x ∈ var (C1) ∩ var (C2) : σ(x) ∈ X. (iii) For a universal clause C and a step clause D = D1 ⇒ D2 we define
C ≤s D iff there exists a substitution σ with Cσ ⊆ ¬D1 or Cσ ⊆ D2. By N ≤s N ′ we denote that all clauses in N ′ are subsumed by clauses in N . Thus, subsumption between two initial, two universal or an initial and a universal clause is defined analogously to the subsumption on regular first-order clauses. However, we can only allow a universal clause to subsume a initial clause, but not conversely, as an initial clause only holds in the initial moment of time while a universal clause is true at every moment of time. We also allow subsumption between a universal and a step clause if and only if the universal either subsumes the negated left-hand side or the right-hand side of the step clause.
For subsumption between two step clauses C1 ⇒ C2 and D1 ⇒ D2,
we have to impose an additional constraint on the substitution that is used for
multiset inclusion: in analogy to inference rules (
To see that, consider a temporal problem P with universal clauses P (x) and
¬Q(c) and a step clause P (x) ⇒ Q(x). The clausification of P will then also
contain a step clause P (c) ⇒ Q(c). This additional step clause can be
resolved with ¬Q(c) using rule (
Lemma 2. Let C and D be initial, step or universal clauses such that C ≤s D. Then it holds for an initial clause D that the formula [( )∀˜C] ⇒ [∀˜D] is valid, and for a step or universal clause D that the formula [ ∀˜C] ⇒ [ ∀˜D] is valid, where ∀˜C denotes the universal closure of C.
Having defined criteria for identifying tautological and subsumed clauses, we could now try to prove that for every refutation without redundancy elimination there exists a refutation with redundancy elimination. However, it turns out that such a correspondence is difficult to establish if the refutation contains applications of the duplicate literal elimination rule whose premise is subsumed.
For example, consider the step clause D1 = P (x) ∧ P (x) ⇒ ⊥ which is subsumed by C1 = P (x)∧P (y) ⇒ ⊥. From D1 we can derive D2 = P (x) ⇒ ⊥ using the duplicate literal elimination rule. But our calculus does not contain a rule which allows us to derive a clause C2 from C1 that subsumes D2 nor does C1 itself subsume D2. Similarly, the universal clause C3 = ¬P (x) ∨ ¬P (y) would also subsume C1. But again, C3 does not subsume D2 nor can we derive a clause from C3 which subsumes D2 using the rules of our calculus.
In order to deal with these two cases we need additional factoring rules, in particular, we need to extend our calculus by the following two rules: – (Arbitrary) Factoring in left-hand sides of terminating step clauses: C ∧ A ∧ B ⇒ (C ∧ A)σ ⇒ ⊥ , ⊥ where σ is a most general unifier of the atoms A and B. – (Arbitrary) Factoring in (at most) monadic negative universal clauses: ¬A1 ∨ · · · ∨ ¬An ∨ ¬An+1 ,
(¬A1 ∨ · · · ∨ ¬An)σ where every atom A1, . . . , An+1 contains at most one free variable and σ is a most general unifier of the atoms An and An+1. The calculus ordered fine-grained resolution with selection extended by the two rules introduced above will be called subsumption complete ordered fine-grained resolution with selection and will be denoted by IFSG,≻,Sub .
Finally, for our completeness proof we also need to require that the selection function is subsumption compatible, as defined below.
Definition 7. We say that a selection function S is subsumption compatible if and only if for every substitution σ and for every two clauses C, D with Cσ ⊆ D it holds for every literal l ∈ D that l ∈ S(D) iff lσ ∈ S(C) We now have everything in place to show that subsumption complete ordered fine-grained resolution with selection allows the elimination of tautological and subsumed clauses.
Lemma 3. Let C1, C2 be initial, universal or step clauses such that C1 is a tautology. Then it holds that every resolvent C of C1 and C2 is either a tautology or subsumed by C2.
Lemma 4. Let C1 be a tautology. Then it holds that every factor C of C1 is a tautology.
Lemma 5. Let U be a set of universal clauses and let N , N˜ be sets of step clauses such that N ≤s N˜ . Additionally, let Δ˜ be a derivation of a step clause C˜ by subsumption complete ordered fine-grained resolution with selection without the clause conversion rule from clauses in U ∪ N˜ .
Then there exists a derivation Δ of a step clause C by subsumption complete ordered fine-grained resolution with selection from clauses in U ∪ N such that C ≤s C˜.
Proof. Lemma 5 is shown by induction on the length of the derivation Δ˜. For
the base case we assume that C˜ is a step clause in N˜ . Then there is a clause C
in N with C ≤s C˜. For the induction step we consider a step clause C˜ that is
derived by one of the rules of fine-grained step resolution excluding the clause
conversion rule, that is, rules (
Lemma 6. Let N and N˜ be sets of initial, universal clauses or step clauses such that N ≤s N˜ . Additionally, let Δ˜ be a derivation of a clause C˜ by subsumption complete ordered fine-grained resolution with selection from clauses in N˜ .
Then there exists a derivation Δ of a clause C by subsumption complete ordered fine-grained resolution with selection from clauses in N such that C ≤s C˜.
The previous statement still holds if N ≤s N˜ \ taut(N˜ ) and C˜ is not a tautology. Function Subsumption-Restricted-FG-BFS Input: A set of universal clauses U and a set of step clauses S, saturated by ordered fine-grained resolution with selection, and an eventuality clause ♦L(x) ∈ E .
Output: A formula R(x) with at most one free variable.
Method: (
′ n
(
(
Fig. 3. Restricted Breadth-First Search Using Ordered Fine-Grained Step Resolution with Selection Proof. Let Δ˜ = D˜1, . . . , D˜n−1, C˜(= D˜n). If N ≤s N˜ , then one can show the existence of the derivation Δ by induction on the length of the derivation Δ˜ in analogy to Lemma 5.
In the case where N ≤s N˜ \ taut(N˜ ) holds, it can be shown inductively for every clause D˜i (1 ≤ i ≤ n) which is not a tautology that there exists a ˜ derivation Δ of a clause Di with Di ≤s Di by subsumption complete ordered fine-grained resolution with selection from clauses in N .
Theorem 3. Let P be the clausification of a monodic temporal problem. Let ≻ be an atom ordering and S a subsumption compatible selection function. Then P is unsatisfiable iff there exists a IFSG,≻,Sub -refutation of Cls(P). Moreover, P is unsatisfiable iff any fair IFSG,≻,Sub-derivation is a refutation of Cls(P). Proof. Given a IFSG,≻-refutation Δ of P we establish by induction on Δ that there also exists a IFSG,≻,Sub -refutation of P using Lemmata 3 to 6. 5
Theorem 3 shows that we can eliminate tautologies and subsumed clauses during the construction of a derivation at the level of inference rule applications of the IFSG,≻,Sub calculus. However, the rules of the calculus are also applied within the fine-grained breadth-first search algorithm FG-BFS which is used to find loop formulae for the application of the eventuality resolution rules. Naturally, the question arises whether tautological and subsumed clauses can also be eliminated within FG-BFS.
The answer to that is positive. Figure 3 shows the so-called subsumption
restricted breadth-first search algorithm using ordered fine-grained step resolution
with selection, a modification of FG-BFS which removes tautological and
subsumed clauses during the saturation process by ordered fine-grained resolution
with selection in step (
We are then able to prove the following result: Theorem 4. Let P be a monodic temporal problem. Let ≻ be an atom ordering and S a subsumption compatible selection function. Then P is unsatisfiable iff there exists a IFSG,≻,Sub-refutation of Cls(P) with applications of the eventuality resolution rule restricted to loop formulae found by the function SubsumptionRestricted-FG-BFS. Moreover, P is unsatisfiable iff any fair IFSG,≻,Sub-derivation with applications of the eventuality resolution rule restricted to loop formulae found by the function Subsumption-Restricted-FG-BFS is a refutation of Cls(P). 6
The subsumption complete ordered fine-grained resolution calculus including the restricted breath-first loop search procedure have been implemented in the theorem prover TSPASS 4, which is based on the first-order resolution prover SPASS 3.0. In order to be able to construct fair derivations, the loop search procedure has been integrated with the remainder of the calculus as described in [14, 15].
The main procedure of TSPASS uses a given-clause algorithm [18] in which a clause selected from the set U S of usable clauses, which initially contains all clauses from a given temporal problem, is used to derive all consequences N EW by resolving the selected clause with all the clauses in the set WO of worked-off clauses, which is initially empty, after the selected clause has been moved from U S to WO. Based on the results in the previous two sections, we can apply tautology elimination (to N EW), forward subsumption and backward subsumption [18]. With forward subsumption all clauses in N EW that are subsumed by a clause in WO or U S are deleted from N EW. With backward subsumption clauses in WO and U S subsumed by a clause in N EW are deleted from these sets. After redundancy elimination the remaining clauses in N EW are added to U S. This process continues until either a contradiction is derived or U S becomes empty.
To show the effectiveness of tautology elimination, forward subsumption, and backward subsumption for the subsumption complete ordered fine-grained resolution calculus, we have applied TSPASS 0.92-0.16, for example, on the specification of the game Cluedo [2]. Due to lack of space we cannot present other examples, but we obtained similar results. The Cluedo problem specifications 4 Available at http://www.csc.liv.ac.uk/~michel/software/tspass/ 1 2 3 4 5 6 1 2 3 4 5 6 consist of six valid, i.e. unsatisfiable, assertions that can be made in an example Cluedo game. The full details can be found in [5, 6]. Problem 4 is the only specification that contains eventuality formulae.
The experiments were run on a PC with an Intel Core 2 Duo E6400 CPU and 2 GB of main memory with a timeout (TO) of 1 CPU hour for each problem. The results are shown in Table 1. Here, ‘+B’, ‘+F’, and ‘+T’ indicate that backward subsumption, forward subsumption, and tautology elimination, respectively, have been enabled while ‘-B’, ‘-F’, and ‘-T’ indicate that they have been disabled. Given that all six assertions are valid, proofs can theoretically be found by a complete reasoner without the need for redundancy elimination. As the experiments indicate this is clearly not the case within a reasonable amount of time. On the other hand with all options for redundancy elimination enabled even the most difficult problem can be solved in little more than one second. As one might expect, forward subsumption is the most effective of the three options, followed by tautology elimination, while backward subsumption can on occasion slow down the process of finding a proof rather than speeding it up. Overall, the experiments confirm that redundancy elimination is crucial for effective resolution-based theorem proving in monodic first-order temporal logic. 7
In this paper we have considered redundancy elimination in the context of ordered fine-grained resolution with selection, a sound and complete resolutionbased calculus for monodic first-order temporal logic. We have shown that a slight modification of the calculus is compatible with the elimination of tautologies and subsumed clauses.
Our results can be used to show that the calculus can also be extended with additional rules, for example, condensation and matching replacement resolution [18] with suitable restrictions on the substitutions and on the orderings of the literals that are to be removed, which reduce to a sequence of inference and redundancy elimination steps. Such rules can be useful to further increase the effectiveness of the calculus and for the construction of decision procedures for decidable fragments of monodic first-order temporal logic [10].
In addition, we have presented experimental results which confirm that the elimination of redundant clauses is essential for effective resolution-based theorem proving in monodic first-order temporal logic.