Abstract
In this paper we present an attempt to abstract from the great diversity of approaches to automated deduction a core collection of operations which are common to all of them. Implementation of this kernel of functions provides a software platform upon which a variety of theorem-proving systems can be built, We outline the architecture for a layered family of software tools to support the development of theorem-proving systems and present in some detail the functions which comprise the two lowest layers. These are the layer implementing primitive abstract data types not supported by the host language and the layer providing primitives for the manipulation of logical formulas. This layer includes the implementation of efficient unification and substitution application algorithms, structure sharing within the formula database, and efficient access to formulas via arbitrary user-defined properties. The tools are provided in a highly portable form (implemented in Pascal) in order that a diverse community of users may build on them.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
W. W. Bledsoe and Larry M, Hines, “Variable elimination and chaining in a resolution-based prover for inequalities,” in Proceedings of the Fifth Conference on Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, v. 87, ed. Robert Kowalski and Wolfgang Bibel, (July 1980).
R. S. Boyer, Locking: a restriction of resolution, Ph.D. Thesis, Univ. of Texas at Austin 1971.
Lawrence Henschen, R. Overbeek, and Lawrence Wos, “Hyperparamodulation: a refinement of paramodulation,” in Proceedings of the Fifth Conference an Automated Deduction, Springer-Verlag Lecture Notes in Computer Science, v. 87, ed. Robert Kowalski and Wolfgang Bibel, (July 1960).
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, v. 87, ed. Robert Kowalski and Wolfgang Bibel, (1980).
E. Lusk and R. Overbeek, Standardizing the external format of formulas, (preprint). September 1980.
E. Lusk and R. Overbeek, “Experiments with resolution-based theorem-proving algorithms,” Computers and Mathematics with Applications, (1981). (to appear)
R. Overbeek, “An implementation of hyper-resolution,” Computers and Mathematics with Applications 1 pp. 201–214 (1975).
S. Winker, “An evaluation of an implementation of qualified hyperresolution,” IEEE Transactions on Computers C-25(8) pp. 835–843 (August 1976).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lusk, E.L., McCune, W.W., Overbeek, R.A. (1982). Logic machine architecture: Kernel functions. 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/BFb0000052
Download citation
DOI: https://doi.org/10.1007/BFb0000052
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