Abstract
This paper is concerned with the integration of recursive data structures with Presburger arithmetic. The integrated theory includes a length function on data structures, thus providing a tight coupling between the two theories, and hence the general Nelson-Oppen combination method for decision procedures is not applicable to this theory, even for the quantifier-free case. We present four decision procedures for the integrated theory depending on whether the language has infinitely many constants and whether the theory has quantifiers. Our decision procedures for quantifier-free theories are based on Oppen’s algorithm for acyclic recursive data structures with infinite atom domain.
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
Bjørner, N.S.: Integrating Decision Procedures for Temporal Verification. PhD thesis, Computer Science Department, Stanford University (November 1998)
Bjørner, N.S., Browne, A., Colón, M., Finkbeiner, B., Manna, Z., Sipma, H.B., Uribe, T.E.: Verifying temporal properties of reactive systems: A STeP tutorial. Formal Methods in System Design 16(3), 227–270 (2000)
Compton, K.J., Henson, C.W.: A uniform method for proving lower bounds on the computational complexity of logical theories. Annals of Pure and Applied Logic 48, 1–79 (1990)
Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Machine Intelligence, vol. 7, pp. 91–99. American Elsevier, Amsterdam (1972)
Downey, J., Sethi, R., Tarjan, R.E.: Variations of the common subexpression problem. Journal of ACM 27, 758–771 (1980)
Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, London (2001)
Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories. Springer, Heidelberg (1979)
Hodges, W.: Model Theory. Cambridge University Press, Cambridge (1993)
Korovin, K., Voronkov, A.: A decision procedure for the existential theory of term algebras with the knuth-bendix ordering. In: Proceedings of 15th IEEE Symposium on Logic in Computer Science (LICS), pp. 291–302 (2000)
Korovin, K., Voronkov, A.: Knuth-Bendix constraint solving is NP-complete. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 979–992. Springer, Heidelberg (2001)
Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite tree. In: Proceedings of the 3rd IEEE Symposium on Logic in Computer Science (LICS), pp. 348–357. IEEE Press, Los Alamitos (1988)
Makanin, G.S.: The problem of solvability of equations in a free semigroup. Math. Sbornik 103, 147–236 (1977); English translation in Math. USSR Sb. 32, 129–198
Mal’cev, A.I.: Axiomatizable classes of locally free algebras of various types. In: The Metamathematics of Algebraic Systems, Collected Papers, ch. 23. pp. 262–281. North-Holland, Amsterdam (1971)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS) 1(2), 245–257 (1979)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of ACM 27(2), 356–364 (1980)
Oppen, D.C.: Elementary bounds for presburger arithmetic. In: Proceedings of 5th Annual ACM Symposium on Theory of Computing (STOC), pp. 34–37. ACM Press, New York (1973)
Oppen, D.C.: Reasoning about recursively defined data structures. Journal of ACM 27(3) (July 1980)
Reddy, C.R., Loveland, D.W.: Presburger arithmetic with bounded quantifier alternation. In: Proceedings of the 10th Annual Symposium on Theory of Computing (STOC), pp. 320–325. ACM Press, New York (1978)
Rybina, T., Voronkov, A.: A decision procedure for term algebras with queues. ACM Transactions on Computational Logic 2(2), 155–181 (2001)
Venkataraman, K.N.: Decidability of the purely existential fragment of the theory of term algebras. Journal of ACM 34(2), 492–510 (1987)
Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 363–376. Springer, Heidelberg (2002)
Zarba, C.G.: Combining sets with integers. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, pp. 103–116. Springer, Heidelberg (2002)
Zhang, T., Sipma, H.B., Manna, Z.: The decidability of the first-order theory of term algebras with Knuth-Bendix order. Submitted to CP 2004 (2004); Extended version available at theory.stanford.edu/~tingz/papers/cp04_extended.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, T., Sipma, H.B., Manna, Z. (2004). Decision Procedures for Recursive Data Structures with Integer Constraints. In: Basin, D., Rusinowitch, M. (eds) Automated Reasoning. IJCAR 2004. Lecture Notes in Computer Science(), vol 3097. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25984-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-25984-8_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22345-0
Online ISBN: 978-3-540-25984-8
eBook Packages: Springer Book Archive