CSE 150 Lecture Notes, February 19, 2004

CSE 150 LECTURE NOTES

February 19, 2004

ANNOUNCEMENTS

The midterm went well. Please start asking questions about the Otter assignment!

THE "PROVES" NOTATION

Suppose we write T |- A. The symbol |- is pronounced"proves." This means that the sentence A can be proved by a theorem-proving algorithm, starting from the sentences in T.

We would like to have T |- A if and only if T |= A. The "only if" direction is called soundness. The "if" direction is called completeness.

Suppose we have a theorem-proving algorithm that will always prove A from T if T entails A. However, if T does not entail A, then the algorithm may fail to terminate (i.e. it may run for ever).

COMPLETENESS AND SEMI-DECIDABILITY

Definition: The proof algorithm |- is complete if whenever KB |= A then KB |- A in finite time.

Here |= means logical entailment, which is a semantic notion, while |- means provability, which is a syntactic, i.e. algorithmic notion. Completeness says that if A is true, then it can be proved eventually.

Given KB and A, it may be the case that KB |= A is not true and also KB |= ~A is also not true. Completeness says nothing about this case, where neither A nor ~A is entailed by KB, that is KB leaves the truth value of A unsettled.

Definition: The entailment relation |= is semi-decidable if a complete proof algorithm exists for it, while it is decidable if a proof algorithm exists that is complete and also always terminates in finite time.

Gödel's completeness theorem: First-order logic entailment |= is semi-decidable. In iother words, there exists an algorithm |- that is sound and semi-complete.

Gödel's incompleteness theorem (alternative statement): First-order logic entailment |= is not decidable.

REFUTATION PROOFS

Let's look at a theorem-proving method for FOL. This method is sound and semi-complete. It is basically the method used by Otter.

In order to prove a sentence in first-order logic, say alpha, add the negation of alpha to the knowledge base and derive a contradiction, i.e. prove that "false" follows from the axioms in the knowledge base.

Lemma: KB |= alpha if and only if KB union { ~alpha } is unsatisfiable.

Example: How to prove eats(jo,fish) from the following axioms? (Here x, y, z are variables that are implicitly universally quantified.)

~cat(x) v likes(x,fish)
~cat(y) v ~likes(y,z) v eats(y,z)
cat(jo)

Answer: add ~eats(jo,fish) and derive ~beta and beta separately for some literal beta. For example:

    ~eats(jo,fish)     ~cat(y) v ~likes(y,z) v eats(y,z)
           \\            /
       ~cat(jo) v ~likes(jo,fish)    cat(jo)
                         \\         /
~cat(x) v likes(x,fish) ~likes(jo,fish)
                    \      //
                     ~cat(jo)    cat(jo)
                           \     /
                             false

The proof above is typical, although of course it is very small. Some typical aspects:

The same axiom may be used many times, e.g. cat(jo) above.
The first step in the proof uses the negated goal.
The proof has a linear structure: each step uses the conclusion of the previous step, together with an axiom.

The "backbone" or main path of the proof is indicated with double red slashes above.

RESOLUTION

Exactly what inference rule(s) did we use in the example proof above? Answer: Just one rule, named resolution.

Resolution is a single inference rule that, when used in the right way, yields an inference algorithm that is complete. Resolution was invented by J. A. Robinson in 1965, building on ideas developed in the previous decade in the U.S. and in the Soviet Union.

Resolution is a generalization of unit propagation, which we saw as part of the DPLL algorithm.

Suppose that positive literal pj and the negative literal qk can be unified, with substitution S. (Unification is explained later). Then

p1 v ... v pj v ... v pm q1 v ... qk v ... v qn
------------------------------------------------------------------
(p1 v ... pj-1 v pj+1 ... v pm v q1 v ... qk-1 v qk+1 v ... v qn)S

In words, the consequent of the resolution inference rule is the disjunction of the two antecedent clauses, with the unifying literals pj and qk removed, and the unifying substitution S applied.

So-called modus ponens is a very special case of resolution. Let j = m = 1 and k = 1, n = 2, and show the negation sign on q1:

p1 ~q1 v q2
--------------
(q2)S

The modus ponens special case illustrates how resolution can make progress by yielding a conclusion that is shorter than its antecedents. In general, resolution yields a conclusion that is longer than either of the two inputs

Resolution is a form of reasoning by cases: either pj is true, or qk is true (after unification); there is no third possibility.

UNIFICATION

When two clauses in FOL are resolved together, we may need to match a variable in one clause with a constant in the other. This process is called unification.