Advertisement

Communication Predicates: A Complete Strategy for Resolution-Based Theorems-Provers—an Evaluation of an Implementation

  • E. P. L. Passos
  • R. L. De Carvalho
  • S. R. Peixoto

Abstract

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.

Keywords

Order Logic Current Topic Predicate Symbol Communication Predicate Empty Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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
  2. 2.
    J. A. Robinson, “A Machine-Oriented Logic Based on the Resolution Principle” J. ACM. 12, No. 1, 23–41 (January, 1965).MATHCrossRefGoogle Scholar
  3. 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
  4. 4.
    G. Robinson and D. Carson, “Efficiency and Completeness of the Set of Support Strategy in Theorem-Proving” J. ACM. 12, No. 4, 536–541 (October, 1955).MathSciNetGoogle Scholar
  5. 5.
    R. S. Bover, “Locking: A Restriction of Resolution”, Ph.D. Thesis (The University of Texas at Austin, 1971).Google Scholar
  6. 6.
    C. Chang and R. C. Lee, Symbolic Logic and Mechanical Theorem-Proving (Academic Press, New York, 1973).MATHGoogle Scholar

Copyright information

© The World Organisation of General Systems and Cybernetics 1978

Authors and Affiliations

  • E. P. L. Passos
    • 1
  • R. L. De Carvalho
    • 1
  • S. R. Peixoto
    • 1
  1. 1.Computer Science DepartmentPontificia Universidade CatolicaRio de JaneiroBrazil

Personalised recommendations