[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: H. Zhang
Date: April 1991
Summary: Find more restrictive strategies in Boolean-ring based methods for resolution-like first-order theorem proving.
Since the work of Hsiang [Hsi85], several Boolean-ring based methods have been proposed for resolution-like first-order theorem proving. In [KN85], superposition rules were defined using multiple overlaps (requiring unifications of products of atoms). It is unknown whether single overlaps (requiring only unifications of atoms) are sufficient in these inference rules. Also, it is not known if unifications of maximal atoms (under a given term ordering) suffice. (The same problem for Hsiang’s method was solved positively in [MSA88][Zha91].) In other respects, too, the set of inference rules in [BD87, KN85] may be larger than necessary and the simplification weaker than possible.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |