← All problems
Unverified

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

The source page states the original problem together with its recorded qualifications and progress updates as follows.

It was shown in [Franz Baader, 1993] 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 [Franz Baader, 1993] require solvability of constant elimination problems, which was shown to be equivalent to presupposing solvability of unification problems with arbitrary constant restrictions [Franz Baader, 1993]. 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?

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu