{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:02:57Z","timestamp":1725663777873},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544876"},{"type":"electronic","value":"9783540384014"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54487-9_54","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:54:26Z","timestamp":1330192466000},"page":"95-109","source":"Crossref","is-referenced-by-count":5,"title":["Decision problems for tarski and presburger arithmetics extended with sets"],"prefix":"10.1007","author":[{"given":"D.","family":"Cantone","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V.","family":"Cutello","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. T.","family":"Schwartz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W.W. Bledsoe","year":"1977","unstructured":"W.W. Bledsoe. Non-resolution theorem proving. J. Art. Int., 9:1\u201335, 1977.","journal-title":"J. Art. Int."},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"W.W. Bledsoe. Some automatic proof in analysis. Contemporary AMS editor, Automated Theorem Proving after 25 years, 1984.","DOI":"10.1090\/conm\/029"},{"key":"6_CR3","unstructured":"D. Cantone, A. Ferro, and E.G. Omodeo. Computable Set Theory. Oxford University Press, 1990."},{"key":"6_CR4","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1002\/cpa.3160400303","volume":"XL","author":"D. Cantone","year":"1987","unstructured":"D. Cantone, A. Ferro, E. Omodeo, and J.T. Schwartz. Decision algorithms for some fragments of Analysis and related areas. Comm. Pure App. Math., XL:281\u2013300, 1987.","journal-title":"Comm. Pure App. Math."},{"key":"6_CR5","unstructured":"D. Cantone and E. Omodeo. On the decidability of formulae involving continuous and closed functions. In N.S. Sridharam, editor, Eleventh Int. Joint Conf. on Art. Intell., pages 425\u2013430, 1989."},{"issue":"8","key":"6_CR6","doi-asserted-by":"crossref","first-page":"1175","DOI":"10.1002\/cpa.3160420809","volume":"XLII","author":"D. Cantone","year":"1989","unstructured":"D. Cantone and E. Omodeo. Topological syllogistic with continuous and closed functions. Comm. Pure App. Math., XLII, n. 8:1175\u20131188, 1989.","journal-title":"Comm. Pure App. Math."},{"key":"6_CR7","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume":"33","author":"G.E. Collins","year":"1975","unstructured":"G.E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. Proc. 2nd GI Conf. Automata Theory and Formal Languages. Springer Lecture Notes in CS, 33:134\u2013183, 1975.","journal-title":"Springer Lecture Notes in CS"},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF00245817","volume":"6","author":"D. Cantone","year":"1990","unstructured":"D. Cantone, E. Omodeo, and A. Policriti. The automation of syllogistic. II. Optimisation and complexity issues. Journal of Automated Reasoning, 6:173\u2013187, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR9","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"J.H. Davenport","year":"1988","unstructured":"J.H. Davenport and J. Heintz. Real quantifier elimination is doubly exponential. J. Symb. Comp., 5:29\u201335, 1988.","journal-title":"J. Symb. Comp."},{"key":"6_CR10","unstructured":"J.H. Davenport, Y. Siret, and E. Tournier. Computer Algebra. Systems and algorithms for algebraic computation. Academic Press Limited, 1988."},{"key":"6_CR11","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1002\/cpa.3160400302","volume":"XL","author":"A. Ferro","year":"1987","unstructured":"A. Ferro and E. Omodeo. Decision procedures for elementary sublanguages of set theory. VII. validity in set theory when a choice operator is present. Comm. Pure App. Math., XL:265\u2013280, 1987.","journal-title":"Comm. Pure App. Math."},{"key":"6_CR12","doi-asserted-by":"crossref","first-page":"599","DOI":"10.1002\/cpa.3160330503","volume":"XXXIII","author":"A. Ferro","year":"1980","unstructured":"A. Ferro, E. Omodeo, and J.T. Schwartz. Decision procedures for elementary sublanguages of set theory. I. Multilevel syllogistic and some extensions. Comm. Pure App. Math., XXXIII:599\u2013608, 1980.","journal-title":"Comm. Pure App. Math."},{"key":"6_CR13","volume-title":"Integer programming","author":"R.S. Garfinkel","year":"1972","unstructured":"R.S. Garfinkel and G.L. Nemhauser. Integer programming. John Wiley & Sons, Inc., New York, 1972."},{"key":"6_CR14","first-page":"354","volume":"11","author":"Y. Matijasevi\u010d","year":"1970","unstructured":"Y. Matijasevi\u010d. Enumerable sets are Diophantine sets. Soviet Math. Doklady, 11:354\u2013357, 1970.","journal-title":"Soviet Math. Doklady"},{"key":"6_CR15","unstructured":"E.G. Omodeo. Decidability and proof procedures for set theory with a choice operator. PhD thesis, New York University, 1984."},{"issue":"4","key":"6_CR16","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"C.H. Papadimitriou","year":"1981","unstructured":"C.H. Papadimitriou. On the complexity of Integer Programming. Journal of ACM, 28, N. 4:765\u2013768, 1981.","journal-title":"Journal of ACM"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"F. Parlamento and A. Policriti. Decision procedures for elementary sublanguages of set theory. XIII. Model graphs, reflection and decidability. To appear in J. Automated Reasoning, 1990.","DOI":"10.1007\/BF00243810"},{"key":"6_CR18","unstructured":"M. Presburger. \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetic ganzer Zahlen, in welchem die Addition als einsige Operation hervortritt. In Comptes-rendus du Premier Congr\u00e8s des Mathematiciens des Pays Slaves, pages 192\u2013201,395. Warsaw, 1929."},{"key":"6_CR19","volume-title":"Integer programming","author":"H.M. Salkin","year":"1975","unstructured":"H.M. Salkin. Integer programming. Addison-Wesley Publishing Co., Inc., Reading, Mass., 1975."},{"key":"6_CR20","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A decision method for elementary algebra and geometry","author":"A. Tarski","year":"1951","unstructured":"A. Tarski. A decision method for elementary algebra and geometry. Univ. of California Press, Berkeley, 2nd ed. rev., 1951.","edition":"2nd ed. rev."},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"A. Tarski. What is elementary geometry? In L. Henkin, P. Suppes, and A. Tarski, editors, The axiomatic method with special reference to geometry and physics, pages 16\u201329, 1959.","DOI":"10.1016\/S0049-237X(09)70017-5"},{"key":"6_CR22","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V. Weispfenning","year":"1988","unstructured":"V. Weispfenning. The complexity of linear problems in fields. J. Symb. Comp., 5:3\u201328, 1988.","journal-title":"J. Symb. Comp."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54487-9_54.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,30]],"date-time":"2021-12-30T22:50:22Z","timestamp":1640904622000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54487-9_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544876","9783540384014"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-54487-9_54","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}