Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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...

share|cite|improve this question
up vote 0 down vote accepted

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.

share|cite|improve this answer
Thanks. This is "resolution": – 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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.