Abstract
We discuss a sequent style clause-based proof system that supports several important strategies in automatic theorem proving. The system has a goal-subgoal structure and supports back chaining with caching; it permits semantic deletion, sometimes using multiple models; it is also a genuine set of support strategy; and it is complete for first order logic in clause form.
This work was supported in part by the National Science Foundation under grant DCR-8516243.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Ballantyne, A. and W.W. Bledsoe, "On Generating and Using Examples in Proof Discovery", Machine Intelligence, V 10, pp. 3–39, Harwood, Chichester 1982.
Bibel, W., "Automated Theorem Proving", Friedr. Vieweg & Sohn Verlagsgesellschaft MbH, Braunschweig 1982.
Bledsoe, W.W., "Using Examples to Generate Instantiations for Set Variables", Technical Report No. ATP-67, Department of Computer Science, University of Texas at Austin, July 1982.
Boyer, R., "Locking: A Restriction of Resolution", Ph.D. dissertation, University of Texas at Austin, Austin, TX, 1970.
Gelernter, H., "Realization of a Geometry Theorem-Proving Machine", Proc. ICIP, pp. 273–282, Paris UNESCO House, 1959.
Loveland, D.W., "A Simplified Format for the Model Elimination Theorem-Proving Procedure", J. ACM, Vol. 16, No. 3, pp. 349–363, July 1969.
Luckham, D., "Refinement Theorems in Resolution Theory", Proc. IRIA Symp. Automatic Demonstration, Versailles, France, 1968, Springer-Verlag, New York, pp. 163–190, 1970.
Plaisted, D.A., "Non-Horn Clause Logic Programming Without Contrapositives", Journal of Automated Reasoning, Vol. 4, Nov. 3, September 1988.
Reiter, R., "A Semantically Guided Deductive System for Automatic Theorem Proving", IEEE Transaction on Computers, Vol. C-25, No. 4, pp. 328–334, April 1976.
Robinson, J.A., "A Machine-oriented Logic Based on the Resolution Principles", JACM 12, pp. 23–41, 1965.
Sandford, D.M., "Using Sophisticated Models in Resolution Theorem Proving", Lecture Notes in Computer Science, No. 90, G. Goos and J. Hartmanis eds, Springer-Verlag, 1980.
Slagle, J.R., "Automatic Theorem Proving with Renamable and Semantics Resolution", JACM, Vol. 14, No. 4, pp. 687–697, October 1967.
Stickel, M.E., "A PROLOG Technology Theorem Prover", Journal of Automated Reasoning, Vol. 4, No. 4, pp. 353–380, 1988.
Walther, C., "A Mechanical Solution of Schubert's Steamroller by Manysorted Resolution", Proc. 8th AAAI, pp. 330–334, 1984.
Wang, T.C., "Designing Examples for Semantically Guided Hierarchical Deduction", Proc. of IJCAI, pp. 1201–1207, 1985.
Wang, T.C. and W.W. Bledsoe, "Hierarchical Deduction", Journal of Automated Reasoning, Vol. 3, No. 1, 1987.
Wos, L.T., G.A. Robinson and D.F. Carson, "Efficiency and Completeness of the Set of Support Strategy in Theorem Proving", J. of ACM, Vol. 12, No. 4, October 1965.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nie, X., Plaisted, D.A. (1990). A complete semantic back chaining proof system. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_76
Download citation
DOI: https://doi.org/10.1007/3-540-52885-7_76
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52885-2
Online ISBN: 978-3-540-47171-4
eBook Packages: Springer Book Archive