How to obtain the empty clause from CNF? 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.
 A: 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.
