{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T13:13:12Z","timestamp":1791033192542,"version":"4.1.0"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2007,7,27]],"date-time":"2007-07-27T00:00:00Z","timestamp":1185494400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2007,8,22]]},"DOI":"10.1007\/s10472-007-9078-x","type":"journal-article","created":{"date-parts":[[2007,7,26]],"date-time":"2007-07-26T09:43:27Z","timestamp":1185443007000},"page":"231-254","source":"Crossref","is-referenced-by-count":28,"title":["Decision procedures for extensions of the theory of arrays"],"prefix":"10.1007","volume":"50","author":[{"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Enrica","family":"Nicolini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniele","family":"Zucchelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2007,7,27]]},"reference":[{"key":"9078_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In: Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS\u201905). LNCS, vol. 3717, pp. 65\u201380. Springer (2005)","DOI":"10.1007\/11559306_4"},{"issue":"2","key":"9078_CR2","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140\u2013164 (2003)","journal-title":"Inf. Comput."},{"key":"9078_CR3","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Stickel, M.E., Uribe, T.E.: A practical integration of first-order reasoning and decision procedures. In: Proceedings of the 14th International Conference on Automated Deduction (CADE\u201997). LNCS, vol. 1249, pp. 101\u2013115. Springer (1997)","DOI":"10.1007\/3-540-63104-6_13"},{"key":"9078_CR4","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR\u201906). LNCS, vol. 4130, pp. 513\u2013527. Springer (2006)","DOI":"10.1007\/11814771_42"},{"issue":"10","key":"9078_CR5","doi-asserted-by":"crossref","first-page":"1493","DOI":"10.1016\/j.ic.2005.05.011","volume":"204","author":"M. Bozzano","year":"2006","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient theory combination via boolean search. Inf. Comput. 204(10), 1493\u20131525 (2006)","journal-title":"Inf. Comput."},{"key":"9078_CR6","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201906). LNCS, vol. 3855, pp. 427\u2013442. Springer (2006)","DOI":"10.1007\/11609773_28"},{"key":"9078_CR7","doi-asserted-by":"crossref","unstructured":"Brodnik, A., Carlsson, S., Demaine, E.D., Munro, J.I., Sedgewick, R.: Resizable arrays in optimal time and space. In: Proceedings of 6th International Workshop on Algorithms and Data Structures (WADS\u201999). LNCS, vol. 1663, pp. 37\u201348. Springer (1999)","DOI":"10.1007\/3-540-48447-7_4"},{"key":"9078_CR8","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe, D., Ranise, S.: Light-weight theorem proving for debugging and verifying units of code. In: Proceedings of the 1st International Conference on Software Engineering and Formal Methods (SEFM\u201903), pp. 220\u2013228. IEEE Computer Society (2003)","DOI":"10.1109\/SEFM.2003.1236224"},{"issue":"4","key":"9078_CR9","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1145\/322092.322104","volume":"25","author":"P.J. Downey","year":"1978","unstructured":"Downey, P.J., Sethi, R.: Assignment commands with array references. J. ACM 25(4), 652\u2013666 (1978)","journal-title":"J. ACM"},{"key":"9078_CR10","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"1972","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic, New York (1972)"},{"key":"9078_CR11","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row (1986)"},{"key":"9078_CR12","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Korovin, K.: Integrating equational reasoning in instantiation-based theorem proving. In: Proceedings of the 18th International Workshop on Computer Science in Logic (CSL\u201904). LNCS, vol. 3210, pp. 71\u201384. Springer (2004)","DOI":"10.1007\/978-3-540-30124-0_9"},{"issue":"3\u20134","key":"9078_CR13","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/s10817-004-6241-5","volume":"33","author":"S. Ghilardi","year":"2004","unstructured":"Ghilardi, S.: Model-theoretic methods in combined constraint satisfiability. J. Autom. Reason. 33(3\u20134), 221\u2013249 (2004)","journal-title":"J. Autom. Reason."},{"key":"9078_CR14","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Deciding extension of the theory of arrays by integrating decision procedures and instantiation strategies. Rapporto Interno DSI 309-06, Universit\u00e0 degli Studi di Milano, Milano (Italy) (2006) Available at http:\/\/homes.dsi.unimi.it\/~zucchell\/publications\/techreport\/GhiNiRaZu-RI309-06.pdf"},{"issue":"2","key":"9078_CR15","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0020-0190(81)90007-7","volume":"12","author":"J. Jaffar","year":"1981","unstructured":"Jaffar, J.: Presburger arithmetic with array segments. Inf. Process. Lett. 12(2), 79\u201382 (1981)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"9078_CR16","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1145\/322248.322250","volume":"28","author":"P. Mateti","year":"1981","unstructured":"Mateti, P.: A decision procedure for the correctness of a class of programs. J. ACM 28(2), 215\u2013232 (1981)","journal-title":"J. ACM"},{"key":"9078_CR17","unstructured":"McCarthy, J.: Towards a mathematical theory of computation. In: Proceedings of IFIP Congress, pp. 21\u201328 (1962)"},{"key":"9078_CR18","doi-asserted-by":"crossref","unstructured":"McPeak, S., Necula, G.: Data structures specification via local equality axioms. In: Proceedings of the 17th International Conference on Computer Aided Verification (CAV\u201905). LNCS, vol. 3576, pp. 476\u2013490. Springer (2005)","DOI":"10.1007\/11513988_47"},{"issue":"2","key":"9078_CR19","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9078_CR20","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, chapter\u00a07, pp. 371\u2013443. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"issue":"5","key":"9078_CR21","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1145\/359104.359110","volume":"22","author":"J.C. Reynolds","year":"1979","unstructured":"Reynolds, J.C.: Reasoning about arrays. Commun. ACM 22(5), 290\u2013299 (1979)","journal-title":"Commun. ACM"},{"key":"9078_CR22","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS\u201902), pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"9078_CR23","unstructured":"Rusinowitch, M.: D\u00e9monstration Automatique (Techniques de r\u00e9\u00e9criture). InterEditions (1989)"},{"key":"9078_CR24","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley (1986)"},{"key":"9078_CR25","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science (LICS\u201901). pp. 29\u201337. IEEE Computer Society (2001)","DOI":"10.1109\/LICS.2001.932480"},{"issue":"1","key":"9078_CR26","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/322169.322185","volume":"27","author":"N. Suzuki","year":"1980","unstructured":"Suzuki, N., Jefferson, D.R.: Verification decidability of Presburger array programs. J. ACM 27(1), 191\u2013205 (1980)","journal-title":"J. ACM"},{"key":"9078_CR27","unstructured":"van Dalen, D.: Logic and Structure, 2nd edn. Springer (1989)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-007-9078-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-007-9078-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-007-9078-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T22:34:21Z","timestamp":1737326061000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-007-9078-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7,27]]},"references-count":27,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2007,8,22]]}},"alternative-id":["9078"],"URL":"https:\/\/doi.org\/10.1007\/s10472-007-9078-x","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,7,27]]}}}