CSE 463/563, Spring 2005

# Another Resolution Example

 Last Update: 17 March 2005 Note: or material is highlighted

Here's another example of the use of Refutation + Resolution + Unification to show the validity of a first-order inference:

Show that the following inference is valid:

x[P(x) v Q(x)], x.¬P(x) x.Q(x)

1. Convert all premises to Clause Form:

x[P(x) v Q(x)] ---> P(x) v Q(x) ---> [P(x), Q(x)] (where "--->" means "rewrites as")

x.¬P(x) ---> [¬P(c)] (where c is a Skolem constant)

2. Convert the negation of the conclusion (for Refutation) to Clause Form:

¬x.Q(x) ---> x.¬Q(x) ---> [¬Q(x)]

3. Union the above, renaming variables:

{[P(x),Q(x)], [¬P(c)], [¬Q(y)]}

4. Apply Resolution to derive [ ]. Where Unification is needed in order to do this, show the MGU.

```     [P(x),Q(x)] -P(c)	-Q(y)
\      /      /
\    /      /
{x/c} \  /      /
\/      /
Q(c)    /
\    /
{y/c} \  /
\/
[]
```

Alternatively:

```   [P(x),Q(x)]  -Q(y)	 -P(c)
\         /        /
\       /        /
\     /        /
{y/x} \   /        /
\ /        /
P(x)      / {x/c}
\      /
\    /
\  /
\/
[]
```