Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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