Derive the box from a set of FOL clauses

S = {{P(x,y), P(f(y),z), Q(x,y)}, {~P(y, a), Q(y, x)}, {R(h(x), x), ~Q(x, a)},
{~R(x, y), ~R(h(z), y), ~Q(z, u)}}

For each resolution step specify the relabeling, the unification set and the mgu.

I have the answer for this, but I have no clue how to arrive at the answer nor do I know what the logic behind it is. Can someone explain?

The picture has the answer, I just need to figure out how to do it myself.

[EDIT] Yes, there are several combinations that will yield the same result, the box. However, what is important to me is the thought process and the rules to follow so that I can reproduce this for any set.

• In this example each resolution step is based on the first literal in the clause. Is this a requirement of the task, or just incidental to the known solution (which is just once of many). If it's not a requirement, then different clauses could be resolved first, e.g., $\{R(h(x),x),\lnot Q(x,a)\}$ could be resolved with $\{\lnot P(y,a),Q(y,x)\}$ on the the $Q$ literal. – Joshua Taylor Apr 25 '13 at 0:48

The principle behind resolution is that given two disjunctions, say $p \lor r$ and $\lnot r \lor q$, any model that satisfies both must also satisfy the disjunction $p \lor q$, since if the model satisfies $p \lor r$ by virtue of $r$ being true, then it can't also make $\lnot r \lor q$ true by virtue of $\lnot r$ being true. Similarly, if the model makes $\lnot r$ true, then if it make $p \lor r$ true, it must have made $p$ true. Since either $r$ or $\lnot r$ true, then either $p$ or $q$ must be true, and thus $p \lor q$ true.

For propositional logic, a resolution algorithm starts with a set of clauses and picks a pair of clauses $c_1$ and $c_2$ that contain complementary literals (i.e., one contains some proposition $\phi$ and the other contains $\lnot \phi$) and that have not yet been picked. The algorithm resolves the clauses to form a new clause containing all the literals of $c_1$ and $c_2$ except for $\phi$ and $\lnot \phi$ and adds the new clause to the set of clauses. Any clause containing a literal and its complement (i.e., some $\phi$ and $\lnot \phi$) may immediately be removed the set of clauses, as it is tautologous. This process continues until either an empty clause is derived, in which case the original set of clauses is unsatisfiable, or else there are no more resolvable clauses, which indicates that the original set of clauses is satisfiable.

In the case of predicate logic where clauses contain only ground literals (i.e., no variables), a resolution algorithm can do exactly the same thing. For instance, $\{p(a) \lor q(b)\}$ can be resolved with $\{\lnot q(b) \lor p(b)\}$ to yield $\{p(a) \lor p(b)\}$.

When literals contain variables, however, the process becomes more complicated. Each variable is implicitly universally quantified over each clause, so a clause like $\{p(x) \lor q(x)\}$ means that for every $x$, either $p(x) \lor q(x)$. Consider resolving that clause with, for instance, $\{\lnot p(a)\}$. Both contain a literal on the relation $p$, but the term $a$ is a constant, whereas $x$ is a universally quantified variable. We might attempt to instantiate $\{p(x) \lor q(x)\}$ with $a$ to yield $\{p(a) \lor q(a)\}$ and then resolve this with $\{\lnot p(a)\}$ to yield $\{q(a)\}$. Indeed, this is valid, and $\{q(a)\}$ is a result that we should like to see. The resolution algorithm accomplishes this by finding a unifier for the complementary literals (in this case, $\sigma = [x/a]$), applying it to both clauses, and unifies as in the the propositional case. Of course, this means that it is not sufficient simply to find a literals $p(\dots)$ and $\lnot p(\dots)$; to resolve two clauses, the complementary literals must be unifiable. Since two clauses may use the same variable, renaming of variables may be necessary before two clauses can be resolved.

So, let's take a look at the problem at hand. The set of clauses is:

1. $\{P(x,y), P(f(y),z), Q(x,y)\}$
2. $\{\lnot P(y, a), Q(y, x)\}$
3. $\{R(h(x), x), \lnot Q(x, a)\}$
4. $\{\lnot R(x, y), \lnot R(h(z), y), \lnot Q(z, u)\}$

We start by finding two clauses with unifiable complementary literals, say, 2 and 3, based on the literals $Q(y,x)$ from 2 and $\lnot Q(x,a)$ from 3. The variable $x$ appears in both, so let's rewrite 3 as 3' by replacing $x$ with $z$ to give $\{R(h(z), z), \lnot Q(z,a)$. That takes care of the relabeling. The literals $Q(y,x)$ from 2 and $Q(z,a)$ from 3 (notice we dropped the negation for the purpose of unifying) are unified under the substitution $\sigma = [y/z, x/a]$. (For information on how to find the most general unifier, see, for instance, S. Tanimoto's slides on unification.) Applying $\sigma$ to 2 and 3' gives the clauses

• $\{\lnot P(z,a), Q(z,a)\}$
• $\{R(h(z),z), \lnot Q(z,a)\}$

which can be resolved to get the new clause

$$\{\lnot P(z,a), R(h(z),z) \}$$

Keep doing this, and eventually the empty clause will appear, showing that the initial set is unsatisfiable.

The example I just used performed resolution on two clauses where one literal from each were complementary. That is, 2 contains only one positive literal on $Q$, and 3' contains only one negative literal on $Q$. Some of the resolutions in the example from the question, however, use more than two literals. For instance, in the clauses (after renaming)

• $\{P(x,y), P(f(y),z), Q(x,y)\}$
• $\{\lnot P(y_1,a), Q(y_1,x_1)\}$

there are, for $P$, two positive literals and one negative literal. The most general unifier of these three literals is

$$\sigma = [y/a, z/a, x/f(a), y_1/f(a)]$$

Tanimoto's slides linked above only describe how to find the most general unifier of two literals, but there are plenty of resources out that describe multi-literal unification as well, e.g., Kutsia's slides. It is really just a generalization of the binary case; instead of scanning two literals looking for mismatches, scan all literals. In this case, the set of literals contains

• $P(x,y)$
• $P(f(y),z)$
• $\lnot P(y_1,a)$ (but while scanning, we ignore the negation)

Walking through the entire unification algorithm is a bit tedious, but Kutsia's slides above cover it (along with substitutions and substitution composition) in detail. Intuitively however, the second arguments to $P$ are $y$, $z$, and $a$. Since $a$ is a non-variable term, both $y$ and $z$ must be replaced by $a$, so we expect our substitution to contain $[y/a, z/a]$. If this substitution is in effect, though, the first arguments to $P$ are now $x$, $f(a)$, and $y_1$. Since $f(a)$ is a ground term, and both $x$ and $y_1$ are variables, the substitution must also also contain $[x/f(a), y_1/f(a)]$. Now, the process of combining substitutions (substitution composition) can be tricky, but this is not really one of the tricky cases, and the final substitution is just $[y/a, z/a, x/f(a), y_1/f(a)]$.

As an aside, in other resources on substitutions and unification, authors use different conventions for denoting substitutions, particular whether $[x/y]$ is a substitution that replaces $x$ with $y$, or a substitution that replaces $y$ with $x$. Personally, I'm fond of the $[x/y]$ meaning that $y$ will be replaced with $x$, because of the syntactic parallel with arithmetic, where $(x/y)y$ is $x$, since the $y$'s "cancel out." That's my preference, but it's not universal (as the original question shows), and both are present in the literature.

• Can you explain how the σ of my R1 example came from? σ = [y/a, z/a, x/f(a), y1/f(a)] does not make sense to me. – CharlieK Apr 25 '13 at 4:44
• Not a problem. In the example I worked though, the clauses were resolved based on a single complementary literal from each ($Q(z,a)$ and $\lnot Q(z,a)$). In the example from the question (and I didn't notice this at first), resolution is occurring on multiple literals from the clauses. In $R_1$, both positive literals on $P$ are being used in addition to the negative literal on $P$ from the second clause. The most general unifier, $\sigma$ is being computed for three literals, not just two. I'll update my answer. – Joshua Taylor Apr 25 '13 at 13:07