How does kommutation affect unification in first oder predicate logic

123 Views Asked by At

This was asked on an exam last semester. I know that my algorithm fails in this case, or does it not? because of the function being not the same like $g(f(x))=f(g(x))$.

The problem: given by 2 lists $(s_1,\dots,s_n)$ and $(t_1,\dots,t_n)$ can be seen as solving a system of equations $$\Gamma=[s_1=t_1,\dots ,s_n=t_n]$$

This can be done by the following rules that were similarly formulated by J. Herbrand in 1930.

  • $x, y, z_i$ are variables

  • $a,b$ constance

  • $p_i,q_i,s$ and $s_i$ are arbitrary terms.

  • $t$ is a term and not a variable

  1. remove every equation $s=s$ in $\Gamma$

  2. replace every equation $f(p_1,\dots,p_n)=f(q_1,\dots, q_n)$ with $p_1=q_1\dots,p_n=q_n$

  3. for every equation $x=s$, for which $x$ is not under the variables of Term $s$, substitute every other occurrence of $x$ in $\Gamma$ with $s$.

  4. replace every eqation $t=x$ with $x=t$.

  5. if there is an equation like $a=b$ in $\Gamma$, there is no solution.

  6. if there is an equation like $f(p_1,\dots,p_n)=g(q_1,\dots,q_n)$ in $\Gamma$, there is no solution.

  7. if there is an equation like $f(p_1,\dots,p_n)=a$ or $a=f(p_1,\dots,p_n)$ in $\Gamma$, there is no solution.

  8. if there is an equation like $x=t$ in $\Gamma$ where $x$ occurs in $t$ there is no solution

The system is solved when it only consists of $z_i=s_i (i=1,...,k)$ where $z_i$ doesn't occur else in $\Gamma$. Then the unificator of the 2 lists ist the substitution $\{z_1\leftarrow s_1,\dots,z_k\leftarrow s_k\}$