Abstract
This paper describes a class of decision procedures that we have found useful for efficient, domain-specific deductive synthesis, and a method for integrating this type of procedure into a general-purpose refutation-based theorem prover. We suggest that this is a large and interesting class of procedures and show how to integrate these procedures to accelerate a general-purpose theorem prover doing deductive synthesis. While much existing research on decision procedures has been either in isolation or in the context of interfacing procedures to non-refutation-based theorem provers, this appears to be the first reported work on decision procedures in the context of refutation based deductive synthesis where witnesses must be found.
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.
Reference
Baader, F. & Tinelli, C, “A New Approach for Combining Decision Procedures for the Word Problem, and its Connection to the Nelson-Oppen Combination Method,” CADE14, pp. 19–33, 1997.
R. Boyer and Moore, J, Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic, Institute for Computing Science and Computer Applications, University of Texas as Austin, 1988.
Burckert, H. J., “A Resolution Principle for a Logic With Restricted Quantifiers,” Lecture Notes in Artificial Intelligence, Vol. 568, Springer-Verlag, 1991.
Chang, C & Lee, R.C., Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973.
Cyrluk, D., Lincoln, P., Shankar, N. “On Shostak’s decision procedures for combinations of theories,” Automated Deduction—CADE-13 in Lecture Notes in AI 1104, (M. A. McRobbie and J. K. Slaney Eds), Springer, pp. 463–477, 1996.
Deville, Y. and Lau, K., “Logic Program Synthesis,” Journal of Logic Programming, 19,20: 321–350, 1994.
Dunham, B. and North, J., “Theorem Testing by Computer,” Proceedings of the Symposium on Mathematical Theory of Automata, Polytechnic Press, Brooklyn, N.Y., pp. 173–177, 1963.
Gallier, J.H., Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, 1986.
C.A.R. Hoare, “Proof of Correctness of Data Representations,” Acta Infomatica, Vol. 1, pp. 271–281, 1973.
M. Lowry and J. Van Baalen, “META-Amphion: Synthesis of Efficient Domain-Specific Program Synthesis Systems”, Automated Software Engineering, vol 4, pp. 199–241, 1997.
Nelson, G., and Oppen, D., “Simplification By Cooperating Decision Procedures,” ACM Transactions on Programming Languages and Systems, No. 1, pp. 245–257, 1979.
Nelson, G., and Oppen, D., “Fast decision procedures based on congruence closure,” Journal of the ACM, 27, 2, pp. 356–364, 1980.
Owre, S., Rushby, M., and Shankar, N., “PVS: A Prototype Verification System,” CADE-11, LNAI Vol. 607, pp. 748–752, 1992.
Roach, S., “TOPS: Theory Operationalization for Program Synthesis,” Ph.D. Thesis at University of Wyoming, 1997.
Shostak, R., “A practical decision procedure for arithmetic with function symbols,” Journal of the ACM, Vol. 26, pp. 351–360, 1979.
Shostak, R., “Deciding Combinations of Theories,” Journal of the ACM, Vol. 31, pp. 1–12, 1984.
M. Stickel, R. Waldinger, M. Lowry, T. Pressburger, and I. Underwood, “Deductive Composition of Astronomical Software from Subroutine Libraries,” CADE-12, 1994. See http://ic-www.arc.nasa.gov/ic/projects/amphion/docs/amphion.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Van Baalen, J., Roach, S. (1999). Using Decision Procedures to Accelerate Domain-Specific Deductive Synthesis Systems. In: Flener, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 1998. Lecture Notes in Computer Science, vol 1559. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48958-4_4
Download citation
DOI: https://doi.org/10.1007/3-540-48958-4_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65765-1
Online ISBN: 978-3-540-48958-0
eBook Packages: Springer Book Archive