1
$\begingroup$

I have the following formula $\mathcal{F} = A(c, y) \wedge A(c, z) \wedge \neg E(c, z) \wedge \neg A(z, c)$ from which I've derived the clauses $\{A(c, y)\},\{A(c, z)\},\left\{\neg E\left(c, z_{1}\right)\right\},\left\{\neg A\left(z_{2}, c\right)\right\}$, however I'm unsure how to simplify them to obtain the empty clause by using the resolution method.

My textbooks suggests applying the substitution $\sigma=\left\{c / z_{2}, c / y\right\}$, but how does that really work?

I seem to miss some understanding from the meaning of substitution.

$\endgroup$
1
  • $\begingroup$ Which means do you know to simplify a formula? $\endgroup$
    – Taroccoesbrocco
    Commented Sep 9, 2020 at 15:54

1 Answer 1

Reset to default
1
$\begingroup$

Applying the substitution $\{c/z, c/y\}$ to the formula $\mathcal{F}$ means that you have to replace each free occurrence of $z$ and $y$ in $\mathcal{F}$ with $c$. And similarly for clauses.

Consider the clauses $\{A(c, y)\}, \ \{A(c, z)\},\ \left\{\neg E\left(c, z_{1}\right)\right\}, \ \left\{\neg A\left(z_{2}, c\right)\right\}$ that you correctly derived from the formula $\mathcal{F}$. To derive the empty clause by applying the resolution method, you are allowed to apply substitutions to clauses. In particular, by applying the substitution $\sigma = \{c/z_2, c/y\}$, you get the clauses $$\{A(c, c)\}, \ \{A(c, z)\},\ \left\{\neg E\left(c, z_{1}\right)\right\}, \ \left\{\neg A\left(c, c\right)\right\}$$

Note that $z, \, z_1, \, z_2$ are pairwise distinct variables, so the substitution affects only the first and last clauses. By applying the resolution rule to the first and last clauses, since they negate each other, you get the empty clause $\{\, \}$.

We have then found a way to derive the empty clause from the clauses given at the beginning. This is sufficient to conclude that the set of starting clauses, and then the starting formula $\mathcal{F}$, are unsatisfiable.

An accessible explanation of the theory of the resolution method for predicate logic is here.

There is another approach to prove that the formula $\mathcal{F}$ is unsatisfiable. Since the $\mathcal{F}$ is a conjunctive normal form (i.e. a conjunction of clausal formulas), it is unsatisfiable if and only if there is a substitution that makes it unsatisfiable.

So, by applying the substitution $\{c/z, \, c/y\}$ to the formula $\mathcal{F}$, you get:

\begin{align} \mathcal{F}\{c/z, \, c/y\} &= A(c,c) \land A(c,c) \land \lnot E(c,c) \land \lnot A(c,c) &\text{(substitution } \sigma) \\ &\equiv A(c,c) \land \lnot E(c,c) \land \lnot A(c,c) &\text{(idempotence of } \land) \\ &\equiv\lnot E(c,c) \land A(c,c) \land \lnot A(c,c) &\text{(commutativity of } \land) \\ &\equiv\lnot E(c,c) \land \bot &\text{(negation law for } \land) \\ &\equiv \bot &\text{(domination law for } \land) \end{align}

where $\bot$ is the falsehood (aka absurdity or empty clause), i.e. a formula that is always false.

I used the logical equivalences listed here.

$\endgroup$
9
  • $\begingroup$ Does $c/z$ and $c/y$ mean that I have to substitute $z$ and $y$ with $c$? $\endgroup$
    – Kevin
    Commented Sep 9, 2020 at 15:59
  • $\begingroup$ Kevin - Exactly! I edited my answer to explain that. $\endgroup$
    – Taroccoesbrocco
    Commented Sep 9, 2020 at 15:59
  • $\begingroup$ What's the intuition behind the substitution? I mean, substituting $z$ and $y$ with $c$ seems to force the formula to be always false (seems a particular case), but how do I know that it is also false from some other values? Sorry for the dumb question, but I'm new to logic :/ $\endgroup$
    – Kevin
    Commented Sep 9, 2020 at 16:05
  • $\begingroup$ @Kevin - Do you know what is the resolution method? How do you usually prove that a formula is equivalent to the empty clause? $\endgroup$
    – Taroccoesbrocco
    Commented Sep 9, 2020 at 16:07
  • 1
    $\begingroup$ @Kevin - Coming back to your first question in the comments, there is an important theorem about the resolution method: if a set $Δ$ of clauses is unsatisfiable, then there is a resolution derivation of the empty clause from $Δ$. This means that to prove that a formula $\mathcal{F}$ is unsatisfiable (i.e. always false), it is sufficient that there is a way to transform $\mathcal{F}$ to a clausal form and derive the empty clause from it. It is enough to find a way to do that, hence it is enough to find a particular substitution such that you can eventually derive the empty clause. $\endgroup$
    – Taroccoesbrocco
    Commented Sep 9, 2020 at 16:32

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .