=Paper=
{{Paper
|id=Vol-556/paper-6
|storemode=property
|title=Redundancy Elimination in Monodic Temporal Reasoning
|pdfUrl=https://ceur-ws.org/Vol-556/paper05.pdf
|volume=Vol-556
|dblpUrl=https://dblp.org/rec/conf/ftp/LudwigH09
}}
==Redundancy Elimination in Monodic Temporal Reasoning==
<pdf width="1500px">https://ceur-ws.org/Vol-556/paper05.pdf</pdf>
<pre>
 Redundancy Elimination in Monodic Temporal
                 Reasoning

                      Michel Ludwig1 and Ullrich Hustadt1

    Department of Computer Science, University of Liverpool, United Kingdom
                {Michel.Ludwig,U.Hustadt}@liverpool.ac.uk


      Abstract. 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.


1   Introduction
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 proper-
ties, 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 tempo-
ral logic, several resolution-based calculi have been proposed for the logic, start-
ing 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 fine-
grained temporal resolution with selection calculus, was presented in [10].
    Essentially, the inference rules of ordered fine-grained resolution with selec-
tion 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 deriva-
tions, 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 in-
ference 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

                                         34
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 imple-
mentation of the calculus and present some experimental results which show the
effectiveness of redundancy elimination.


2    First-Order Temporal Logic

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 non-
empty 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             S interpreta-
tion In . An assignment a is a function from the set of variables to n∈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

                                           35
      Mn |=a ⊤
      Mn |=a P (t1 , . . . , tn ) iff (In (a(t1 )), . . . , In (a(tn ))) ∈ In (P )
      Mn |=a ¬ϕ                   iff not Mn |=a ϕ
            a
      Mn |= ϕ ∨ ψ                 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 ϕ
            a
      Mn |=     ϕ                 iff for all m ≥ n, Mm |=a ϕ
            a
      Mn |= ϕ 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               ϕ

               Fig. 1. Truth-Relation for First-Order Temporal Logic

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, Ei, 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 non-
ground 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, Ei the monodic
FOTL formula I∧ U∧ ∀xS∧ ∀xE. When we talk about particular properties

                                            36
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 tech-
nique which substitutes non-atomic subformulae by atomic formulae with new
predicate symbols and replaces temporal operators by their fixed point defini-
tions as described, for example, in [8].
Theorem 1 (see [4], Theorem 3.4). Any monodic formula in first-order tem-
poral 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, Ei be a monodic temporal problem. With ev-
ery eventuality ♦L(x) ∈ E and constant c occurring in P we uniquely associate
a propositional symbol pL          c . 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, consist-
ing of the clausification of U and clauses ¬pL            c ∨ 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 ♦pL                       ′
                                                                   c 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 conse-
quence 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 in-
stantiated 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     Ordered Fine-Grained Resolution with Selection
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.


                                              37
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.
(1) First-order ordered resolution with selection between two universal clauses
                                    C1 ∨ A ¬B ∨ C2
                                        (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.
(2) First-order ordered positive factoring with selection
                                        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.
(3) First-order ordered resolution with selection between an initial and a uni-
     versal clause, between two initial clauses, and ordered positive factoring with
     selection on an initial clause. These are defined in analogy to the two deduc-
     tion rules above with the only difference that the result is an initial clause.
(4) Ordered fine-grained step resolution with selection.
                         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.

                                          38
(5) Ordered fine-grained positive step factoring with selection.
                                   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 σ.
(6) Clause conversion. A step clause of the form C ⇒ ⊥ is rewritten to the
    universal clause ¬C.
    Step clauses of the form C ⇒ ⊥ will also be called terminating or final
    step clauses.
(7) Duplicate literal elimination in left-hand sides of terminating step clauses.
    A clause of the form (C ∧ A ∧ A) ⇒ ⊥ yields the clause (C ∧ A) ⇒ ⊥.
(8) Eventuality resolution rule w.r.t. U:
       ∀x(A1 (x) ⇒ B1 (x)) · · · ∀x(An (x) ⇒ Bn (x))                ♦L(x)
                                    Vn                                     (♦Ures ) ,
                                 ∀x i=1 ¬Ai (x)
    where ∀x(Ai (x) ⇒ Bi (x)) are formulae computed from the set of step
    clauses such that for every i, 1 ≤ i ≤   W n, the loop side conditions ∀x(U ∧
    Bi (x) ⇒ ¬L(x)) and ∀x(U ∧ Bi (x) ⇒ nj=1 (Aj (x))) are valid.2
    The set of full merged step clauses, satisfying
                                              Wn        the loop side conditions, is
    called a loop in ♦L(x) and the formula j=1 Aj (x) is called a loop formula.
    More details can be found in [10].
(9) Ground eventuality resolution rule w.r.t. U:
                     A1 ⇒ B1 · · · An ⇒ Bn                ♦l
                                    Vn                        (♦U
                                                                res ) ,
                                      i=1 ¬Ai
    where Ai ⇒ Bi are ground formulae computed from the set of step clauses
                Wn every i, 1 ≤ i ≤ n, the loop side conditions U ∧ Bi |= ¬l and
    such that for
    U ∧ Bi |= j=1 Aj are valid. The notions of ground loop and ground loop
    formula are defined similarly to the case above.
    Rules (1) to (7), also called rules of fine-grained step resolution, are either
identical or closely related to the deduction rules of ordered first-order resolution
with selection; a fact that we exploit in our implementation of the calculus. The
condition in rules (4) and (5) that a unifier σ may not map variables from
the antecedent into a constant or a functional term is a consequence of the
expanding domain assumption. Without this restriction, the calculus would be
unsound [12, Example 5].
    Loop formulae, which are required for applications of the rules (8) and (9),
can be computed by the fine-grained breadth-first search algorithm (FG-BFS),
depicted in Fig. 2. In this algorithm, LT(S) is the minimal set of clauses contain-
ing S such that for every non-ground step clause (P (x) ⇒ M (x)) ∈ S, the set
LT(S) contains the clause P (cl ) ⇒ M (cl ) (cl is a constant used only for loop
search). The process of running the FG-BFS algorithm is called loop search. A
variant of the FG-BFS algorithm for handling ground eventualities also exists.
2
    In the case U |= ∀x¬L(x), the degenerate clause, ⊤ ⇒ ⊤, can be considered as a
    premise of this rule; the conclusion of the rule is then ¬⊤.


                                         39
    Function 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 loop formula H(x) with at most one free variable.
    Method: (1) Let H0 (x) = true; M0 = ∅; i = 0
            (2) Let Ni+1 = U ∪ LT(S) ∪ {true ⇒ (¬Hi (cl ) ∨ L(cl ))}. Apply
                the rules of ordered fine-grained resolution with selection except
                the clause conversion rule to Ni+1 . If we obtain a contradiction,
                then return the loop true (in this case ∀x¬L(x) is implied by the
                universal part).
                Otherwise let Mi+1 = {Cj ⇒           ⊥}nj=1 be the set of all new
                terminating step clauses in the saturation of Ni+1 .
            (3) If Mi+1 = ∅, return false; else let Hi+1 (x) = n      ˜      l
                                                                 j=1 (∃Cj ){c → x}
                                                               W

            (4) If ∀x(Hi (x) ⇒ Hi+1 (x)), return Hi+1 (x).
            (5) i = i + 1; goto 2.
    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 (1) to (7) above, together with the ground and non-ground eventuality
resolution rules described above, i.e. rules (8) and (9). We denote this calculus
by IS,≻
     FG
        .
Definition 4 (Derivation). A (linear) derivation ∆ (in IS,≻              FG
                                                                            ) from the clausi-
fication Cls(P) = hU1 , I1 , S1 , Ei of a monodic temporal problem P is a sequence
of tuples ∆ = hU1 , I1 , S1 , Ei, hU2 , I2 , S2 , Ei, . . . 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 IS,≻      FG    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 (IS,≻
     FG
          -)refutation of hU1 , I1 , S1 , Ei.
     A derivation ∆ is fairS if and     S only ifS for each clause C which can be de-
rived from premises in h i≥1 Ui , i≥1 Ii , i≥1 Si , Ei there exists an index j such
that C occurs in hUj , Ij , Sj , Ei.

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 IS,≻FG
                                                   -refutation of Cls(P). Moreover, P
is unsatisfiable iff any fair IS,≻
                               FG
                                   -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 .


                                             40
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 IS,≻
                                                              FG
                                                                 . Rule (7), which
allows the elimination of duplicate literals in the left-hand sides of step clauses,
is required to establish this correspondence.


4    Adding Redundancy Elimination

Given that our calculus uses an ordering refinement, it seems natural to es-
tablish 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 IS,≻         FG has the re-
duction 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 conclu-
sion 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 IS,≻    FG 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 IFG     S,≻
                                    is not reductive wrt. I. Thus, this model functor
is not suitable for establishing that IS,≻  FG
                                               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 elimi-
nation rules. In the following we will define the notions of a tautological clause
and of a subsumed clause. In order to show that IS,≻       FG
                                                              is still complete if such
clauses are eliminated during a derivation, we need to show that for every refuta-
tion 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:

                                          41
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 uni-
      versal 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 (4) and (5), it has to be ensured
that variables occurring in the left-hand sides C1 and C2 are only mapped to
variables. While for the two inference rules this restriction is imposed to ensure
soundness, here the motivation is completeness.
    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 re-
solved with ¬Q(c) using rule (4) with the identity substitution as unifier to

                                         42
obtain P (c) ⇒ ⊥ which, using the conversion rules, gives us a new univer-
sal clause ¬P (c). Another inference step with P (x) results in a contradiction.
Now, without a restriction on the substitution that can be used in subsumption,
P (x) ⇒ Q(x) would subsume P (c) ⇒ Q(c). We could then try to derive a
contradiction by resolving P (x) ⇒ Q(x) with ¬Q(c). However, the unifier of
Q(x) and Q(c) maps the variable x, which also occurs on the left-hand side of
the step clause to the constant c. Thus, an inference by rule (4) using these two
premises is not possible and a contradiction can no longer be derived.

Definition 6. Let C and D be initial, step or universal clauses. Then we say
that C properly subsumes D, written C <s D, if and only if C subsumes D but
not vice-versa, i.e. C <s D iff C ≤s D and D 6≤s C.

Lemma 2. Let C and D be initial, step or universal clauses such that C ≤s D.
                                                           ˜ ⇒ [∀D]
Then it holds for an initial clause D that the formula [( )∀C]  ˜ is valid,
                                                         ˜       ˜ is valid,
and for a step or universal clause D that the formula [ ∀C] ⇒ [ ∀D]
      ˜
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 .

                                       43
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 IS,≻
                                                   FG,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 , Ñ be sets of step
clauses such that N ≤s Ñ . 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 ∪ Ñ .
    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 Ñ . 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 (1) to (5) and (7), from premises C˜1 and C˜2 which
are either elements of U ∪ Ñ or previously derived clauses. By the induction
hypothesis there are clauses C1 and C2 with C1 ≤s C˜1 and C2 ≤s C˜2 which are
either elements of U ∪ N or previously derived, and either C1 ≤s C,   ˜ C2 ≤s C˜ or
                                       ˜
we can derive a clause C with C ≤s C from C1 and C2 .

Lemma 6. Let N and Ñ be sets of initial, universal clauses or step clauses such
that N ≤s Ñ . Additionally, let ∆˜ be a derivation of a clause C˜ by subsumption
complete ordered fine-grained resolution with selection from clauses in Ñ .
   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 Ñ \ taut(Ñ ) and C is not a
tautology.


                                        44
    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: (1) Let R0 (x) = true; M0 = ∅; i = 0
                       ′
            (2) Let Ni+1   = U ∪ LT(S) ∪ {true ⇒ (¬Ri (cl ) ∨ L(cl ))}. Apply
                the rules of ordered fine-grained resolution with selection except
                                                  ′
                the clause conversion rule to Ni+1   , together with the removal of
                tautological and subsumed clauses. If we obtain a contradiction,
                then return the loop true (in this case ∀x¬L(x) is implied by the
                universal part).
                Otherwise let M′i+1 = {Cj ⇒           ⊥}nj=1 be the set of all new
                                                                  ′
                terminating step clauses in the saturation of Ni+1   .
                                                               Wn ˜
            (3) If Mi+1 = ∅, return false; else let Ri+1 (x) = j=1 (∃Dj ){cl → x}
                     ′

            (4) If ∀x(Ri (x) ⇒ Ri+1 (x)), return Ri+1 (x).
            (5) i = i + 1; goto 2.

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 Ñ , 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 Ñ \ taut(Ñ ) 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 D̃i 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 IS,≻FG,Sub
                                                 -refutation of Cls(P). Moreover, P is
unsatisfiable iff any fair IS,≻
                            FG,Sub
                                   -derivation    is a refutation of Cls(P).

Proof. Given a IS,≻
                  FG -refutation ∆ of P we establish by induction on ∆ that there
also exists a IFG,Sub
               S,≻
                      -refutation of P using Lemmata 3 to 6.


5    Subsumption and Loop Search

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
IS,≻
  FG,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.

                                          45
    The answer to that is positive. Figure 3 shows the so-called subsumption re-
stricted breadth-first search algorithm using ordered fine-grained step resolution
with selection, a modification of FG-BFS which removes tautological and sub-
sumed clauses during the saturation process by ordered fine-grained resolution
with selection in step (2) of the algorithm. In the way in which the algorithm
shown in Figure 3 is defined the constructed sets M′i will not contain terminating
step clauses C ⇒ ⊥ and D ⇒ ⊥ such that C ≤s D.
    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 IS,≻
                 FG,Sub
                        -refutation of Cls(P) with applications of the eventuality
resolution rule restricted to loop formulae found by the function Subsumption-
Restricted-FG-BFS. Moreover, P is unsatisfiable iff any fair IS,≻ FG,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     Implementation and Experimental Results

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 US 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
US to WO. Based on the results in the previous two sections, we can apply
tautology elimination (to N EW), forward subsumption and backward subsump-
tion [18]. With forward subsumption all clauses in N EW that are subsumed by
a clause in WO or US are deleted from N EW. With backward subsumption
clauses in WO and US subsumed by a clause in N EW are deleted from these
sets. After redundancy elimination the remaining clauses in N EW are added to
US. This process continues until either a contradiction is derived or US 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 spec-
ification 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/


                                        46
     -F/-B/-T    -F/+B/-T      -F/-B/+T      -F/+B/+T
  Clauses Time Clauses Time Clauses Time Clauses Time
1      —     TO    —     TO 239202 328.938s 17664 0.193s
2      —     TO    —     TO      —      TO 694574 10.959s
3      —     TO    —     TO      —      TO      —     TO
4      —     TO    —     TO      —      TO 529244 12.566s
5      —     TO    —     TO      —      TO      —     TO
6      —     TO    —     TO      —      TO      —     TO
    +F/-B/-T     +F/+B/-T     +F/-B/+T      +F/+B/+T
  Clauses Time Clauses Time Clauses Time Clauses Time
1     481 0.035s  480 0.039s    445  0.033s    444 0.038s
2   2354 0.130s  2262 0.129s   1926  0.115s   1892 0.124s
3 11065 1.375s   9912 1.310s 10102   1.350s   9170 1.278s
4   1460 0.087s  1559 0.097s   1125  0.074s   1343 0.093s
5     594 0.051s  594 0.052s    488  0.044s    488 0.049s
6     765 0.059s  765 0.055s    645  0.050s    645 0.054s
               Table 1. Results Obtained for the Cluedo Examples

consist of six valid, i.e. unsatisfiable, assertions that can be made in an exam-
ple 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 prob-
lem. 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   Conclusion

In this paper we have considered redundancy elimination in the context of or-
dered fine-grained resolution with selection, a sound and complete resolution-
based calculus for monodic first-order temporal logic. We have shown that a
slight modification of the calculus is compatible with the elimination of tautolo-
gies 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 resolu-

                                       47
tion [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 theo-
rem proving in monodic first-order temporal logic.

References
 1. L. Bachmair and H. Ganzinger. Resolution theorem proving. In Robinson and
    Voronkov [17], chapter 2, pages 19–99.
 2. Cluedo. http://www.hasbro.com.
 3. A. Degtyarev, M. Fisher, and B. Konev. Monodic temporal resolution. In Proc.
    CADE-19, volume 2741 of LNCS, pages 397–411. Springer, 2003.
 4. A. Degtyarev, M. Fisher, and B. Konev. Monodic temporal resolution. ACM
    Transactions On Computational Logic, 7(1):108–150, 2006.
 5. C. Dixon. Specifying and verifying the game Cluedo using temporal logics of
    knowledge. Technical Report ULCS-04-003, University of Liverpool, 2004.
 6. C. Dixon, M. Fisher, B. Konev, and A. Lisitsa. Practical first-order temporal
    reasoning. In Proc. TIME’08, pages 156–163. IEEE Comp. Soc., 2008.
 7. E. A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer
    Science, Volume B: Formal Models and Semantics, pages 995–1072. Elsevier, 1990.
 8. M. Fisher, C. Dixon, and M. Peim. Clausal temporal resolution. ACM Transactions
    on Computational Logic, 2(1):12–56, 2001.
 9. I. Hodkinson, F. Wolter, and M. Zakharyaschev. Decidable fragments of first-order
    temporal logics. Annals of Pure and Applied Logic, 106:85–134, 2000.
10. U. Hustadt, B. Konev, and R. A. Schmidt. Deciding monodic fragments by tempo-
    ral resolution. In Proc. CADE-20, volume 3632 of LNCS, pages 204–218. Springer,
    2005.
11. B. Konev, A. Degtyarev, C. Dixon, M. Fisher, and U. Hustadt. Towards the
    implementation of first-order temporal resolution: the expanding domain case. In
    Proc. TIME-ICTL 2003, pages 72–82. IEEE Comp. Soc., 2003.
12. B. Konev, A. Degtyarev, C. Dixon, M. Fisher, and U. Hustadt. Mechanising first-
    order temporal resolution. Information and Computation, 199(1-2):55–86, 2005.
13. R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev. Temporalising
    tableaux. Studia Logica, 76(1):91–134, 2004.
14. M. Ludwig and U. Hustadt. Implementing a fair monodic temporal logic prover.
    AI Communications. To appear.
15. M. Ludwig and U. Hustadt. Fair monodic temporal reasoning. In Proc. CADE-22,
    2009. To appear.
16. M. Ludwig and U. Hustadt. Resolution-based model construction for PLTL. In
    Proc. of TIME’09, 2009. To appear.
17. J. A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning (in
    2 volumes). Elsevier and MIT Press, 2001.
18. C. Weidenbach. Combining superposition, sorts and splitting. In Robinson and
    Voronkov [17], pages 1965–2013.
19. F. Wolter and M. Zakharyaschev. Axiomatizing the monodic fragment of first-order
    temporal logic. Annals of Pure and Applied Logic, 118:133–145, 2002.



                                         48

</pre>