# Differences

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

 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) Both sides previous revision Previous revision 2008/05/19 14:08 vkuncak 2008/05/19 14:04 vkuncak 2008/05/19 14:04 vkuncak 2008/04/27 17:26 damien 2008/04/25 14:06 vkuncak 2008/04/23 15:10 vkuncak 2008/04/23 11:07 vkuncak 2008/04/23 11:07 vkuncak 2008/04/23 09:10 vkuncak 2008/04/23 09:03 vkuncak 2008/04/23 08:37 vkuncak 2008/04/23 08:36 vkuncak 2008/04/23 08:33 vkuncak 2008/04/23 08:32 vkuncak 2008/04/17 13:48 vkuncak 2008/04/17 13:48 vkuncak 2008/04/17 13:08 vkuncak 2008/04/17 13:07 vkuncak 2008/04/17 13:06 vkuncak created Next revision Previous revision 2008/05/19 14:08 vkuncak 2008/05/19 14:04 vkuncak 2008/05/19 14:04 vkuncak 2008/04/27 17:26 damien 2008/04/25 14:06 vkuncak 2008/04/23 15:10 vkuncak 2008/04/23 11:07 vkuncak 2008/04/23 11:07 vkuncak 2008/04/23 09:10 vkuncak 2008/04/23 09:03 vkuncak 2008/04/23 08:37 vkuncak 2008/04/23 08:36 vkuncak 2008/04/23 08:33 vkuncak 2008/04/23 08:32 vkuncak 2008/04/17 13:48 vkuncak 2008/04/17 13:48 vkuncak 2008/04/17 13:08 vkuncak 2008/04/17 13:07 vkuncak 2008/04/17 13:06 vkuncak created 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