Abstract
This paper reports on a combination of two research efforts, the Prolog Technology Theorem Prover (PTTP), and theory resolution in the guise of linked inference. Both received a great deal of encouragement and support over the years from Woody Bledsoe, by personal discussions and by his inviting me to discuss these topics with his students and colleagues at the University of Texas and MCC. He also invited me to cochair with him an AAAI workshop on the encompassing topic of high-performance theorem proving at Stanford in 1989.
This research was supported by the National Science Foundation under Grant CCR8922330. 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 National Science Foundation or the United States government.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Butler, E. Lusk, W. McCune, and R. Overbeek (1986): Paths to High-Performance Automated Theorem Proving. 8th International Conference on Automated Deduction, Oxford, England, 588–597.
D. W. Loveland (1969): A Simplified Format for the Model Elimination Procedure. Journal of the ACM 16(3), 349–363.
D. W. Loveland (1978): Automated Theorem Proving: A Logical Basis. Amsterdam: North-Holland.
W. W. McCune (1990): OTTER 2.0 Users Guide, Technical Report ANL90/9, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL.
D. A. Plaisted (1988): Non-Horn Clause Logic Programming Without Contrapositives. Journal of Automated Reasoning 4(3), 287–325.
M. E. Stickel (1985): Automated Deduction by Theory Resolution. Journal of Automated Reasoning 1(4), 333–355.
M. E. Stickel (1988a): A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Journal of Automated Reasoning 4(4), 353–380.
M. E. Stickel (1988b): A Prolog-Like Inference System for Computing Minimum-Cost Abductive Explanations in Natural-Language Interpretation. International Computer Science Conference ‘88, Hong Kong, 343–350.
M. E. Stickel (1990): A Prolog Technology Theorem Prover: a New Exposition and Implementation in Prolog. International Symposium on Design and Implementation of Symbolic Computation Systems, Capri, Italy, 154–163.
M. Tarver (1990): An Examination of the Prolog Technology Theorem Prover. 10th International Conference on Automated Deduction, Kaiserslautern, W. Germany, 322–335.
R. Veroff and L. Wos (to appear): The Linked Inference Principle, I: The Formal Treatment. Journal of Automated Reasoning.
L. Wos, R. Overbeek, and R. Lusk (1991): Subsumption, A Sometimes Undervalued Procedure. In: J.-L. Lassez and G. Plotkin, eds.: Computational Logic, Essays in Honor of Alan Robinson. Cambridge, MA: MIT Press.
L. Wos, R. Veroff, B. Smith, and W. McCune (1984): The Linked Inference Principle, II: The User’s Viewpoint. 7th International Conference on Automated Deduction, Napa, CA, 316–332.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Stickel, M.E. (1991). PTTP and Linked Inference. In: Boyer, R.S. (eds) Automated Reasoning. Automated Reasoning Series, vol 1. Springer, Dordrecht. https://doi.org/10.1007/978-94-011-3488-0_14
Download citation
DOI: https://doi.org/10.1007/978-94-011-3488-0_14
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-5542-0
Online ISBN: 978-94-011-3488-0
eBook Packages: Springer Book Archive