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/04/25 14:06] vkuncak |
sav08:deciding_quantifier-free_fol_over_ground_terms [2008/05/19 14:08] vkuncak |
||
|---|---|---|---|
| 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 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 | ||
| + | |||
| + | ===== References ===== | ||
| + | |||
| + | * [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]], see proof of Lemma 25 on page 13 | ||
| + | |||
| + | |||