Communication Predicates: A Complete Strategy for Resolution-Based Theorems-Provers—an Evaluation of an Implementation
A new and complete strategy for resolution-based theorem-provers for first order logic is presented. This strategy is a central result in Bledsoe(1). The strategy extends Bledsoe’s splitting technique, which consists of the replacement of a set SU C 1 v C 2 of clauses. We extend it in the following senses: (a) It enlarges the range of applications by allowing to split sets of clauses, and (b) It allows the occurrence of common variables in the split parts. The new strategy is implemented and is presented from a practical point of view. The examples illustrating the effects of the strategy are discussed.
KeywordsOrder Logic Current Topic Predicate Symbol Communication Predicate Empty Clause
Unable to display preview. Download preview PDF.
- 1.W. W. Bledsoe, “Splitting and Reduction Heuristics in Automatic Theorem-Proving Artificial Intelligence” pp. 55-77 (Feb., 1971); R. L. de Carvalho, Some Results in Automatic Theorem-Proving with Applications in Elementary Set Theory and Topology (University of Toronto, 1974).Google Scholar
- 3.G. Robinson, L. Wos and D. Carson, “The Unit Preference Strategy in Theorem Proving” AFIPS Conference Proceedings 26, (Spartan Books, Washington, D.C., 1969), pp. 615–621.Google Scholar
- 5.R. S. Bover, “Locking: A Restriction of Resolution”, Ph.D. Thesis (The University of Texas at Austin, 1971).Google Scholar