Abstract
A method is given for deciding formulas in combinations of unquatified first-order theories. Rather than coupling separate decision procedures for the contributing theories, it makes use of a single, uniform procedure that minimizes the code needed to accommodate each additional theory. The method is applicable to theories whose semantics can be encoded within a certain class of purely equational canonical form theories that is closed under combination. Examples are given from the equational theories of integer and real arithmetic, a subtheory of monadic set theory, the theory of cons, car, and cdr, and others. A discussion of the speed performance of the procedure and a proof of the theorem that underlies its completeness are also given. The procedure has been used extensively as the deductive core of a system for program specification and verification.
This research was supported in part by NSF grant MCS-7904081, and by AFOSR contract F49620-79-C-0099.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Downey, P.J., R. Sethi, R. Tarjan. “Variations on the common subexpression problem.” To appear in J.ACM.
Jefferson, D. R., “Type reduction and program verification”, Ph.D. Thesis, Carnegie Mellon University, August 1978
Melliar-Smith, P. M., R. L. Schwartz, “Formal specification and mechanical verification of SIFT: a fault-tolerant flight control system”, IEEE Trans. on Computer, July 1982.
Nelson, G., D. Oppen, “Simplification by cooperating decision procedures”, ACM Transactions on Programming Languages and Systems, Vol. 1, No. 2, October 1979
Nelson, G., D. Oppen, “Fast decision procedures based on congruence closure”, J.ACM, Vol. 27, No. 2, April 1980, pp. 356–354
Shostak, R. E., “An algorithm for reasoning about equality”, C.ACM, Vol. 21, No. 7, July 1978, pp. 583–585
Shostak, R. E., “A practical decision procedure for arithmetic with function symbols”, J.ACM Vol. 26, No. 2, April 1979, pp. 351–360
Shostak, R. E., Richard Schwartz, P.M. Melliar-Smith, “STP: A Mechanized Logic for Specification and Verification”, Proceedings of the Sixth Conference on Automated Deduction, Springer-Verlag, June 1982
Tarjan, R.E., “Efficiency of a good but not linear set union algorithm”, J.ACM, Vol. 22, No. 2, April 1975, pp. 215–225.
Wensley, J., et al., “SIFT: Design and Analysis of a Fault-tolerant Computer for Aircraft Control”, Proc. IEEE, Vol. 66, No. 10, Oct. 1978
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shostak, R.E. (1982). Deciding combinations of theories. In: Loveland, D.W. (eds) 6th Conference on Automated Deduction. CADE 1982. Lecture Notes in Computer Science, vol 138. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000061
Download citation
DOI: https://doi.org/10.1007/BFb0000061
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11558-8
Online ISBN: 978-3-540-39240-8
eBook Packages: Springer Book Archive