[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #36

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.

References

[BD87]
Leo Bachmair and Nachum Dershowitz. Inference rules for rewrite-based first-order theorem proving. In Second Symposium on Logic in Computer Science, pages 331–337. IEEE, 1987.
[Hsi85]
Jieh Hsiang. Refutational theorem proving using term-rewriting systems. Artificial Intelligence, 25:255–300, March 1985.
[KN85]
Deepak Kapur and Paliath Narendran. An equational approach to theorem proving in first-order predicate calculus. In Proceedings of the Ninth International Joint Conference on Artificial Intelligence, pages 1146–1153, Los Angeles, CA, August 1985.
[MSA88]
Jürgen Müller and Rolf Socher-Ambrosius. Topics in completion theorem proving. SEKI-Report SR-88-13, Fachbereich Informatik, University of Kaiserslautern, Kaiserslautern, West Germany, 1988. To appear in J. of Symbolic Computation.
[Zha91]
Hantao Zhang. A new strategy for the Boolean ring based approach to first order theorem proving. Technical report, Department of Computer Science, University of Iowa, 1991.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]