# Theorem proving, resolution

Luger: 2.3, 13, (15)

## Why theorem proving in an AI course?

• proving theorems is considered to require high intelligence
• if knowledge is represented by logic, theorem proving is reasoning
• theorem proving uses AI techniques, such as (heuristic) search
• (study how people prove theorems. Differently!)

## What is theorem proving?

Reasoning by theorem proving is a weak method, compared to experts systems, because it does not make use of domain knowledge. This, on the other hand, may be a strength, if no domain heuristics are available (reasoning from first principles). Theorem proving is usually limited to sound reasoning.

Differentiate between

• theorem provers: fully automatic
• proof assistants: require steps as input, take care of bookkeeping and sometimes 'easy' proofs.
Theorem proving requires
• a logic (syntax)
• a set of axioms and inference rules
• a strategy on when how to search through the possible applications of the axioms and rules
Examples of axioms
p -> (q->p)
(p->(q->r)) -> ((p->q) ->(p->r))
p \/ ~p
p->(~p->q)
Notation: I use ~ for "not", since it's on my keyboard.

Examples of inference rules

 name from derive modus ponens p, p->q q modus tollens p->q, ~q ~p and elimination p/\q p and introduction p, q p/\q or introduction p p\/q instantiation for all X p(X) p(a) rename for all X phi(X) for all Y phi(Y) exists-introduction p(a) exists X p(X) substitution phi(p) phi(psi) replacement p->q ~p\/q implication assume p ... ,q p->q contradiction assume ~p ...,false p resolution p\/phi, ~p\/psi phi \/ psi (special case) p, ~p\/psi psi (more special case) p, ~p false

Strategies
forwards - start from axioms, apply rules
backwards - start from the theorem (in general: a set of goals), work backwards to the axioms

when to apply which rule

general questions:
are the rules correct (sound)?
is there a proof for every logical consequence (complete)?
can we remove rules (redundant)?
Having redundant rules may allow shorter proofs, but a larger search space.

## Resolution and refutation

We want to prove theory -> goal.
The theory is usually a set of facts and rules, that can be treated as axioms (by the rule called implication above). A theory is usually quite stable, and used to prove various goals.
• we use contradiction, add ~goal to the axioms, and try to prove false.
• the theory and ~goal are put in clausal form - a set (conjunction) of  clauses
[see Luger p 558-560]
• use resolution and unification to derive false
Clauses
a clause is a universially quantified disjunction of literals
a literal is an atomic formula or its negation
examples of clauses: p \/ q, p(X) \/ q(Y), ~p(X) \/ q(X).
A special case is Horn-clauses: they have at most one positive (not negated) literal.
Three subclasses:
facts (1 pos, 0 neg): p(a,b).
rules (1 pos, > 0 neg): ~p \/ ~q \/ r - often written as: p /\ q -> r
goals(0 pos): ~p \/ ~q - if we want to prove p/\q from the theory, we add this clause - can be written as p /\ q -> false

Skolemization (p. 559)
How to remove existential quantification? Use function symbols!
Example: every person has a mother: (for all X) person(X) -> (exists Y) mother(X,Y)
Give a name to Y: the mother of X. (for all X) person(X) -> mother(X,mother_of(X))

This allows us to define datastructures in the logic.
Example: if X is an element and Y a list, then there is a list with head X and tail Y.
(for all X,Y) elt(X) /\ list(Y) -> (exists Z) list(Z) /\ head(Z,X) /\ tail(Z,Y)
first we name Z the cons of X and Y, then we get 3 rules:
elt(X) /\ list(Y) -> list(cons(X,Y)).
elt(X) /\ list(Y) -> head(cons(X,Y), X).
elt(X) /\ list(Y) -> tail(cons(X,Y), Y).

### Unification

Unification (2.3.2) is used to perform instantiation before (during) resolution.

Simple case:
Resolve list(nil) with ~elt(X) \/ ~list(Y) \/ list(cons(X,Y)).
First we must instantiate Y to nil, then we can derive ~elt(X) \/ list(cons(X,nil)).

Hard case:
I want to prove that there is a list that has the head mother_of(john).
So I take as a goal its negation ~(exists X)(list(X) /\ head(X,mother_of(john)))
This gives the clause  ~list(X) \/ ~head(X,mother_of(john))
We can resolve with ~elt(X) \/ ~list(Y) \/ head(cons(X,Y),X).
Problem 1: the X's in both clauses "accidentally" have the same name.
Solution 1: rename to ~elt(Z) \/ ~list(Y) \/ head(cons(Z,Y),Z).
The unifier is: {Z/mother_of(john), X/cons(mother_of(john),Y)}
The resolvent (resulting clause) is
(~list(X) \/ ~elt(Z) \/ ~list(Y)){Z/mother_of(john), X/cons(mother_of(john),Y)} =
~list(cons(mother_of(john),Y)) \/ ~elt(mother_of(john)) \/ ~list(Y)

Exercise: use the first list-rule and the facts elt(mother_of(john)) and list(nil)to complete the proof.

Unification as rewriting
the algorithm maintains a set of equalities. Each time, remove an equality and apply the applicable  rule.

• Var1 = Var1 - nothing (just remove the equality)
• Var1 = Expr - in all other equalities, replace Var1 by Expr, keep Var1 = Expr
exception: if Var1 occurs in Expr, then FAIL
• f(A1,..,An) = f(B1,..,Bn) - add {A1 = B1, .., An = Bn}
• f(A1,..,An) = g(B1,..,Bm) - FAIL
Example (the equality selected is underlined)