Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:deciding_quantifier-free_fol_over_ground_terms [2008/04/23 15:10] vkuncak |
sav08:deciding_quantifier-free_fol_over_ground_terms [2008/04/27 17:26] damien |
||
---|---|---|---|
Line 9: | Line 9: | ||
Can we treat variables as constants in this case? | Can we treat variables as constants in this case? | ||
- | Is the following formula satisfiable | + | Is the following formula satisfiable ? |
\[ | \[ | ||
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)$).++ |
- | is the following | + | |
+ | |||
+ | And the following ? | ||
\[ | \[ | ||
(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) | ||
Line 55: | Line 57: | ||
**Theorem:** Let $E$ be a set of equations and disequations where disequations are only between variables. Let $E^+ = \{ (t_1 \doteq t_2) \mid (t_1 = t_2) \in E \}$ the unification problem for equations in $E$. Then | **Theorem:** Let $E$ be a set of equations and disequations where disequations are only between variables. Let $E^+ = \{ (t_1 \doteq t_2) \mid (t_1 = t_2) \in E \}$ the unification problem for equations in $E$. Then | ||
* if $E^+$ has no unifier, the set $E$ is unsatisfiable over ground terms; | * if $E^+$ has no unifier, the set $E$ is unsatisfiable over ground terms; | ||
- | * if $E^+$ has a unifier, if the language contains at least one function symbol of arity at least one (i.e. the set of ground terms is infinite) then $E$ is satisfiable. | + | * if $E^+$ has a most general unifier $\sigma$ such that for all $(x \neq y) \in E$ we have $\sigma(x) \neq \sigma(y)$, then if the language contains at least one function symbol of arity at least one (i.e. the set of ground terms is infinite) then $E$ is satisfiable. |
Note: we need assumption that there are infinitely many terms, consider for example ${\cal L} = \{ a,b\}$ and formula $x \neq y \land x \neq z \land y \neq z$. | Note: we need assumption that there are infinitely many terms, consider for example ${\cal L} = \{ a,b\}$ and formula $x \neq y \land x \neq z \land y \neq z$. | ||
Line 93: | Line 95: | ||
* if we have no predicates: theory is decidable, using quantifier elimination (these structures are called "term algebras", see [[List of Theories Admitting QE]]) | * if we have no predicates: theory is decidable, using quantifier elimination (these structures are called "term algebras", see [[List of Theories Admitting QE]]) | ||
* if we have predicates: this is satisfiability in Herbrand models, equivalent to satisfiability in FOL without equality, so it is undecidable | * if we have predicates: this is satisfiability in Herbrand models, equivalent to satisfiability in FOL without equality, so it is undecidable | ||
- |