CSE 463/563, Spring 2005 http://www.cse.buffalo.edu/∼rapaport/563S05.html

HOMEWORK #8: CLAUSE FORM

Last Update: 23 March 2005

Note: NEW or UPDATED material is highlighted

Convert each of the following FOL wffs to clause form, as defined by the algorithm presented in lecture. For partial credit, show all your work, and justify each step using the algorithm’s numbering scheme.

1. (P ∧ Q) ∨ (R ∧ S)

2. ∃x∀y∃z∃w∀u∀v∃t.P(x,y,z,w,u,v,t)

3. ∃x[S(x) ∧ ∀y[S(y) ⊃ y = x]]

4. ∃x∀y[¬S(y,y) ⊃ S(x,y)]

5. Do *NOT* attempt this one unless your mind is entirely clear and you have nothing else to do. But, if you find yourself in that situation, you might find this sort of fun to try :-) (P ≡ Q) ≡ (¬P ≡ ¬Q)

DUE: AT THE BEGINNING OF LECTURE, FRIDAY, APR. 1

\begin{matrix}c \\ ◯ \end{matrix}2005, William J. Rapaport rapaport@cse.buffalo.edu http://www.cse.buffalo.edu/∼rapaport/563S05/hw08-2005-03-23.pdf