Lab for Automated Reasoning and Analysis 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.
 
sav08/unification.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice