The Linked Inference Principle, II: The User’s Viewpoint
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 , 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.
- 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
- Warren, D. H. D., Implementing Prolog — compiling predicate logic programs, DAI Research Reports 39 & 40, University of Edinburgh, May 1977.Google Scholar
- 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
- 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
- Wos, L., Smith, B. and Veroff, R., “The Linked Inference Principle, I: The Formal Treatment,” in preparation.Google Scholar