Abstract
A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete for the full first-order predicate calculus. It differs from Prolog in its use of unification with the occurs check for soundness, the model-elimination reduction rule that is added to Prolog inferences to make the inference system complete, and consecutively bounded depth-first search instead of unbounded depth-first search to make the search strategy complete. A Prolog technology theorem prover has been implemented by an extended Prolog-to-Lisp compiler that supports these additional features. It is capable of proving theorems in the full first-order predicate calculus at a rate of thousands of inferences per second.
Preparation of this paper was supported by the Defense Advanced Research Projects Agency under Contract N00039-84-K-0078 with the Naval Electronic Systems Command. The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the United States government. Approved for public release. Distribution unlimited.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Boyer, R.S. and J.S. Moore. The sharing of structure in theorem-proving programs. In B. Meltzer and D. Michie (eds.). Machine Intelligence 7. Edinburgh University Press, Edinburgh, Scotland, 1972.
Chang, C.L. and R.C.T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, New York, 1973.
Cohen, J. Describing Prolog by its interpretation and compilation. Communications of the ACM 28, 12 (December 1985), 1311–1324.
Colmerauer, A. Prolog and infinite trees. In Clark, K.L. and S.A. Tarnlund (eds.). Logic Programming. Academic Press, New York, New York, 1982.
Fleisig, S., D. Loveland, A.K. Smiley III, and D.L. Yarmush. An implementation of the model elimination proof procedure. Journal of the ACM 21, 1 (January 1974), 124–139.
Korf, R.E. Depth-first iterative-deepening: an optimal admissible tree search. Artificial Intelligence 27, 1 (September 1985), 97–109.
Lawrence, J.D. and J.D. Starkey. Experimental tests of resolution based theorem-proving strategies. Technical Report, Computer Science Department, Washington State University, Pullman, Washington, April 1974.
Loveland, D.W. A simplified format for the model elimination procedure. J. ACM 16, 3 (July 1969), 349–363.
Loveland, D.W. Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam, the Netherlands, 1978.
Loveland, D.W. and M.E. Stickel. The hole in goal trees: some guidance from resolution theory. IEEE Transactions on Computers C-25, 4 (April 1976), 335–341.
Lusk, E.L., W.W. McCune, and R.A. Overbeek. Logic Machine Architecture: kernel functions. Proceedings of the 6th Conference on Automated Deduction, New York, New York, June 1982, 70–84.
Lusk, E.L., W.W. McCune, and R.A. Overbeek. Logic Machine Architecture: inference mechanisms. Proceedings of the 6th Conference on Automated Deduction, New York, New York, June 1982, 85–108.
Lusk, E.L. and R.A. Overbeek. A portable environment for research in automated reasoning. Proceedings of the 7th Conference on Automated Deduction, Napa, California, May 1984, 43–52.
Michie, D., R. Ross, and G.J. Shannan. G-deduction. In B. Meltzer and D. Michie (eds.). Machine Intelligence 7. John Wiley and Sons, New York, New York, 1972, pp. 141–165.
Nilsson, N.J. Principles of Artificial Intelligence. Tioga Publishing Co., Palo Alto, California, 1980.
Plaisted, D.A. The occur-check problem in Prolog. New Generation Computing 2, 4 (1984), 309–322.
Reboh, R., B. Raphael, R.A. Yates, R.E. Kling, and C. Velarde. Study of automatic theorem-proving programs. Technical Note 72, Artificial Intelligence Center, SRI International, Menlo Park, California, November 1972.
Shostak, R.E. Refutation graphs. Artificial Intelligence 7, 1 (Spring 1976), 51–64.
Stickel, M.E. A Prolog technology theorem prover. New Generation Computing 2, 4 (1984), 371–383.
Stickel, M.E. and W.M. Tyson. An analysis of consecutively bounded depth-first search with applications in automated deduction. Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, California, August 1985, 1073–1075.
Warren, D.H.D. An abstract Prolog instruction set. Technical Note 309, Artificial Intelligence Center, SRI International, Menlo Park, California, October 1983.
Wilson, G.A. and J. Minker. Resolution, refinements, and search strategies: a comparative study. IEEE Transactions on Computers C-25, 8 (August 1976), 782–801.
Wos, L.T. Unpublished notes, Argonne National Laboratory, about 1965.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stickel, M.E. (1986). A prolog technology theorem prover: Implementation by an extended prolog compiler. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_122
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_122
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive