Resolution and Clausal Form

Because it is refutation-complete in the sense that given any unsatisfiable set of sentences, it is guaranteed to produce the empty clause through repeated use of the rule, resolution is often used in theorem proving applications. Its disadvantages are that the rule can be difficult to use and some feel that the knowledge base is not intuitive.

Resolution produces proofs by refutation . One proves a statement by resolution by showing that the negation of the statement produces a contradiction with the statements that are known to be true. Resolution gains much of its efficiency by requiring that all the data statements be in a reduced standard form called conjunctive normal form (CNF) or clausal form. However the number of data statements required in clausal form are often larger than those in other logical systems for the same knowledge base. The clausal form is made of literals and clauses. A literal is an atomic sentence (positive literal) or the negation of an atomic sentence (negative literal). A clause is a set of literals operated on as disjunctions. A horn clause is a clause with at most one positive literal.

2 Conjunctive Normal Form and Clausal Form

To convert a prefix predicate calculus statement in conjunctive normal form [Davis, 1960], perform the following sequence of steps:

1. Eliminate the logical operator IF: Use the fact that

(IF A B) can be written as (OR (NOT A) B)

2. Reduce the scope of NOT: Distribute negations over other logical operators until each operator applies to a single atomic sentence. The goal is to move negations inward so that they are only applied to atomic sentences.

(a) Use the fact that (NOT (NOT P)) = P

(b) Apply deMorgan's Laws: (NOT(AND A B)) = (OR (NOT A) (NOT B))

(NOT(OR A B)) = (AND (NOT A) (NOT B))

(c) Apply the standard correspondence between quantifiers:

(NOT (ALL x P)) = (EXIST x (NOT P))

(NOT (EXIST x P)) = (ALL x (NOT P))

3. Distinguish Variables: Standardize variables so that each quantifier binds a unique variable. We do not want the same variable to be quantified more than once within the same logical sentence. This avoids confusion later on when we drop quantifiers. For example,

(OR (ALL x P) (ALL x Q))

would be converted to (OR (ALL x P) (ALL y Q))

This step is a preparation for the next step.

4. Convert to prenex normal form: Move all quantifiers to the left, without changing their relative order. This is possible at this point (after step 3), because there is no conflict among variable names. The result should be structured so that all quantifiers are a prefixto logical sentences which are quantifier-free.

The statement above would be converted to:

(All x y (OR P Q))

5. Eliminate existential quantifiers (Skolemize): Apply the most general form of existential instantiation. This are two cases under this step:

(a) If an existential quantifier does not occur within the scope of a universal quantifier, then drop the quantifier and replace all occurrences of the quantified variable by a Skolem constant, one that has not been used elsewhere in the database.

(b) If an existential quantifier is within the scope of any universal quantifier, there is the possibility that the value of the existential variable depends on the values of the associated universal variables. Thus we cannot replace the existential variable with a constant. Instead we replace the variable with a term formed from a Skolem function applied to all the variables associated with the universal quantifier outside the existential quantifier in question. For example the logical sentence (ALL x (EXIST y (R x y))) could be replaced by (ALL x (R x (F x))) where F is a Skolem function which has not been used before.

6. Eliminate universal quantifiers. Because all universal quantifiers are at the left of the statement, the quantifier can be eliminated if we assume now that any variable is universally quantified.

7. Convert all logical sentences into conjunctions of disjunctions (conjunctive normal form). Use the associative and distributive laws of classical logic.

For example,

8. Apply And Elimination (AE) in order to put the statements into clausal form: Statement Q2 above would remain unchanged. Statements Q1 and Q3 would be converted to the following set of logical sentences:

9. Standardizing the variables apart: In the last step we rename variables so that no variable appears in more than one clause.

3. Exercises on Clausal Form:

3.1 (IF (ALL x (F x)) (ALL x (G x)))

i). Eliminate IF: (OR (NOT (ALL x (F x))) (ALL x (G x)))

ii). Reduce scope of NOT: (OR (EXIST x (NOT (F x))) (ALL x (G x)))

iii). Distinguish variables: (OR (EXIST x (NOT (F x))) (ALL y (G y)))

iv). Convert to prenex form: (ALL y (OR (EXIST x (NOT (F x))) (G y)))

v). Apply EI: (ALL y (OR (NOT (F (E y))) (G y)))

vi). Eliminate universal quantifiers: (OR (NOT (F (E y))) (G y))

3.2 (EXIST x (IF (F x) (G x)))

i). Eliminate IF: (EXIST x (OR (NOT (F x)) (G x)))

ii). Apply EI: (OR (NOT (F X)) (G X))

3.3 (EXIST x (ALL y (F x y)))

Solution 3.3:

i). Convert to prenex form: (ALL y (EXIST x (F x y)))

ii). Apply EI: (ALL y (F (E y) y))

iii). Eliminate universal quantifiers: (F (E y) y)

4. Resolution Procedure

5. Exercises on Resolution

5.1 Resolution is a refutation proof method performed on logical sentences in conjunctive normal form. This can best be described by an example. Consider the following set of axioms or logical sentences in prefix predicate logic form.

1 (P1 A)

2. (IF (P1 x) (Q1 x))

3. (IF (P2 x) (Q1 x))

4. (IF (P2 x) (Q2 x))

5. (IF (P3 x) (Q2 x))

6. (IF (Q1 x) (R1 x))

7. (IF (Q2 x) (R3 x))

The first step is to put all of the logical sentences into conjunctive normal form.

1. (P1 A)

2. (OR (NOT (P1 x1))(Q1 x1))

3. (OR (NOT (P2 x2))(Q1 x2))

4. (OR (NOT (P2 x3))(Q2 x3))

5. (OR (NOT (P3 x4))(Q2 x4))

6. (OR (NOT (Q1 x5))(R1 x5))

7. (OR(NOT (Q2 x6))(R3 x6))

Let us prove that (R1 A) is true by resolution. We do this by adding the negation of the goal to the data base.

8. (NOT (R1 A))

9. (Q1 A)

10. (R1 A)

We have shown a contradiction and have proven that (R1 A) is true.

6 Problem

P1: Some pipes have large cracks.

P2: A pipe with a large crack is a failure.

7 References