Abstract
The role of decision procedures is often essential in theorem proving. Decision procedures can reduce the search space of heuristic components of a prover and increase its abilities. However, in some applications only a small number of conjectures fall within the scope of the available decision procedures. Some of these conjectures could in an informal sense fall ‘just outside’ that scope. In these situations a problem arises because lemmas have to be invoked or the decision procedure has to communicate with the heuristic component of a theorem prover. This problem is also related to the general problem of how to flexibly integrate decision procedures into heuristic theorem provers. In this paper we address such problems and describe a framework for the flexible integration of decision procedures into other proof methods. The proposed framework can be used in different theorem provers, for different theories and for different decision procedures. New decision procedures can be simply ‘plugged-in’ to the system. As an illustration, we describe an instantiation of this framework within the Clam proof-planning system, to which it is well suited. We report on some results using this implementation.
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
L. Bachmair and H. Ganzinger. Strict basic superposition. In Kirchner and Kirchner [12], pages 160–174.
L. Bachmair, H. Ganzinger, and A. Voronkov. Elimination of equality via transformation with ordering constraints. In Kirchner and Kirchner [12], pages 175–190.
R. S. Boyer and J S. Moore. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In J. E. Hayes, J. Richards, and D. Michie, editors, Machine Intelligence 11, pages 83–124, 1988.
A. Bundy. The use of proof plans for normalization. In R. S. Boyer, editor, Essays in Honor of Woody Bledsoe, pages 149–166. Kluwer, 1991.
A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647–648. Springer-Verlag, 1990..
D. C. Cooper. Theorem proving in arithmetic without multiplication. In B. Meltzer and D. Michie, editors, Machine Intelligence 7, pages 91–99. Edinburgh University Press, 1972.
D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak’s decision procedure for combinations of theories. In M. McRobbie and J. Slaney,editors, 13th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 1104, New Brunswick, NJ, USA, 1996. Springer-Verlag.
User guide for the Ehdm specification language and verification system, version 6.1. Technical report, SRI Computer Science Laboratory, 1993.
L. Hodes. Solving problems by formula manipulation in logic and linear inequalities. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence, pages 553–559, Imperial College, London, England, 1971. The British Computer Society.
P. Janičić, I. Green, and A. Bundy. A comparison of decision procedures in Presburger arithmetic. In R. Tošić and Z. Budimac, editors, Proceedings of the VIII Conference on Logic and Computer Science (LIRA’ 97), pages 91–101, Novi Sad, Yugoslavia, September 1-4 1997. University of Novi Sad.
D. Kapur and X. Nie. Reasoning about numbers in Tecton. In Proceedings of 8th International Symposium on Methodologies for Intelligent Systems, Charlotte, North Carolina, USA, October 1994.
C. Kirchner and H. Kirchner, editors. 15th International Conference on Automated Deduction, Lindau, Germany, July 1998.
G. Kreisel and J. L. Krivine. Elements of mathematical logic: Model theory. North Holland, Amsterdam, 1967.
D. C. Luckham, S. M. German, F. W. von Henke, R. A. Karp, P. W. Milne, D. C. Oppen, W. Polak, and W. L. Scherlis. Stanford Pascal verifier user manual. CSD Report STAN-CS-79-731, Stanford University, 1979.
Z. Manna et al. STeP: The Stanford Temporal Prover. Technical Report STANCSTR;94-1518, Stanford University, 1994.
G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, October 1979.
S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. K. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T. A. Henzinger, editors, Proceedings of the 1996 Conference on Computer-Aided Verification, number 1102in LNCS, pages 411–414, New Brunswick, New Jersey, U. S. A., 1996. Springer-Verlag.
M. Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Sprawozdanie z I Kongresu metematyków slowiańskich, Warszawa 1929, pages 92–101, 395. Warsaw, 1930. Annotated English version also available [20].
R. E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1–12, January 1984.
R. Stansifer. Presburger’;s article on integer arithmetic: Remarks and translation. Technical Report TR 84-639, Department of Computer Science, Cornell University, September 1984.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Janičić, P., Bundy, A., Green, I. (1999). A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_9
Download citation
DOI: https://doi.org/10.1007/3-540-48660-7_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66222-8
Online ISBN: 978-3-540-48660-2
eBook Packages: Springer Book Archive