Abstract
We present an outline of the principal features of an on-line interactive theorem-proving program, and a brief account of the results of some experiments with it. This program has been used to obtain proofs of new mathematical results recently announced without proof in the Notices of the American Mathematical Society.
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
Andrews, P.B. (1968) Resolution with merging. J. Ass. comput. Mach., 15, 367–81.
Chinthayamma (1969) Sets of independent axioms for a ternary Boolean algebra. Notices of Amer. Math. Soc.. 16, 69T-A69, 654.
Grau, A.A. (1947) Ternary Boolean Algebra. Bull. Amer. Math. Soc., 53, 567–72.
Green, C. & Raphael, B. (1968) The use of theorem-proving techniques in question-answering, Proc. 23rd National Conference ACM. Washington, D.C.: Thompson Book Co.
Guard, J.R., Oglesby, F.C., Bennett, J.H. & Settle, L.G. (1969) Semi-automated mathematics. J. Ass. comput. Mach., 16, 49–62.
Kieburtz, R. & Luckham, D. (1969) Compatibility of Refinements of the Resolution Principle (in press).
Loveland, D. (1969) A linear format for resolution. Proceedings IRIA Symposium on Automatic Demonstration. Versailles, France, December 1968. Springer-Verlag (in press)
Luckham, D. (1967) The resolution principle in theorem-proving. Machine Intelligence I, (eds Collins, N.L. & Michie, D.). Edinburgh: Oliver and Boyd.
Luckham, D. (1968) Some tree-paring strategies for theorem-proving. Machine Intelligence 3, pp. 95–112 (ed. Michie, D.). Edinburgh: Edinburgh University Press.
Luckham, D. (1969) Refinement theorems in resolution theory. Proceedings IRIA Symposium on Automatic Demonstration. Versailles, France, December 1968. Springer-Verlag (in press).
Luckham, D. & Nilsson, N. (1969) On extracting information from resolution proof trees. Stanford Artificial Intelligence Project Memo (in press).
Robinson, J.A. (1965a) A machine-oriented logic based on the resolution principle. J. Ass. comput. Mach., 12, 23–41.
Robinson, J.A. (1965b) Automatic deduction with hyper-resolution. International Journal of computer Mathematics, 1, 227–34.
Wos, L., Robinson, G., & Carson, D. (1965) Efficiency and completeness of the set of support strategy in theorem-proving. J. Ass. comput. Mach., 12, 536–41.
Wos, L., Robinson, G., Carson, D. & Shalla, L. (1967) The concept of demodulation in theorem-proving. J. Ass. comput. Mach., 14, 698–704.
Wos, L. & Robinson, G. (1969) Paramodulation and set of support. Proceedings IRIA Symposium on Automatic Demonstration. Versailles, France, December, 1968, Springer-Verlag (in press).
Reference cited
Luckham, D.C., Morales, J.J., and Schreiber, J.F., “AStudy in the Application of Theorem Proving”. Proceedings of the Conference on Artifial Intelligence and Simulation of Behavior, Hamburg, Germany. July 1978, pp.176–188.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1983 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Allen, J., Luckham, D. (1983). An Interactive Theorem-Proving Program. In: Siekmann, J.H., Wrightson, G. (eds) Automation of Reasoning. Symbolic Computation. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-81955-1_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-81955-1_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-81957-5
Online ISBN: 978-3-642-81955-1
eBook Packages: Springer Book Archive