The Linked Inference Principle, II: The User’s Viewpoint

  • L. Wos
  • R. Veroff
  • B. Smith
  • W. McCune
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


In the field of automated reasoning, the search continues for useful representations of information, for powerful inference rules, for effective canonlcallzatlon procedures, and for intelligent strategies. The practical objective of this search is, of course, to produce ever more powerful automated reasoning programs. In this paper, we show how the power of such programs can be sharply increased by employing inference rules called linked inference rules. In particular, we focus on linked UR-resolutlon, a generalization of standard UR-resolution [2], and discuss ongoing experiments that permit comparison of the two inference rules. The intention is to present the results of those experiments at the Seventh Conference on Automated Deduction. Much of the treatment of linked inference rules given in this paper is from the user’s viewpoint, with certain abstract considerations reserved for Section 3.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Luckham, D. C., “Some Tree-paring Strategies for Theorem Proving,” Machine Intelligence 3 (ed. Michle, D.), Edinburgh University Press 1968, pp. 95–112.Google Scholar
  2. [2]
    McCharen, J., Overbeek, R. and Wos, L., “Problems and experiments for and with automated theorem proving programs,” IEEE Transactions on Computers, Vol. C-25(1976), pp. 773–782.CrossRefzbMATHGoogle Scholar
  3. [3]
    Robinson, J., “A machlne-orlented logic based on the resolution principle,” J. ACM, Vol. 12(1965), pp. 23–41.CrossRefGoogle Scholar
  4. [4]
    Warren, D. H. D., Implementing Prolog — compiling predicate logic programs, DAI Research Reports 39 & 40, University of Edinburgh, May 1977.Google Scholar
  5. [5]
    Wojclechowski, W. and Wojcik, A., “Automated design of multlple-valued logic circuits by automatic theorem proving teehnlques,” to appear in IEEE Transactions on Computers.Google Scholar
  6. [6]
    Wos, L., Carson, D. and Robinson, G., “The unit preference strategy in theorem proving,” Proc. AFIPS 1964 Fall Joint Computer Conference, Vol. 26, Part II, pp. 615–621 (Spartan Books, Washington, D.C.).Google Scholar
  7. [7]
    Wos, L., Carson, D. and Robinson, G., “Efficiency and completeness of the set of support strategy in theorem proving,” J. ACM, Vol. 12(1965), pp. 536–541.MathSciNetCrossRefzbMATHGoogle Scholar
  8. [8]
    Wos, L., Smith, B. and Veroff, R., “The Linked Inference Principle, I: The Formal Treatment,” in preparation.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • L. Wos
    • 1
  • R. Veroff
    • 2
  • B. Smith
    • 1
  • W. McCune
    • 3
  1. 1.Mathematics and Computer Science DivisionArgonne National LaboratoryArgonne
  2. 2.Department of Computer ScienceUniversity of New MexicoAlbuquerque
  3. 3.Department of Electrical Engineering and Computer ScienceNorthwestern UniversityEvanston

Personalised recommendations