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

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

Problem #67

Originator: Franz Baader, Klaus Schulz [BS92]
Date: June 1993

Summary: Investigate the exact difference between linear constant restrictions and arbitrary constant restrictions in unification problems.

It was shown in [BS92] that being able to solve unification problems with linear constant restrictions is a necessary and sufficient condition for the possibility of combining unification algorithms. Other approaches [SS89][Bou90] require solvability of constant elimination problems, which was shown to be equivalent to presupposing solvability of unification problems with arbitrary constant restrictions [BS92]. Is there an equational theory for which solvability of unification problems with linear constant restrictions is decidable, but solvability of unification problems with arbitrary constant restrictions is undecidable? Is there an equational theory for which unification problems with linear constant restrictions always have a finite complete set of solutions, but unification problems with arbitrary constant restrictions sometimes don’t?

References

[Bou90]

Alexandre Boudet. Unification in combination of equational theories: An efficient algorithm. In Proceedings of the Tenth International Conference on Automated Deduction (Kaiserslautern, Germany), volume 449 of Lecture Notes in Computer Science. Springer-Verlag, 1990.

[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.

[SS89]

Manfred Schmidt-Schauß. Combination of unification algorithms. Journal of Symbolic Computation, 8, 1989.

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

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