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:deciding_quantifier-free_fol_over_ground_terms [2008/05/19 14:04]
vkuncak
sav08:deciding_quantifier-free_fol_over_ground_terms [2015/04/21 17:30] (current)
Line 10: Line 10:
  
 Is the following formula satisfiable ? Is the following formula satisfiable ?
-\[+\begin{equation*}
   a=f(a) \land a \neq b   a=f(a) \land a \neq b
-\++|No. When interpreting variables as constants, two syntactically different terms are different ($a \neq f(a)$).+++\end{equation*} ​++|No. When interpreting variables as constants, two syntactically different terms are different ($a \neq f(a)$).++
  
  
 And the following ? And the following ?
-\[+\begin{equation*}
    ​(f(a)=b \lor (f(f(f(a))) = a \land f(a) \neq f(b))) \land f(f(f(f(a)) \neq b \land b=f(b)    ​(f(a)=b \lor (f(f(f(a))) = a \land f(a) \neq f(b))) \land f(f(f(f(a)) \neq b \land b=f(b)
-\]+\end{equation*}
  
 ===== Axioms for Term Algebras ===== ===== Axioms for Term Algebras =====
  
 Term algebra axioms for function symbols (recall [[Unification]]):​ Term algebra axioms for function symbols (recall [[Unification]]):​
-\[+\begin{equation*}
    ​\forall x_1,​\ldots,​x_n,​y_1,​\ldots,​y_n.\ f(x_1,​\ldots,​x_n)=f(y_1,​\ldots,​y_n) \rightarrow \bigwedge_{i=1}^n x_i=y_i    ​\forall x_1,​\ldots,​x_n,​y_1,​\ldots,​y_n.\ f(x_1,​\ldots,​x_n)=f(y_1,​\ldots,​y_n) \rightarrow \bigwedge_{i=1}^n x_i=y_i
-\]+\end{equation*}
 and and
-\[+\begin{equation*}
    ​\forall x_1,​\ldots,​x_n,​y_1,​\ldots,​y_m.\ f(x_1,​\ldots,​x_n) \neq g(y_1,​\ldots,​y_m)    ​\forall x_1,​\ldots,​x_n,​y_1,​\ldots,​y_m.\ f(x_1,​\ldots,​x_n) \neq g(y_1,​\ldots,​y_m)
-\]+\end{equation*}
 for $g$ and $f$ distinct symbols. for $g$ and $f$ distinct symbols.
  
 Unless the language is infinite, we have that each element is either a constant or is result of application of some function symbols: Unless the language is infinite, we have that each element is either a constant or is result of application of some function symbols:
-\[+\begin{equation*}
    ​\forall x. \bigvee_{f \in {\cal L}} \exists y_1,​\ldots,​y_{ar(f)}.\ x=f(y_1,​\ldots,​y_{ar(f)})    ​\forall x. \bigvee_{f \in {\cal L}} \exists y_1,​\ldots,​y_{ar(f)}.\ x=f(y_1,​\ldots,​y_{ar(f)})
-\]+\end{equation*}
  
 Additional axiom schema for finite terms: Additional axiom schema for finite terms:
-\[+\begin{equation*}
     \forall x. t(x) \neq x     \forall x. t(x) \neq x
-\]+\end{equation*}
 if $t(x)$ is a term containing $x$ but not identical to $x$. if $t(x)$ is a term containing $x$ but not identical to $x$.
  
Line 46: Line 46:
  
 Represent each disequation $t_1 \neq t_2$ as Represent each disequation $t_1 \neq t_2$ as
-\[+\begin{equation*}
    x_1 = t_1 \land x_2 = t_2 \land x_1 \neq x_2    x_1 = t_1 \land x_2 = t_2 \land x_1 \neq x_2
-\]+\end{equation*}
 where $x_1,x_2$ are fresh variables. where $x_1,x_2$ are fresh variables.
  
Line 76: Line 76:
  
 Represent $cons(x,​y)=z$ by  Represent $cons(x,​y)=z$ by 
-\[+\begin{equation*}
     x=car(x) \land y = cdr(z) \land \lnot atom(z)     x=car(x) \land y = cdr(z) \land \lnot atom(z)
-\]+\end{equation*}
 here  here 
   * $atom(x)$ is negation of $Is_{cons}$   * $atom(x)$ is negation of $Is_{cons}$
Line 98: Line 98:
 ===== References ===== ===== References =====
  
-  * [[http://​lara.epfl.ch/​~kuncak/​papers/​KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]],​ see Lemma 25 on page 13+  * [[http://​lara.epfl.ch/​~kuncak/​papers/​KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]],​ see proof of Lemma 25 on page 13 
  
 
sav08/deciding_quantifier-free_fol_over_ground_terms.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice