# FOL Deduction (with resolution).

Let $a$ be a constant symbol, $P,Q, A, Io, C$ a predicate symbol, x a variable symbol. Given the following set of FOL (first order logic) formulae $KB$:

1)$\forall x \exists y \exists z P(x)\wedge A(y) \wedge A(z) \wedge Q(x,y,z)\Rightarrow Q(a,y,z)$

2)$\forall x \forall y \forall z P(x)\wedge A(y) \wedge A(z) \wedge Q(x,y,z)\Rightarrow Q(a,y,z)$

3)$\forall x Io(x)\Rightarrow C(x)$

Using resolution, determine a formula such that, simultaneously combined with the formulas (1) (2) (3), causes a contradiction in the KB.

I rewrote the formulas in the conjunctive normal form:

$\rceil P(x)\vee \rceil A(f(x))\vee \rceil A(g(x))\vee \rceil Q(x,f(x),g(x))\vee Q(a,f(x),g(x))$

$\rceil P(x)\vee \rceil A(y)\vee \rceil A(z)\vee \rceil Q(x,y,z)\vee Q(a,y,z)$

$\rceil Io(x)\vee C(x)$

where f and g are Skolem functions. Now I can not go forward...

-

Observe that (under the assumption that the domain has two or more elements, otherwise 1) and 2) are trivially true), 1) is entailed by 2).

This suggests making 2) and 3) false, using a suitable disjunction. For example:

$$\left[Io(a) \land \neg C(a)\right] \lor \forall x\forall y\forall z\left[P(x) \land A(y) \land A(z) \land \neg Q(a,y,z) \land (x \ne a \implies Q(x,y,z))\right]$$

Edit: To apply resolution to the entire formula would be nightmarishly complicated. In fact, the whole procedure seems like it is only ever feasible when fed to a computer.

Therefore, I will discard my previous assumption that "pairing the contradictory formula with a proper subset of 1), 2), 3) does not give a contradiction". (It may not even have been an intended assumption by the problem designer.)

Concretely, we focus on adding an assumption making $\forall x(Io(x) \implies C(x))$ false. That is, we simply take $Io(a) \land \neg C(a)$ from our previous formula.

Following the resolution protocol, we recall the CNF form of our formula:

$$\neg Io(x) \lor C(x)$$

This, paired with our assumption, yields the following set of clauses:

$$S = \{ \neg Io(x) \lor C(x), Io(a), \neg C(a)\}$$

The necessary unifications amount to replacing $S$ by:

$$S' = \{\neg Io(a) \lor C(a), Io(a),\neg C(a)\}$$

Now we can get started with the actual resolution, which is now easy:

$$\frac{\quad \neg Io(a) \lor C(a) \qquad Io(a) \quad}{C(a)}\qquad \frac{\quad C(a) \qquad \neg C(a)\quad}{}$$

Now the empty space under the latter bar signifies $\bigvee \varnothing$, the disjunction over zero statements. This is logically equivalent to $\bot$, i.e., a contradiction. We are done.

Now if we wanted to tackle the longer formula above, we would first have to bring it into CNF, which in itself is already tedious. Then we'd have to apply similar mechanical procedures to arrive at a contradiction.

-
Thanks. This is "resolution": en.wikipedia.org/wiki/Resolution_(logic) – Mark Sep 27 '13 at 12:12
Edited to include a resolution of the first disjunct in the proposed formula. – Lord_Farin Sep 27 '13 at 12:36