[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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?
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |