LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:unification [2008/04/02 20:30]
vkuncak
sav08:unification [2015/04/21 17:30] (current)
Line 9: Line 9:
   * equation $x \doteq t(x)$ where $t$ is a term containing $x$ but not identical to $x$ ++| is contradictory++   * equation $x \doteq t(x)$ where $t$ is a term containing $x$ but not identical to $x$ ++| is contradictory++
  
-===== Unification ​Examples =====+===== Examples =====
  
 First-order language: First-order language:
Line 19: Line 19:
 **Example 1** **Example 1**
  
-\[+\begin{equation*}
   R(x,f(x,y)) \doteq R(f(a,​v),​f(f(u,​b),​f(u,​u)))   R(x,f(x,y)) \doteq R(f(a,​v),​f(f(u,​b),​f(u,​u)))
-\]+\end{equation*}
  
 **Example 2** **Example 2**
  
-\[+\begin{equation*}
   R(x,f(x,x)) \doteq R(f(a,​v),​f(f(u,​b),​f(u,​u)))   R(x,f(x,x)) \doteq R(f(a,​v),​f(f(u,​b),​f(u,​u)))
-\]+\end{equation*}
  
 **Example 3** **Example 3**
  
-\[+\begin{equation*}
   R(x,f(x,y)) \doteq R(f(u,v),v)   R(x,f(x,y)) \doteq R(f(u,v),v)
-\]+\end{equation*}
  
 **Definition:​** Unifier of a set $E$ of syntactic equations is a substitution that makes all equations true. **Definition:​** Unifier of a set $E$ of syntactic equations is a substitution that makes all equations true.
Line 52: Line 52:
  
 A set of equations is in //solved form// if it is of the form $\{ x_1 \doteq t_1,\ldots, x_n \doteq t_n \}$ iff variables $x_i$ do not appear in terms $t_j$, that is A set of equations is in //solved form// if it is of the form $\{ x_1 \doteq t_1,\ldots, x_n \doteq t_n \}$ iff variables $x_i$ do not appear in terms $t_j$, that is
-\[+\begin{equation*}
    ​\{x_1,​\ldots,​x_n \} \cap (FV(t_1) \cup \ldots FV(t_n)) = \emptyset    ​\{x_1,​\ldots,​x_n \} \cap (FV(t_1) \cup \ldots FV(t_n)) = \emptyset
-\]+\end{equation*}
  
 We obtain a solved form in finite time using the non-deterministic algorithm that applies the following rules as long as no clash is reported and as long as the equations are not in solved form. We obtain a solved form in finite time using the non-deterministic algorithm that applies the following rules as long as no clash is reported and as long as the equations are not in solved form.