Abstract
The Interactive Theorem Prover (ITP), an environment that supports research into the theory and application of automated reasoning, is described. ITP is an interactive system providing convenient access to and control of the many inference mechanisms of Logic Machine Architecture (LMA), described elsewhere, LMA itself has been substantially enhanced since the last report on its status, and we describe here some of the enhancements, particularly the addition of a tightly-coupled logic programming component, which provides an integration of the theorem-proving and logic programming approaches to problems represented in the predicate calculus.
This work was partially supported by the Applied Mathematical Sciences Research Program (KC-04-02) of the Office of Energy Research of the U.S. Department of Energy under Contract W-31-109-Eng-38, and also by National Science Foundation grant MCS82-07496.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
W. F. Clocksin and C. S. Mellish, Programming in Prolog, Springer-Verlag, New York (1981).
E. Lusk, William McCune, and R. Overbeek, “Logic Machine Architecture: inference mechanisms,” pp. 85–108 in Proceedings of the Sixth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 138, ed. D. W. Loveland,Springer-Verlag, New York ().
E. Lusk and R. Overbeek, “Data structures and control architecture for the implementation of theorem-proving programs,” in Proceedings of the Fifth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 87, ed. Robert Kowalski and Wolfgang Bibel, ().
E. Lusk, William McCune, and R. Overbeek, “Logic machine architecture: kernel functions,” pp. 70–84 in Proceedings of the Sixth Conference on Automated Deduction, Springer-verlag Lecture. Notes in Computer Science, vol. 138, ed. D. W. Loveland,Springer-Vertag, New York (1982).
Ewing L. Lusk and Ross A. Overbeek, “An LMA-based theorem prover,” ANL-82-75, Argonne National Laboratory (December, 1982).
Ewing L. Lusk and Ross A. Overbeek, “Logic Machine Architecture inference mechanisms — layer 2 user reference manual,” ANL-82-84, Argonne National Laboratory (December, 1982).
J. McCharen, R. Overbeek, and L. Wos, “Complexity and related enhancements for automated theorem-proving programs,” Camputers and Mathematics with Applications 2 pp, 1–16 (1976).
S. Winker and L. Wos, “Procedure implementation through demodulation and related tricks,” pp. 109–131 in Proceedings of the Sixth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, Vol. 138, ed. D. W. Loveland,Springer-Verlag, New York (1982).
L. Wos, G. Robinson, D. Carson, and L. Shalla, “The concept of demodulation in theorem proving,” Journal of the ACM 14 pp, 698–704 (1967).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lusk, E.L., Overbeek, R.A. (1984). A Portable Environment for Research in Automated Reasoning. In: Shostak, R.E. (eds) 7th International Conference on Automated Deduction. CADE 1984. Lecture Notes in Computer Science, vol 170. Springer, New York, NY. https://doi.org/10.1007/978-0-387-34768-4_2
Download citation
DOI: https://doi.org/10.1007/978-0-387-34768-4_2
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-96022-7
Online ISBN: 978-0-387-34768-4
eBook Packages: Springer Book Archive