Abstract
The str∔ve theorem prover is designed to prove theorems about dense linear orders. In this paper, we discuss two extensions of str∔ve to theorems about the integers. We describe a version of str∔ve which proves theorems solely about integers. Also, we describe a version for theorems over two separate linear orders, one dense and one the integers.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Bledsoe, W. W., “The Sup-Inf Method in Presburger Arithmetic”. The University of Texas at Austin, Math Department Memo ATP-18. December 1974. Essentially the same as: A new method for proving certain Presburger formulas. Fourth IJCAI, Tbilisi, USSR, September 3–8, 1975.
Bledsoe, W. W., and L. M. Hines, “Variable Elimination and Chaining in a Resolution-Base Prover for Inequalities”, Proc. 5th Conference on Automated Deduction, Les Arcs, France, Springer-Verlag, (July 1980) 70–87.
Boyer, R. S. and J S. Moore, “Integrating Decision Procedures into Heuristics Theorem Provers: A Case Study of Linear Arithmetic”, Technical Report ICSCA-CMP-44, University of Texas, Austin, TX, January 1985.
Brooks, R. A., Model-Based Computer Vision, UMI Research Press, Ann Arbor, MI.
Davis, M. and H. Putman, “A Computing Procedure for Quantification Theory”, J. Association of Computing Machinery 7, (1960) 201–215.
Käufl, T., “Reasoning about Systems of Linear Inequalities”, Proc. 9th International Conference on Automated Deduction, Argonne, Illinois, Springer-Verlag, (May 1988) 469–486.
Hines, L. and W. W. Bledsoe, “The Str∔ve Prover”, Technical Report ATP-94, University of Texas at Austin, 1990.
Hines, L., “Building In Axioms and Lemmas”, Ph.D. Dissertation, University of Texas at Austin, (May 1988).
Hines, L., “Hyper-Chaining and Knowledge-Based Theorem Proving”, Proc. 9th International Conference on Automated Deduction, Argonne, Illinois, Springer-Verlag, (May 1988) 469–486.
Hines, L., “Completeness of a Prover for Dense Linear Orders”, Journal of Automated Reasoning, Vol. 8, 45–75, 1992, Netherlands, Kluwer Academic Pulishers.
Hines, L., “StR∔ve⊂@#@)-: The STR∔VE-based Subset Prover”, 10th International Conference on Automated Deduction, July 1990, Kaiserslautern, Germany, Springer-Verlag, 193–206.
Hines, L., “The Central Variable Strategy of Str∔ve”, 11th International Conference on Automated Deduction, June 1992, Saratoga Springs, NY, Springer-Verlag, 35–49.
King, J. C., A Program Verifier, Phd Dissertation, Carnegie-Mellon University, 1969.
Nelson, G., and D. Oppen, “A Simplifier Based on Efficient Decision Algorithms”, Proc. Fifth ACM Symp. on Principles of Programming Languages, 1978.
Rabinov, A., “A Restriction of Factoring in Binary Resolution”. Proc. 9th International Conference of Automated Deduction, Argonne, Illinois, USA, Springer-Verlag, (May 1988) 582–591.
Shostak, R., “A Practical Decision Procedure for Arithmetic with Function Symbols”, JACM, April 1979.
Slagle, J. R., and L. Norton, “Experiments with an Automatic Theorem Prover Having Partial Ordering Rules”, CACM 16, 1973, pp 683–688.
Stickel, M. E., “Automated Deduction by Theory Resolution, IJCAI-85, Los Angeles, California 1985, pp 1181–1186.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hines, L.M. (1994). Str∔ve and integers. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_29
Download citation
DOI: https://doi.org/10.1007/3-540-58156-1_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58156-7
Online ISBN: 978-3-540-48467-7
eBook Packages: Springer Book Archive