[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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].
A positive solution is given in [Taj93].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |