[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #66 (Solved !)

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?

Remark

This has been answered in the affirmative [Oto12] by exhibiting such an equational theory.

References

[BS92]

Franz Baader and Klaus Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Computer Science, Saratoga Springs, NY, June 1992. Springer-Verlag.

[Oto12]

Jan Otop. E-unification with constants vs. general E-unification. Journal of Automated Reasoning, 48(3):363–390, March 2012.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]