• English only

# 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)
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