{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T10:52:53Z","timestamp":1769856773550,"version":"3.49.0"},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,10,13]],"date-time":"2006-10-13T00:00:00Z","timestamp":1160697600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2006,12,13]]},"DOI":"10.1007\/s10817-006-9042-1","type":"journal-article","created":{"date-parts":[[2006,10,12]],"date-time":"2006-10-12T09:52:35Z","timestamp":1160646755000},"page":"213-239","source":"Crossref","is-referenced-by-count":49,"title":["Deciding Boolean Algebra with Presburger Arithmetic"],"prefix":"10.1007","volume":"36","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[]},{"given":"Huu Hai","family":"Nguyen","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,10,13]]},"reference":[{"key":"9042_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. North Holland, Amsterdam (1954)"},{"key":"9042_CR2","doi-asserted-by":"crossref","unstructured":"Arkoudas, K., Zee, K., Kuncak, V., Rinard, M.: Verifying a file system implementation. In: Sixth International Conference on Formal Engineering Methods (ICFEM \u201904), vol. 3308 of LNCS. Seattle (2004)","DOI":"10.1007\/978-3-540-30482-1_32"},{"key":"9042_CR3","volume-title":"The Description Logic Handbook: Theory, Implementation and Applications","year":"2003","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.) The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Boston, Massachusetts (2003)"},{"key":"9042_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) Proceedings of the 16th International Conference on Computer Aided Verification (CAV \u201904). Lecture Notes in Computer Science, vol. 3114, pp. 515\u2013518. Boston, Massachusetts (2004)","DOI":"10.1007\/978-3-540-27813-9_49"},{"issue":"1","key":"9042_CR5","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0304-3975(80)90037-7","volume":"11","author":"L. Berman","year":"1980","unstructured":"Berman, L.: The complexity of logical theories. Theor. Comp. Sci. 11(1), 71\u201377 (1980)","journal-title":"Theor. Comp. Sci."},{"issue":"3","key":"9042_CR6","doi-asserted-by":"crossref","first-page":"614","DOI":"10.1145\/1071596.1071601","volume":"6","author":"B. Boigelot","year":"2005","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Logic 6(3), 614\u2013633 (2005)","journal-title":"ACM Trans. Comput. Logic"},{"key":"9042_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Springer, Berlin Heidelberg New York (1997)"},{"key":"9042_CR8","volume-title":"FOSSACS\u201905. Lecture Notes in Computer Science","author":"M. Bozga","year":"2005","unstructured":"Bozga, M., Iosif, R.: On decidability within the arithmetic of addition and divisibility. In: FOSSACS\u201905. Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York (2005)"},{"key":"9042_CR9","doi-asserted-by":"crossref","first-page":"191","DOI":"10.36045\/bbms\/1103408547","volume":"1","author":"V. Bruy\u00e9re","year":"1994","unstructured":"Bruy\u00e9re, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin 1, 191\u2013238 (1994)","journal-title":"Bull. Belg. Math. Soc. Simon Stevin"},{"issue":"4","key":"9042_CR10","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. ACM Trans. Program. Lang. Syst. 21(4), 747\u2013789 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"9042_CR11","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1023\/A:1015019416843","volume":"28","author":"M. Cadoli","year":"2002","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate quantified boolean formulae and its experimental evaluation. J. Autom. Reason. 28(2), 101\u2013142 (2002)","journal-title":"J. Autom. Reason."},{"key":"9042_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3452-2","volume-title":"Set Theory for Computing","author":"D. Cantone","year":"2001","unstructured":"Cantone, D., Omodeo, E., Policriti, A.: Set Theory for Computing. Springer, Berlin Heidelberg New York (2001)"},{"key":"9042_CR13","unstructured":"Chaieb, A., Nipkow, T.: Generic proof synthesis for Presburger arithmetic. Technical report, Technische Universit\u00e4t M\u00fcnchen (2003)"},{"issue":"1","key":"9042_CR14","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. Assoc. Comput. Mach. 28(1), 114\u2013133 (1981)","journal-title":"J. Assoc. Comput. Mach."},{"key":"9042_CR15","doi-asserted-by":"crossref","unstructured":"Chin, W.-N., Khoo, S.-C., Xu, D.N.: Extending sized types with collection analysis. In: ACM PEPM\u201903, San Diego, California (2003)","DOI":"10.1145\/777388.777397"},{"key":"9042_CR16","first-page":"91","volume-title":"Machine Intelligence, vol. 7","author":"D.C. Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 91\u2013100. Edinburgh University Press, London, UK (1972)"},{"issue":"1","key":"9042_CR17","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1145\/357062.357064","volume":"1","author":"R.K. Dewar","year":"1979","unstructured":"Dewar, R.K.: Programming by refinement, as exemplified by the SETL representation sublanguage. ACM Trans. Program. Lang. Syst. 1(1), 27\u201349 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9042_CR18","doi-asserted-by":"crossref","first-page":"57","DOI":"10.4064\/fm-47-1-57-103","volume":"47","author":"S. Feferman","year":"1959","unstructured":"Feferman, S., Vaught, R.L.: The first order properties of products of algebraic systems. Fundam. Math. 47, 57\u2013103 (1959)","journal-title":"Fundam. Math."},{"key":"9042_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0062837","volume-title":"The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718","author":"J. Ferrante","year":"1979","unstructured":"Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718 Springer, Berlin Heidelberg New York (1979)"},{"key":"9042_CR20","volume-title":"Introduction to HOL, a Theorem Proving Environment for Higher-order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL, a Theorem Proving Environment for Higher-order Logic. Cambridge University Press, UK (1993)"},{"key":"9042_CR21","volume-title":"TACAS \u201995. Lecture Notes in Computer Science, vol. 1019","author":"J. Henriksen","year":"1995","unstructured":"Henriksen, J., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: TACAS \u201995. Lecture Notes in Computer Science, vol. 1019. Springer, Berlin Heidelberg New York (1995)"},{"issue":"10","key":"9042_CR22","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"9042_CR23","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: IMACS International Conference on Applications of Computer Algebra, Beaumont, Texas (2004)"},{"key":"9042_CR24","volume-title":"Proc. 5th International Conference on Implementation and Application of Automata. Lecture Notes in Computer Science","author":"N. Klarlund","year":"2000","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Proc. 5th International Conference on Implementation and Application of Automata. Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York (2000)"},{"key":"9042_CR25","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/0304-3975(80)90048-1","volume":"10","author":"D. Kozen","year":"1980","unstructured":"Kozen, D.: Complexity of boolean algebras. Theor. Comput. Sci. 10, 221\u2013247 (1980)","journal-title":"Theor. Comput. Sci."},{"key":"9042_CR26","volume-title":"Theory of Computation","author":"D. Kozen","year":"2006","unstructured":"Kozen, D.: Theory of Computation. Springer, Berlin Heidelberg New York (2006)"},{"key":"9042_CR27","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean algebra with Presburger arithmetic. In: 20th International Conference on Automated Deduction, CADE-20, Tallinn, Estonia (2005)","DOI":"10.1007\/11532231_20"},{"key":"9042_CR28","unstructured":"Kuncak, V., Rinard, M.: On the theory of structural subtyping. Technical Report 879. Laboratory for Computer Science, Massachusetts Institute of Technology (2003a)"},{"key":"9042_CR29","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: Structural subtyping of non-recursive types is decidable. In: Eighteenth Annual IEEE Symposium on Logic in Computer Science, Ottawa, Canada (2003b)","DOI":"10.1109\/LICS.2003.1210049"},{"key":"9042_CR30","unstructured":"Kuncak, V., Rinard, M.: The first-order theory of sets with cardinality constraints is decidable. Technical Report 958, MIT CSAIL (2004)"},{"key":"9042_CR31","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: Decision procedures for set-valued fields. In: 1st International Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL), Paris, France (2005)","DOI":"10.1016\/j.entcs.2005.01.022"},{"key":"9042_CR32","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: An overview of the Jahob analysis system: Project goals and current status. In: NSF Next Generation Software Workshop, Rhodes, Greece (2006)","DOI":"10.1109\/IPDPS.2006.1639580"},{"key":"9042_CR33","volume-title":"CAV\u201904. Lecture Notes in Computer Science, vol. 3114","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Seshia, S.A.: The UCLID decision procedure. In: CAV\u201904. Lecture Notes in Computer Science, vol. 3114. Springer, Berlin Heidelberg New York (2004)"},{"key":"9042_CR34","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1145\/981009.981016","volume":"39","author":"P. Lam","year":"2004","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking using set interfaces and pluggable analyses. SIGPLAN Not. 39, 46\u201355 (2004)","journal-title":"SIGPLAN Not."},{"key":"9042_CR35","doi-asserted-by":"crossref","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking for data structure consistency. In: 6th International Conference on Verification, Model Checking and Abstract Interpretation, Paris (2005)","DOI":"10.1007\/978-3-540-30579-8_28"},{"key":"9042_CR36","first-page":"228","volume":"76","author":"L. Loewenheim","year":"1915","unstructured":"Loewenheim, L.: \u00dcber M\u00f6gligkeiten im Relativkalk\u00fcl. Math. Ann. 76, 228\u2013251 (1915)","journal-title":"Math. Ann."},{"key":"9042_CR37","unstructured":"Marnette, B., Kuncak, V., Rinard, M.: On algorithms and complexity for sets with cardinality constraints. Technical report, MIT CSAIL (2005)"},{"key":"9042_CR38","unstructured":"Marriott, K., Odersky, M.: Negative boolean constraints. Technical Report 94\/203, Monash University (1994)"},{"key":"9042_CR39","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Conference on Programming Language Design and Implementation, Snowbird, Utah (2001)","DOI":"10.1145\/378795.378851"},{"issue":"2","key":"9042_CR40","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":"9042_CR41","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283 of LNCS","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283 of LNCS. Springer, Berlin Heidelberg New York (2002)"},{"key":"9042_CR42","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/978-94-017-0437-3_3","volume-title":"Automated Deduction. A Basis for Applications, vol. 3","author":"H.J. Ohlbach","year":"1998","unstructured":"Ohlbach, H.J., Koehler, J.: How to extend a formal system with a Boolean algebra component. In: Schmidt, W.B.P.H. (ed.) Automated Deduction. A Basis for Applications, vol. 3, pp. 57\u201375. Kluwer, Boston, Massachusetts (1998)"},{"key":"9042_CR43","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) 11th CADE, vol. 607 of LNAI, pp. 748\u2013752 (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"issue":"4","key":"9042_CR44","doi-asserted-by":"crossref","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"C.H. Papadimitriou","year":"1981","unstructured":"Papadimitriou, C.H.: On the complexity of integer programming. J. Assoc. Comput. Mach. 28(4), 765\u2013768 (1981)","journal-title":"J. Assoc. Comput. Mach."},{"key":"9042_CR45","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1145\/1040305.1040317","volume-title":"ACM POPL","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: ACM POPL, pp. 132\u2013144. ACM, New York (2005)"},{"key":"9042_CR46","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Aritmethik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du premier Congr\u00e8s des Math\u00e9maticiens des Pays slaves, Warsawa, pp. 92\u2013101 (1929)"},{"key":"9042_CR47","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. In: Supercomputing \u201991: Proceedings of the 1991 ACM\/IEEE Conference on Supercomputing, Albuquerque, New Mexico, pp. 4\u201313 (1991)","DOI":"10.1145\/125826.125848"},{"key":"9042_CR48","first-page":"320","volume-title":"ACM STOC","author":"C.R. Reddy","year":"1978","unstructured":"Reddy, C.R., Loveland, D.W.: Presburger arithmetic with bounded quantifier alternation. In: ACM STOC, pp. 320\u2013325. ACM, New York (1978)"},{"key":"9042_CR49","volume-title":"Proc. Advances in Databases and Information Systems (ADBIS\u201904). Lecture Notes in Computer Science, vol. 3255","author":"P. Revesz","year":"2004","unstructured":"Revesz, P.: Quantifier-elimination for the first-order theory of boolean algebras with linear cardinality constraints. In: Proc. Advances in Databases and Information Systems (ADBIS\u201904). Lecture Notes in Computer Science, vol. 3255. Springer, Berlin Heidelberg New York (2004)"},{"key":"9042_CR50","doi-asserted-by":"crossref","unstructured":"Ruess, H., Shankar, N.: Deconstructing Shostak. In: Proc. 16th IEEE LICS, Washington\u2013Brussels\u2013New York (2001)","DOI":"10.1109\/LICS.2001.932479"},{"key":"9042_CR51","doi-asserted-by":"crossref","unstructured":"Rugina, R.: Quantitative shape analysis. In: Static Analysis Symposium (SAS\u201904), Verona, Italy (2004)","DOI":"10.1007\/978-3-540-27864-1_18"},{"issue":"3","key":"9042_CR52","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217\u2013298 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9042_CR53","unstructured":"Skolem, T.: Untersuchungen \u00fcber die Axiome des Klassenkalk\u00fcls and \u00fcber \u201cProduktations-und Summationsprobleme\u201d, welche gewisse Klassen von Aussagen betreffen. Skrifter utgit av Vidnskapsselskapet i Kristiania, I, klasse, no. 3, Oslo (1919)"},{"issue":"1","key":"9042_CR54","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"J.W. Thatcher","year":"1968","unstructured":"Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Syst. Theory 2(1), 57\u201381 (1968)","journal-title":"Math. Syst. Theory"},{"key":"9042_CR55","volume-title":"Handbook of Formal Languages Vol. 3: Beyond Words","author":"W. Thomas","year":"1997","unstructured":"Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages Vol. 3: Beyond Words. Springer, Berlin Heidelberg New York (1997)"},{"issue":"3","key":"9042_CR56","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C. Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.: Combining non-stably infinite theories. J. Autom. Reason. 34(3), 209\u2013238 (2005)","journal-title":"J. Autom. Reason."},{"key":"9042_CR57","unstructured":"Tiwari, A.: Decision procedures in automated deduction. Ph.D. thesis, Department of Computer Science, State University of New York at Stony Brook (2000)"},{"issue":"2","key":"9042_CR58","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/BF00881918","volume":"15","author":"A. Voronkov","year":"1995","unstructured":"Voronkov, A.: The anatomy of Vampire (implementing bottom-up procedures with code trees). J. Autom. Reason. 15(2), 237\u2013265 (1995)","journal-title":"J. Autom. Reason."},{"key":"9042_CR59","doi-asserted-by":"crossref","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning, vol. 2, Chapt. 27","author":"C. Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, Chapt. 27, pp. 1965\u20132013. Elsevier Science, Amsterdam (2001)"},{"key":"9042_CR60","volume-title":"Proceedings of 10th TACAS","author":"G. Yorsh","year":"2004","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Proceedings of 10th TACAS. Springer, Berlin Heidelberg New York (2004)"},{"key":"9042_CR61","unstructured":"Zarba, C.G.: The combination problem in automated reasoning. Ph.D. thesis, Stanford University (2004a)"},{"key":"9042_CR62","first-page":"762","volume-title":"Verification: Theory and Practice. Lecture Notes in Computer Science, vol. 2772","author":"C.G. Zarba","year":"2004","unstructured":"Zarba, C.G.: Combining sets with elements. In: Dershowitz, N. (ed.) Verification: Theory and Practice. Lecture Notes in Computer Science, vol 2772, pp. 762\u2013782. Springer, Berlin Heidelberg New York (2004b)"},{"key":"9042_CR63","unstructured":"Zarba, C.G.: A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator. In: 18th International Workshop on Unification (2004c)"},{"issue":"1","key":"9042_CR64","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-005-3075-8","volume":"34","author":"C.G. Zarba","year":"2005","unstructured":"Zarba, C.G.: Combining sets with cardinals. J. Autom. Reason. 34(1), 1\u201329 (2005)","journal-title":"J. Autom. Reason."},{"key":"9042_CR65","first-page":"442","volume-title":"ICCAD \u201902: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: ICCAD \u201902: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design, pp. 442\u2013449. New York, USA (2002)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9042-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9042-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9042-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,9]],"date-time":"2023-05-09T09:28:57Z","timestamp":1683624537000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9042-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10,13]]},"references-count":65,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,12,13]]}},"alternative-id":["9042"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9042-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10,13]]}}}