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

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

Problem #42 (Solved !)

Originator: Hubert Comon
Date: April 1991

Summary: Can negations be effectivly eliminated from first-order formulas over trees, where equality is the only predicate?

Given a first-order formula with equality as the only predicate symbol, can negation be effectively eliminated from an arbitrary formula φ when φ is equivalent to a positive formula? Equivalently, if φ has a finite complete set of unifiers, can they be computed? Special cases were solved in [Com88, LM87].

Remark

A positive solution is given in [Taj93].

References

[Com88]

Hubert Comon. Unification et Disunification: Théorie et Applications. PhD thesis, Institut National Polytechnique de Grenoble, 1988. In French.

[LM87]

J.-L. Lassez and K. G. Marriott. Explicit representation of terms defined by counter examples. Journal of Automated Reasoning, 3(3):1–17, September 1987.

[Taj93]

Mohamed Tajine. Negation elimination for syntactic equational formula. In Claude Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, pages 316–327, Montreal, Canada, June 1993. Springer-Verlag.

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

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