[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Franz Baader, Klaus Schulz
Date:
Summary: Is there an equational theory for which unification with constants is decidable, but general unification is undecidable?
Is there an equational theory for which unification with constants is decidable, but general unification (where free function symbols of arbitrary arity may occur) is undecidable? From the results in [BS92] it follows that this question can be reformulated as follows: Is there an equational theory for which unification with constants is decidable, but unification with linear constant restrictions is undecidable? Another way of formulating the question is: Consider positive first-order formulæ containing equality as the only predicate symbol, and function symbols from a given alphabet F. Is there an equational theory E with alphabet F such that whether E ⊨ φ is decidable for closed formulae φ with quantifier prefix ∀^{∗}∃^{∗}, but undecidable for arbitrary quantifier prefixes?
This has been answered in the affirmative [Oto12] by exhibiting such an equational theory.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |