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