Differences
This shows you the differences between two versions of the page.
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 |