logic: unification of a formula

Question

apply the unification algorithm to the following two clauses and show how it progresss towards finding a most general unifier or concluding that the clause is not unifiable?

{P(x,y),P(y,f(z))},{P(g(x),y),P(y,y),P(u,f(w))}

can somebody show me how to do it step by step and explain the meaning of it. im a bit lost on this section(about the unifier and general unifier)

by the way im using the book "logic for computer scientists"　by uwe schoning

based on the algorithm in p.84 of the textbook.

this is what i have done: for the clause {P(x,y),P(y,f(z))} i have the substitution as sub=sub[x/y][y/f(z)] and the most general unifier as Lsub={P(f(z),f(z))}

for the second clause {P(g(x),y),P(y,y),P(u,f(w))} i follow the unifier algorithm step1:sub=sub[y/g(x)] and has a result as {P(g(x),g(x)} step2:sub=sub[u/g(x)] and has a result as {P(g(x),f(w)} step3:since non of "f" and "g" is variable. so output non-unifiable

Answer 1

See page 83 :

Now we introduce the predicate logic version of resolution. The new idea is to resolve clauses in predicate logic to clauses in predicate logic where each resolution step is
accompanied by a substitution. These substitutions are performed in a guarded manner.

For example, in the case of the two clauses $\{ P(x), \lnot Q(g(x)) \}$ and $\{ \lnot P(f(y)) \}$, it suffices to use the substitution $[x/f(y)]$ to obtain the resolvent $\{ \lnot Q(g(f(y)) \}$. There is no need at this point to substitute anything for the variable $y$.

The "trick is that with the above subst, we will have :

$\{ P(f(y)), \lnot Q(g(f(y))) \}$ and $\{ \lnot P(f(y)) \}$

so that we have unified the two literals $P(x)$ and $P(f(y))$.

Central for the following investigations is the search for a substitution which unifies two or more literals, i.e., makes them identical. In the above example, $[x/f(y)]$ unifies the two literals $P(x)$ and $P(f(y))$. The substitution $[x/f(a)] [y/a]$ would also be a unifier but does not satisfy the definition of a most general unifier.

In a sense (defined formally below), this substitution makes more substitutions than necessary.

The Unification Algorithm is described at page 84.

You have to recall the resolution calculus [page 29] :

Resolution is a simple syntactic transformation applied to formulas. From two given formulas in a resolution step (provided resolution is applicable to the formulas), a third formula is generated. This new formula can then be used in further resolution steps, and so on. [...] the task is to prove unsatisfiability of a given formula.

In propositional logic, first you transform a formula $F$ in CNF ;

$F = (L_{1,1} \lor ... \lor L_{1,n_1}) \land ... \land (L_{k,1} \lor ... \lor L_{k,n_k})$ ;

the we represent the CNF as sets of clauses where a clause is a set of literals:

$F = \{ \{ L_{1,1},... L_{1,n_1} \}, ... \{ L_{k,1}, ... L_{k,n_k} \} \}$.

The resolution procedure "simplify" the set of clauses until reach an end; if the result of the last step is the empty clause, then the "initial" clause set is unsatisfiable. By property of the CNF, also the initial formula is unsatisfiable.

Thus, if the initial formula was $\varphi$, having shown that it is unsatisfiable, we conclude that $\lnot \varphi$ is a tautology.

In predicate logic, the basic concepts are the same; we say that a formula is valid instead of tautological, but the aim of the procedure is the same : to check if the initial formula is unsatisfiable.

In this case, we start with an initial formula and transform it into RPF; then produce its Skolem formula; recall that [Theorem page 57] :

For each formula $\varphi$ in RPF, $\varphi$ is satisfiable if and only if its Skolem form is satisfiable.

Finally, convert the matrix of the Skolem formula into CNF [see page 60].

From now on, we apply the resolution procedure; in predicate logic it is more complicated, due to the "richer" semantics for f-o language.

We need the Herbrand universe and the Herbrand expansion, and unification, but the goal is the same : transform the clause set in order to find if it is unsatisfiable.

If so, "rewinding" the above process, we have that the Skolem formula is unsat, and thus the RPF is; finally, also the initial formula $\varphi$ is unsat, and thus we conclude that $\lnot \varphi$ is valid.