Abstract
Two versions of the simplified problem reduction format are compared with locking resolution on some examples. The simplified problem reduction format is a complete strategy which has a goal-subgoal structure and combines features of resolution and natural deduction. Checking subgoals against previously generated subgoals to avoid solving the same subproblems repeatedly was found to be a significant benefit in the simplified problem reduction format. In general, the simplified problem reduction format with checking for repeated subgoals was found to be a better strategy than locking resolution in terms of total computing time used, although the search spaces for locking resolution were often smaller. The smaller search spaces and longer times for locking resolution persisted when the deletion method was replaced by a faster, less powerful deletion method, indicating that the difference with the problem reduction format is not due to the choice of a deletion method. The use of a faster, less powerful deletion method did lead to better performance in the looking resolution prove, however.
This work was partially supported by the National Science Foundation under Grant-MCS 79-04897 and MCS-81-05896.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Andrews, P.B. Theorem proving via general matings. J. ACM 28: 193–214, 1981.
Bledsoe, W.W. Non-resolution theorem proving. Artificial Intelligence 9: 1–35, 1977.
Boyer, R.S. Locking, a restriction of resolution. PhD thesis, University of Taxas at Austin, TX, 1971.
Brand, D. Proving theorems with the modification method. SIAM Journal of Computing 4:412–430, 1975.
Chang, C.L. and Lee, R.C. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
Henschen, L. and Wos, L. Unit refutations and Horn sets. J. ACM 21:590–605, 1974.
Knuth, D.E. and Bendix, P.B. Simple word problems in universal algebras. Pergamon Press, Oxford, 1970.
Lankford, D.S. Canonical algebraic simplification in computational logic. Technical Report ATP-25, University of Texas at Austin, Texas, 1975. Automatic Theorem Proving Project.
Loveland, D.W. and Reddy, C.R. Deleting repeated goals in the problem reduction format. J. ACM 28:646–661, 1981.
Manna, Z. Mathematical Theory of Computation. McGraw-Hill, New York, 1974.
Murray, N.V. Completely non-clausal theorem proving. Artificial Intelligence 18:67–86, 1982.
Pereira, L. Pereira, F. and Warren, D. User's guide to DEC System-10 PROLOG. Technical Report 03/13/5570, Labortorio Nacional De Engenharia Civil, Lisbon, 1978.
Plaisted, D. A simplified problem reduction format. Artificial Intelligence, to appear.
Robinson, G.A. and Wos, L. Paramodulation and theorem proving in first-order theories with equality. American Elsevier, New York, 1969.
Robinson, J.A. Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1:227–234, 1965.
Warren, D.H.D. Efficient processing of interactive relational database queries expressed in logic. Technical Report, Dept. of Artificial Intelligence, University of Edinburgh, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Greenbaum, S., Nagasaka, A., O'Rorke, P., Plaisted, D. (1982). Comparison of natural deduction and locking resolution implementations. In: Loveland, D.W. (eds) 6th Conference on Automated Deduction. CADE 1982. Lecture Notes in Computer Science, vol 138. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000058
Download citation
DOI: https://doi.org/10.1007/BFb0000058
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11558-8
Online ISBN: 978-3-540-39240-8
eBook Packages: Springer Book Archive