CS 472/572 Spring 1997

Programming Project 3 AUTOMATED THEOREM PROVING

In this project, you will write programs to pass the graduate-level AI Qualifying Exam questions on logic :-)

1. (Warning: This part is relatively easy.)

(a) Given the following rules for converting a wff into clause form (also called Skolem standard form

(SSF)), write a Lisp function that takes a wff as input and returns an equivalent wff in SSF:

i. Eliminate all occurrences of ⇔ by rewriting all occurrences of

(P ⇔ Q) as ((P ⇒ Q) ∧ (Q ⇒ P)). ii. Eliminate all occurrences of ⇒ by rewriting all occurrences of

(P ⇒ Q) as (¬ P ∨ Q). iii. Reduce the scope of all ¬ signs to apply to at most one atomic wff by using these rewrite

rules:^{1}

¬ (P ∨ Q) → (¬ P ∧ ¬ Q)
¬ (P ∧ Q) → (¬ P ∨ ¬ Q)
¬ ∀vP  → ∃v[¬ P]
¬ ∃vP  → ∀v[¬ P]
¬ ¬ P  → P

iv. Rename variables so that every quantifier binds a unique variable, using rewrite rules of the following form:

(Q_{1}v_{1}F (v_{1}^{∗}) # Q_{2}v_{1}G(v_{1}^{∗})) → (Q_{1}v_{1}F (v_{1}^{∗}) # Q_{2}v_{2}G(v_{2}^{∗}))

where the Q_{i} are quantifiers (either the same or different), # is either ∨ or ∧, the v_{i} are variables such that ‘v_{1}’ ≠ ‘v_{2}’, and ‘F (v_{1}^{∗})’ represents a wff containing 0 or more occurrences of ‘v_{1}’. An example would be:

(∀xP (a, x) ∧ ∃xR(a)) → (∀xP (a, x) ∧ ∃yR(a))

v. Put the wff in Skolem Normal Form (SNF) by eliminating all existential quantifiers and

introducing appropriate Skolem constants and Skolem functions. vi. Put the wff in Prenex Normal Form (PNF) by moving all universal quantifiers to the left.

This can be done mechanically, but it is offically justified by the following equivalences:

• ((∀x[F(x)] ∨ ∀y[G(y)]) ⇔ ∀x∀y[F(x) ∨ G(y)])

• ((∀x[F(x)] ∧ ∀y[G(y)]) ⇔ ∀x∀y[F(x) ∧ G(y)])

• ((∀x[F(x)] ∨ H{x}) ⇔ ∀x[F(x) ∨ H{x}])

• ((∀x[F(x)] ∧ H{x}) ⇔ ∀x[F(x) ∧ H{x}]) where ‘F(x)’ and ‘G(x)’ denote wffs containing a free variable x, and ‘H{x}’ denotes a wff that does not contain the variable x.

vii. Eliminate all universal quantifiers. viii. Put the result into Skolem Standard Form (SSF) by rewriting

(P ∨ (Q ∧ R)) as ((P ∨ Q) ∧ (P ∨ R)).

(b) Apply your algorithm to the following wff:

∀x[Animal(x) ⇒ (P redator(x) ⇔ ∃y[Animal(y) ∧ Eats(x, y)])]

1The notation ‘α → β’ means: “rewrite α as β”.

2. (Warning: This part is relatively hard.)

(a) Implement a unification algorithm (either the one in the text, the one given in lecture, or—if you did it correctly—your pattern-matcher from Project 1 (perhaps suitably modified)). More precisely, your algorithm should take a pair of wffs as input and either return their MGU if they are unifiable or else return a message such as “NOT UNIFIABLE”. You may assume that the notation f(x, g(x)) can be understood as: (f x (g x)), if you prefer using Lispish notation.

(b) Use your algorithm to answer this question. For each of the following pairs of terms, if they unify, show a most general unifier (mgu); if they don’t, say so, and state why. Assume that u, v, x, y, and z are variables, and that a, b, and c are individual constants.

i. P (a, x, c) and P (y, b, z) ii. P (a, x, c) and P (y, b, y) iii. P (x, x, c) and P (u, v, u) iv. P (x, f(x), f(y)) and P (f(a), f(z), z) v. P (x, f(x), f(a)) and P (f(z), f(z), z)

3. (a) (Warning: The computational implementation of this part is relatively hard.) THE COMPUTATIONAL IMPLEMENTATION OF THIS PART IS OPTIONAL

Write a resolution + unification theorem prover for first-order predicate logic.

(b) Using resolution, show that the following set of clauses is inconsistent. Assume that a, b, and c are individual constants, and that x and y are variables. DO THIS PART (AT LEAST BY HAND) WHETHER OR NOT YOU DO PART 3a.

i. {On(a, b)} ii. {On(b, c)} iii. {Red(a)} iv. {Green(c)} v. {Red(b), Green(b)} vi. {¬Red(x), ¬Green(y), ¬On(x, y)}

NOTE: Please do all exercises at least by hand (in addition to, or instead of, using Lisp) as part of your report. I will hand out a tentative grading scheme to make it easier for you to organize your final report.

DUE AT START OF LECTURE, THURSDAY, APRIL 10.

NOTE: Starting with this project, I will institute a policy of what some people call “slip” days (I prefer the term “grace period”). You now have 3 “slip” days that you can use on this project or the next one. This works as follows: You may turn this project in up to 3 days late, with no penalty (where a “day” is a 24-hour time period; thus, you may turn this project in as late April 13). If you “spend” all your slip days on this project, then you will have none for the next one. If you turn this one in 1 day late (“spending” 1 of your slip days), then you will only have 2 slip days for the next project, and so on. Any projects turned in late after your slip days are used up will be accepted at the discount mentioned in the syllabus.