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/27 17:26] damien |
sav08:deciding_quantifier-free_fol_over_ground_terms [2008/05/19 14:04] vkuncak |
||
|---|---|---|---|
| Line 95: | 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 Lemma 25 on page 13 | ||
| + | |||