resolution - satisfiability of formula (edit: renaming clause variables)

Question

I need to determine whether the following formula is satisfiable, using binary resolution:
$$exists x forall y forall z ((P(y) to Q(z)) to (P(x) to Q(x)))$$
I re-framed the problem to showing that the [above] formula's negation is unsatisfiable:
$lnotexists x forall y forall z ((P(y) to Q(z)) to (P(x) to Q(x)))$ negation of the [original] formula
$forall x  lnot ((P(g(x)) to Q(h(x))) to (P(x) to Q(x)))$ skolemized: y = g(x) & z = h(x)
$forall x ((lnot P(g(x)) lor Q(h(x))) land P(x) land (lnot Q(x)))$ converted to CNF
Now, it is clear that I cannot derive an empty clause from the set of clauses $${[lnot P(g(x)), Q(h(x))], , [P(x)], , [lnot Q(x)] }$$ Does this mean that the negation of the [original] formula is satisfiable?

But I'm unable to derive an empty clause even using the original formula:
$exists x forall y forall z ((P(y)  to Q(z)) to (P(x) to Q(x)))$ original formula
$forall y forall z ((P(y) to  Q(z)) to (P(a) to Q(a)))$ skolemized: x = a
$forall y forall z ((P(y) lor lnot P(a) lor Q(a)) land (lnot Q(z) lor lnot P(a) lor Q(a))$ converted to CNF
Now, again clearly I cannot derive an empty clause from the set of clauses
$${[P(y), lnot P(a), Q(a)], , [lnot Q(z), lnot P(a), Q(a)] }$$ Does this mean that the satisfiability of the [original] formula cannot be determined?

Taroccoesbrocco · Accepted Answer

In fact, the formula
$$tag{1} exists x forall y forall z big( (P(y) to Q(z)) to (P(x) to Q(x)) big)$$
is valid, which means that every structure satisfies it. In particular, it is satisfiable.
This is because, by applying the resolution method to the negation of the formula $(1)$, it is possible to get the empty clause. Hence, the negation of $(1)$ is unsatisfiable, which amounts to say that $(1)$ is valid.
Your syntactical handling starting from the negation of $(1)$ is correct, eventually you get the clauses:
begin{align}
{¬P(g(x)), Q(h(x))} && {P(x)} && {¬ Q(x)}
end{align}
and after renaming the free variables so that distinct clauses have no variables in common (all variables in a clause are implicitly universally quantified, hence renaming does not change satisfiability), you get
begin{align}
tag{2}
{¬P(g(x)), Q(h(x))} && {P(y)} && {¬ Q(z)}
end{align}
You can resolve the first two clauses on $(2)$ thanks to the MGU ${y leftarrow g(x)}$, thus the resolvent is the clause
begin{align}
tag{3}
{Q(h(x))}
end{align}
You can resolve the clause $(3)$ with the third clause in $(2)$ thanks to the MGU ${z leftarrow h(x)}$, and the resolvent is the empty clause $square$.
Since there is a way to derive the empty clause by repeating the resolution method, the negation of $(1)$ is unsatisfiable and hence $(1)$ is valid, in particular $(1)$ is satisfiable.

EDIT. Note that the formula
$$forall x big((lnot P(g(x))lor Q(h(x)))land P(x) land lnot Q(x) big) $$
(the CNF you correctly wrote in the OP) is logically equivalent to
$$forall x (lnot P(g(x))lor Q(h(x))) land forall x P(x) land forall xlnot Q(x)$$
which is the same as
$$forall x (lnot P(g(x))lor Q(h(x))) land forall y P(y) land forall zlnot Q(z).$$
This the logical reason that explains why the clauses
begin{align}
{¬P(g(x)), Q(h(x))} && {P(x)} && {¬ Q(x)}
end{align}
can be rewritten as in $(2)$ above, after renaming the free variables so that distinct clauses have no variables in common.

resolution - satisfiability of formula (edit: renaming clause variables)

One Answer

Add your own answers!

Ask a Question