{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:38:12Z","timestamp":1725557892992},"publisher-location":"Berlin, Heidelberg","reference-count":134,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642143083"},{"type":"electronic","value":"9783642143090"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14309-0_3","type":"book-chapter","created":{"date-parts":[[2010,6,23]],"date-time":"2010-06-23T13:09:58Z","timestamp":1277298598000},"page":"37-63","source":"Crossref","is-referenced-by-count":11,"title":["Theory-Specific Automated Reasoning"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Formisano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eugenio G.","family":"Omodeo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"LNAI","first-page":"238","volume-title":"Automated Deduction - CADE-12","year":"1994","unstructured":"Bundy, A. (ed.): CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 238\u2013251. Springer, Heidelberg (1994); The QED Manifesto"},{"key":"3_CR2","doi-asserted-by":"publisher","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P.B. Andrews","year":"1971","unstructured":"Andrews, P.B.: Resolution in type theory. The J. of Symbolic Logic\u00a036, 414\u2013432 (1971)","journal-title":"The J. of Symbolic Logic"},{"key":"3_CR3","unstructured":"Andrews, P.B., Longini Cohen, E.: Theorem proving in type theory. In: Proc. of IJCAI 1977, pp. 566\u2013566 (1977)"},{"key":"3_CR4","unstructured":"Arenas-S\u00e1nchez, P., Dovier, A.: Minimal set unification. In: Alpuente, M., Sessa, M.I. (eds.) GULP-PRODE 1995, Marina di Vietri, Italy, September 11-14, pp. 447\u2013458 (1995)"},{"issue":"5","key":"3_CR5","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1017\/S0960129509990041","volume":"19","author":"A. Asperti","year":"2009","unstructured":"Asperti, A., Geuvers, H., Natarajan, R.: Social processes, program verification, and all that. Math. Struct. in Comp. Science\u00a019(5), 877\u2013896 (2009)","journal-title":"Math. Struct. in Comp. Science"},{"key":"3_CR6","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/10720084_17","volume-title":"Frontiers of Combining Systems","author":"F. Baader","year":"2000","unstructured":"Baader, F., Tinelli, C.: Combining equational theories sharing non-collapse-free constructors. In: Kirchner, H., Ringeissen, C. (eds.) FroCos 2000. LNCS (LNAI), vol.\u00a01794, pp. 260\u2013274. Springer, Heidelberg (2000)"},{"key":"3_CR7","series-title":"Algorithms and computation in mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in real algebraic geometry","author":"S. Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.-F.: Algorithms in real algebraic geometry. Algorithms and computation in mathematics, vol.\u00a010. Springer, Heidelberg (2006)"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BF01457985","volume":"86","author":"H. Behmann","year":"1922","unstructured":"Behmann, H.: Beitr\u00e4ge zur Algebra der Logik, insbesondere zum Entscheidungsproblem. Math. Annalen\u00a086, 163\u2013220 (1922)","journal-title":"Math. Annalen"},{"key":"3_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/978-3-540-45085-6_18","volume-title":"Automated Deduction \u2013 CADE-19","author":"J.G.F. Belinfante","year":"2003","unstructured":"Belinfante, J.G.F.: Reasoning about iteration in G\u00f6del\u2019s class theory. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 228\u2013242. Springer, Heidelberg (2003)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Bell\u00e8, D., Parlamento, F.: Decidability and completeness for open formulas of membership theories. Notre Dame J. of Formal Logic\u00a036 (1995)","DOI":"10.1305\/ndjfl\/1040248461"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Bell\u00e8, D., Parlamento, F.: The decidability of the \u2200\u2009*\u2009\u2203 class and the axiom of foundation. Notre Dame J. of Formal Logic\u00a042 (2001)","DOI":"10.1305\/ndjfl\/1054301354"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Bell\u00e8, D., Parlamento, F.: Truth in V for \u2203\u2009*\u2009\u2200\u2009\u2200-sentences is decidable. J. of Symbolic Logic\u00a071 (2006)","DOI":"10.2178\/jsl\/1164060452"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W.W. Bledsoe","year":"1977","unstructured":"Bledsoe, W.W.: Non-resolution theorem proving. Artificial Intelligence\u00a09, 1\u201335 (1977)","journal-title":"Artificial Intelligence"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1002\/cpa.3160340203","volume":"34","author":"M. Breban","year":"1981","unstructured":"Breban, M., Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision Procedures for Elementary Sublanguages of Set Theory II. Formulas involving Restricted Quantifiers, together with Ordinal, Integer, Map, and Domain Notions. Comm. Pure Appl. Math.\u00a034, 177\u2013195 (1981)","journal-title":"Comm. Pure Appl. Math."},{"key":"3_CR15","series-title":"London Mathematical Society Lecture Note Series","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511565847","volume-title":"Gr\u00f6ebner bases and Applications","author":"B. Buchberger","year":"1998","unstructured":"Buchberger, B., Winkler, F.: Gr\u00f6ebner bases and Applications. London Mathematical Society Lecture Note Series, vol.\u00a0251. Cambridge University Press, Cambridge (1998)"},{"key":"3_CR16","unstructured":"Burstall, R., Goguen, J.: Putting theories together to make specifications. In: Reddy, R. (ed.) Proc. 5th International Joint Conference on Artificial Intelligence, Cambridge, MA, pp. 1045\u20131058 (1977)"},{"key":"3_CR17","first-page":"31","volume":"63","author":"D. Cantone","year":"2008","unstructured":"Cantone, D., Chiaruttini, C., Nicolosi Asmundo, M., Omodeo, E.G.: Cumulative hierarchies and computability over universes of sets. Le Matematiche\u00a063, 31\u201384 (2008)","journal-title":"Le Matematiche"},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1002\/cpa.3160400303","volume":"40","author":"D. Cantone","year":"1987","unstructured":"Cantone, D., Cincotti, G.: Decision algorithms for some fragments of analysis and related areas. Comm. Pure Appl. Math.\u00a040, 281\u2013300 (1987)","journal-title":"Comm. Pure Appl. Math."},{"issue":"7","key":"3_CR19","doi-asserted-by":"publisher","first-page":"763","DOI":"10.1016\/j.jsc.2006.02.003","volume":"41","author":"D. Cantone","year":"2006","unstructured":"Cantone, D., Cincotti, G., Gallo, G.: Decision algorithms for fragments of real analysis. I. Continuous functions with strict convexity and concavity predicates. J. of Symbolic Computation\u00a041(7), 763\u2013789 (2006)","journal-title":"J. of Symbolic Computation"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/3-540-51084-2_39","volume-title":"Symbolic and Algebraic Computation","author":"D. Cantone","year":"1989","unstructured":"Cantone, D., Cutello, V., Ferro, A.: Decision procedures for elementary sublanguages of set theory. XIV. Three languages involving rank related constructs. In: Gianni, P. (ed.) ISSAC 1988. LNCS, vol.\u00a0358, pp. 407\u2013422. Springer, Heidelberg (1989)"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/3-540-54487-9_54","volume-title":"Computer Science Logic","author":"D. Cantone","year":"1991","unstructured":"Cantone, D., Cutello, V., Schwartz, J.T.: Decision problems for Tarski\u2019s and Presburger\u2019s arithmetics extended with sets. In: Sch\u00f6nfeld, W., B\u00f6rger, E., Kleine B\u00fcning, H., Richter, M.M. (eds.) CSL 1990. LNCS, vol.\u00a0533, pp. 95\u2013109. Springer, Heidelberg (1991)"},{"key":"3_CR22","first-page":"383","volume":"III","author":"D. Cantone","year":"1985","unstructured":"Cantone, D., Ferro, A.: Some recent decidability results in set theory. Atti degli incontri di Logica Matematica\u00a0III, 383\u2013387 (1985)","journal-title":"Atti degli incontri di Logica Matematica"},{"key":"3_CR23","unstructured":"Cantone, D., Ferro, A., Omodeo, E.G.: Computable set theory, Vol.1. Oxford Science Publications of International Series of Monographs on Computer Science, vol. no.6. Clarendon Press (1989)"},{"key":"3_CR24","unstructured":"Cantone, D., Ferro, A., Omodeo, E.G., Policriti, A.: Scomposizione sillogistica disgiuntiva. In: Mello [78], pp. 199\u2013209"},{"issue":"1","key":"3_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(87)90001-8","volume":"34","author":"D. Cantone","year":"1987","unstructured":"Cantone, D., Ferro, A., Schwartz, J.T.: Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator. J. of Computer and System Sciences\u00a034(1), 1\u201318 (1987)","journal-title":"J. of Computer and System Sciences"},{"key":"3_CR26","unstructured":"Cantone, D., Formisano, A., Omodeo, E.G., Schwartz, J.T.: Various commonly occurring decidable extensions of multi-level syllogistic. In: Ranise, S., Tinelli, C. (eds.) Pragmatics of Decision Procedures in Automated Reasoning, PDPAR 2003 (CADE-19), Electronic proceedings, Miami, USA (2003)"},{"key":"3_CR27","unstructured":"Cantone, D., Nicolosi Asmundo, M.: On the satisfiability problem for a 3-level quantified syllogistic. In: Complexity, Expressibility, and Decidability in Automated Reasoning \u2013 CEDAR 2008, Sydney, Australia, pp. 31\u201346 (2008)"},{"key":"3_CR28","first-page":"425","volume-title":"Proc. of the 11th International Joint Conference on Artificial Intelligence","author":"D. Cantone","year":"1989","unstructured":"Cantone, D., Omodeo, E.G.: On the decidability of formulae involving continuous and closed functions. In: Sridharan, N.S. (ed.) Proc. of the 11th International Joint Conference on Artificial Intelligence, pp. 425\u2013430. Morgan Kaufmann, San Francisco (1989)"},{"key":"3_CR29","series-title":"Monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3452-2","volume-title":"Set Theory for Computing. From Decision Procedures to Declarative Programming with Sets","author":"D. Cantone","year":"2001","unstructured":"Cantone, D., Omodeo, E.G., Policriti, A.: Set Theory for Computing. From Decision Procedures to Declarative Programming with Sets. Monographs in Computer Science. Springer, Heidelberg (2001)"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Cantone, D., Omodeo, E.G., Schwartz, J.T., Ursino, P.: Notes from the logbook of a proof-checker\u2019s project. In: Dershowitz (ed.) [45], pp. 182\u2013207","DOI":"10.1007\/978-3-540-39910-0_8"},{"key":"3_CR31","unstructured":"Cantone, D., Schwartz, J.T., Zarba, C.G.: Decision procedures for fragments of set theory with monotone and additive functions. In: Rossi, Jayaraman [106], pp. 1\u20138"},{"key":"#cr-split#-3_CR32.1","doi-asserted-by":"crossref","unstructured":"Cantone, D., Ursino, P., Omodeo, E.G.: Formative processes with applications to the decision problem in set theory: I. Powerset and singleton operators. Inf.??Comput.??172(2), 165???201 (2002);","DOI":"10.1006\/inco.2001.3096"},{"key":"#cr-split#-3_CR32.2","unstructured":"Appeared as Transitive Venn diagrams with applications to the decision problem in set theory. In: [79]"},{"key":"3_CR33","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-46508-1_8","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"D. Cantone","year":"2000","unstructured":"Cantone, D., Zarba, C.G.: A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol.\u00a01761, pp. 126\u2013136. Springer, Heidelberg (2000)"},{"key":"3_CR34","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-48754-9_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"D. Cantone","year":"1999","unstructured":"Cantone, D., Zarba, C.G.: A tableau-based decision procedure for a fragment of set theory involving a restricted form of quantification. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol.\u00a01617, pp. 97\u2013112. Springer, Heidelberg (1999)"},{"key":"3_CR35","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-7091-9459-1","volume-title":"Quantifier elimination and cylindrical algebraic decomposition","author":"B.F. Caviness","year":"1998","unstructured":"Caviness, B.F., Johnson, J.R.: Quantifier elimination and cylindrical algebraic decomposition. Texts and Monographs in Computer Science. Springer, Heidelberg (1998)"},{"key":"3_CR36","volume-title":"Mechanical Geometry Theorem Proving","author":"S.C. Chou","year":"1988","unstructured":"Chou, S.C.: Mechanical Geometry Theorem Proving. Reidel Publ. Comp., Dordrecht (1988)"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindric algebra decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"3_CR38","first-page":"113","volume-title":"JAF, 26\u00e8mes Journ\u00e9es sur les Arithm\u00e9tiques Faibles","author":"G. D\u2019Agostino","year":"2007","unstructured":"D\u2019Agostino, G., Omodeo, E.G., Schwartz, J.T., Tomescu, A.I.: Self-applied proof verification (Extended abstract). In: Cord\u00f3n-Franco, A., Fern\u00e1ndez-Margarit, A., Lara-Martin, F.F. (eds.) JAF, 26\u00e8mes Journ\u00e9es sur les Arithm\u00e9tiques Faibles, pp. 113\u2013117. F\u00e9nix Editora, Sevilla, Spain (2007), http:\/\/www.cs.us.es\/glm\/jaf26"},{"key":"3_CR39","unstructured":"Davis, M.: A program for Presburger\u2019s algorithm. In: Summary of talks presented at the Summer Institute for Symbolic Logic, pp. 215\u2013233. Cornell University (1957); In: [112]"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Davis, M.: Eliminating the irrelevant from mechanical proofs. In: Proc. of Symposia in Applied Mathematics, vol.\u00a015, pp. 15\u201330. AMS (1963); Reprinted in [112]","DOI":"10.1090\/psapm\/015\/0170497"},{"key":"3_CR41","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/B978-044450813-3\/50003-5","volume-title":"Handbook of Automated Reasoning","author":"M. Davis","year":"2001","unstructured":"Davis, M.: The early history of automated deduction. In: Handbook of Automated Reasoning, pp. 3\u201313. Elsevier, Amsterdam (2001)"},{"issue":"3","key":"3_CR42","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"J. of the ACM"},{"key":"3_CR43","unstructured":"Davis, M., Schwartz, J.T.: Correct-program technology \/ Extensibility of verifiers \u2013 Two papers on Program Verification with Appendix of Edith Deak. Technical Report No. NSO-12, Courant Institute of Mathematical Sciences, New York University (1977)"},{"key":"3_CR44","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0898-1221(79)90044-0","volume":"5","author":"M. Davis","year":"1979","unstructured":"Davis, M., Schwartz, J.T.: Metatheoretic extensibility for theorem verifiers and proof-checkers. Computers and Mathematics with Applications\u00a05, 217\u2013230 (1979)","journal-title":"Computers and Mathematics with Applications"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science","volume-title":"International symposium on verification (Theory and Practice) celebrating Zohar Manna\u2019s 10000002 th birthday","year":"2003","unstructured":"Dershowitz, N. (ed.): International symposium on verification (Theory and Practice) celebrating Zohar Manna\u2019s 10000002 th birthday. LNCS, vol.\u00a02772. Springer, Heidelberg (2003)"},{"key":"3_CR46","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol.\u00a0B, pp. 243\u2013320. Elsevier and MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"3_CR47","unstructured":"Dovier, A., Formisano, A., Omodeo, E.G.: Provable \u2203\u2009\u2009\u2217\u2009\u2009\u2200-sentences about sets with atoms. In: Rossi, Jayaraman [106], pp. 9\u201317"},{"issue":"2","key":"3_CR48","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/1131313.1131317","volume":"7","author":"A. Dovier","year":"2006","unstructured":"Dovier, A., Formisano, A., Omodeo, E.G.: Decidability results for sets with atoms. ACM Transactions on Computational Logic\u00a07(2), 269\u2013301 (2006)","journal-title":"ACM Transactions on Computational Logic"},{"key":"3_CR49","unstructured":"Dovier, A., Formisano, A., Policriti, A.: On T-logic programming. In: Falaschi, M., Navarro, M., Policriti, A. (eds.) Joint Conference on Declarative Programming, AGP 1997, Grado, Italy, June 16-19, pp. 457\u2013466 (1997)"},{"key":"#cr-split#-3_CR50.1","unstructured":"Dovier, A., Formisano, A., Policriti, A.: On T-logic programming. In: Proc. of ILPS 1997, pp. 323???337 (1997);"},{"key":"#cr-split#-3_CR50.2","unstructured":"A preliminary version appeared in [49]"},{"issue":"4","key":"3_CR51","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s002000050109","volume":"9","author":"A. Dovier","year":"1999","unstructured":"Dovier, A., Omodeo, E.G., Policriti, A.: Solvable set\/hyperset contexts: II. A goal-driven unification algorithm for the blended case. Appl. Algebra Eng. Commun. Comput.\u00a09(4), 293\u2013332 (1999)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"3_CR52","first-page":"111","volume-title":"ICLP 1991","author":"A. Dovier","year":"1991","unstructured":"Dovier, A., Omodeo, E.G., Pontelli, E., Rossi, G.: {log}: A logic programming language with finite sets. In: Furukawa, K. (ed.) ICLP 1991, pp. 111\u2013124. MIT Press, Cambridge (1991)"},{"key":"3_CR53","unstructured":"Dovier, A., Omodeo, E.G., Pontelli, E., Rossi, G.: {log}: A logic programming language with finite sets. In: Asirelli, P. (ed.) Sesto convegno nazionale di programmazione logica, GULP 1991, Pisa, pp. 241\u2013355 (1991)"},{"key":"3_CR54","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1007\/3-540-56454-3_8","volume-title":"Extensions of Logic Programming","author":"A. Dovier","year":"1993","unstructured":"Dovier, A., Omodeo, E.G., Pontelli, E., Rossi, G.: Embedding finite sets in a logic programming language. In: Lamma, E., Mello, P. (eds.) ELP 1992. LNCS (LNAI), vol.\u00a0660, pp. 150\u2013167. Springer, Heidelberg (1993)"},{"issue":"1","key":"3_CR55","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0743-1066(95)00147-6","volume":"28","author":"A. Dovier","year":"1996","unstructured":"Dovier, A., Omodeo, E.G., Pontelli, E., Rossi, G.: A language for programming in logic with finite sets. J. of Logic Programming\u00a028(1), 1\u201344 (1996); See also [52, 54, 53]","journal-title":"J. of Logic Programming"},{"key":"3_CR56","unstructured":"Dovier, A., Piazza, C., Rossi, G.: Narrowing the gap between set-constraints and CLP(SET)-constraints. In: Freire-Nistal, J.L., Falaschi, M., Ferro, M.V. (eds.) Joint Conference on Declarative Programming, AGP 1998, A\u00a0Coru\u00f1a, Spain, July 20-23, pp. 43\u201356 (1998)"},{"issue":"6","key":"3_CR57","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1017\/S1471068406002730","volume":"6","author":"A. Dovier","year":"2006","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory and Practice of Logic Programming\u00a06(6), 645\u2013701 (2006)","journal-title":"Theory and Practice of Logic Programming"},{"key":"3_CR58","unstructured":"Downey, P.J.: Undecidability of Presburger arithmetic with a single monadic predicate letter. Technical Report 18-72, Harvard University Center for Research in Computing Technology (1972)"},{"key":"3_CR59","volume-title":"The Decision Problem. Solvable classes of quantificational formulas","author":"B. Dreben","year":"1979","unstructured":"Dreben, B., Goldfarb, W.D.: The Decision Problem. Solvable classes of quantificational formulas. Addison-Wesley, Reading (1979)"},{"key":"3_CR60","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1070\/RM1965v020n04ABEH001188","volume":"20","author":"Y.L. Ershov","year":"1965","unstructured":"Ershov, Y.L., Lavrov, I.A., Taimanov, A.D., Taitslin, M.A.: Elementary theories. Russ. Math. Survey\u00a020, 35\u2013106 (1965)","journal-title":"Russ. Math. Survey"},{"key":"3_CR61","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W.M. Farmer","year":"1993","unstructured":"Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: An interactive mathematical proof system. J. Automated Reasoning\u00a011, 213\u2013248 (1993)","journal-title":"J. Automated Reasoning"},{"key":"3_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/3-540-10009-1_8","volume-title":"5th Conference on Automated Deduction","author":"A. Ferro","year":"1980","unstructured":"Ferro, A., Omodeo, E.G., Schwartz, J.T.: Decision procedures for some fragments of set theory. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol.\u00a087, pp. 88\u201396. Springer, Heidelberg (1980)"},{"key":"3_CR63","first-page":"27","volume-title":"Complexity and computation","author":"M.J. Fisher","year":"1974","unstructured":"Fisher, M.J., Rabin, M.O.: Super-exponential complexity of Presburger arithmetic. In: Complexity and computation, vol.\u00a0VII, pp. 27\u201341. SIAM-AMS, Philadelphia (1974)"},{"key":"3_CR64","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/3-540-46508-1_12","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"A. Formisano","year":"2000","unstructured":"Formisano, A., Omodeo, E.G.: An equational re-engineering of set theories. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol.\u00a01761, pp. 175\u2013190. Springer, Heidelberg (2000)"},{"key":"3_CR65","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/3-540-45744-5_12","volume-title":"Automated Reasoning","author":"A. Formisano","year":"2001","unstructured":"Formisano, A., Omodeo, E.G., Temperini, M.: Instructing equational set-reasoning with Otter. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 152\u2013167. Springer, Heidelberg (2001)"},{"issue":"4","key":"3_CR66","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1023\/A:1006170514174","volume":"22","author":"A. Formisano","year":"1999","unstructured":"Formisano, A., Policriti, A.: T-resolution: Refinements and model elimination. J. Automated Reasoning\u00a022(4), 433\u2013483 (1999)","journal-title":"J. Automated Reasoning"},{"key":"3_CR67","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s12046-009-0001-5","volume":"34","author":"H. Geuvers","year":"2009","unstructured":"Geuvers, H.: Proof assistants: History, ideas and future. S\u0101dhan\u0101\u00a034, 3\u201325 (2009)","journal-title":"S\u0101dhan\u0101"},{"issue":"3-4","key":"3_CR68","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/s10472-007-9078-x","volume":"50","author":"S. Ghilardi","year":"2007","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell.\u00a050(3-4), 231\u2013254 (2007)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1\/2","key":"3_CR69","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0747-7171(88)80006-3","volume":"5","author":"D. Grigoriev","year":"1988","unstructured":"Grigoriev, D.: Complexity of deciding Tarski algebra. J. of Symbolic Computation\u00a05(1\/2), 65\u2013108 (1988)","journal-title":"J. of Symbolic Computation"},{"key":"3_CR70","first-page":"165","volume":"46","author":"Y. Gurevich","year":"1965","unstructured":"Gurevich, Y.: Elementary properties of ordered Abelian groups. Translations of AMS\u00a046, 165\u2013192 (1965)","journal-title":"Translations of AMS"},{"issue":"20","key":"3_CR71","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19","author":"J. Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.J.: Constraint logic programming: a survey. J. of Logic Programming\u00a0(19\/20), 503\u2013581 (1994)","journal-title":"J. of Logic Programming"},{"issue":"2","key":"3_CR72","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1016\/j.jalgebra.2006.03.033","volume":"302","author":"O. Kharlampovich","year":"2006","unstructured":"Kharlampovich, O., Myasnikov, A.: Elementary theory of free non-Abelian groups. J. of Algebra\u00a0302(2), 451\u2013552 (2006)","journal-title":"J. of Algebra"},{"key":"3_CR73","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D.E. Knuth","year":"1970","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013267. Pergamon Press, Oxford (1970)"},{"key":"3_CR74","series-title":"Springer Monographs in Mathematics","volume-title":"Applied Proof Theory: Proof Interpretations and their Use in Mathematics","author":"U. Kohlenbach","year":"2008","unstructured":"Kohlenbach, U.: Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer, Heidelberg (2008)"},{"key":"3_CR75","series-title":"Texts in Theoretical Computer Science","volume-title":"Decision procedures: an algorithmic point of view","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision procedures: an algorithmic point of view. Texts in Theoretical Computer Science. Springer, Heidelberg (2008)"},{"key":"3_CR76","doi-asserted-by":"crossref","unstructured":"Loveland, D.W.: Automated theorem proving: A quarter century review. In: Bledsoe, W.W., Loveland, D.W. (eds.) Contemporary Mathematics: Automated Theorem Proving - After 25 Years, pp. 1\u201345. AMS (1984)","DOI":"10.1090\/conm\/029\/749237"},{"key":"3_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/978-3-540-40007-3_24","volume-title":"Formal Methods at the Cross Roads. From Panacea to Foundational Support","author":"Z. Manna","year":"2003","unstructured":"Manna, Z., Zarba, C.G.: Combining decision procedures. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Cross Roads: From Panacea to Foundational Support. LNCS, vol.\u00a02757, pp. 381\u2013422. Springer, Heidelberg (2003)"},{"key":"3_CR78","unstructured":"Mello, P. (ed.): Quarto convegno nazionale di programmazione logica. In: GULP 1989, Bologna (1989)"},{"key":"3_CR79","unstructured":"Meo, M.C., Vilares Ferro, M. (eds.): Joint Conference on Declarative Programming, AGP 1999, L\u2019Aquila, Italy, September 6-9. GTE (1999)"},{"issue":"2","key":"3_CR80","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1305\/ndjfl\/1094061860","volume":"35","author":"F. Montagna","year":"1994","unstructured":"Montagna, F., Mancini, A.: A minimal predicative set theory. Notre Dame J. of Formal Logic\u00a035(2), 186\u2013203 (1994)","journal-title":"Notre Dame J. of Formal Logic"},{"issue":"2","key":"3_CR81","doi-asserted-by":"publisher","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 Transaction on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transaction on Programming Languages and Systems"},{"issue":"2","key":"3_CR82","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. of the ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"J. of the ACM"},{"key":"3_CR83","series-title":"LNCS","first-page":"428","volume-title":"TACAS-ETAPS 2009","author":"E. Nicolini","year":"2009","unstructured":"Nicolini, E., Ringeissen, C., Rusinowitch, M.: Satisfiability procedures for combination of theories sharing integer offsets. In: Kowalewski, S., Philippou, A. (eds.) TACAS-ETAPS 2009. LNCS, vol.\u00a05505, pp. 428\u2013442. Springer, Heidelberg (2009); Also in CILC 2009: 24-esimo Convegno Italiano di Logica Computazionale"},{"issue":"1-4","key":"3_CR84","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s10472-009-9118-9","volume":"53","author":"I. Niemel\u00e4","year":"2008","unstructured":"Niemel\u00e4, I.: Stable models and difference logic. Ann. Math. Artif. Intell.\u00a053(1-4), 313\u2013329 (2008)","journal-title":"Ann. Math. Artif. Intell."},{"key":"3_CR85","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0898-1221(82)90042-6","volume":"8","author":"E.G. Omodeo","year":"1982","unstructured":"Omodeo, E.G.: The Linked Conjunct method for automatic deduction and related search techniques. Computers and Mathematics with Applications\u00a08, 185\u2013203 (1982)","journal-title":"Computers and Mathematics with Applications"},{"key":"3_CR86","unstructured":"Omodeo, E.G., Bossi, A., Sambin, G.: Tre possibili orientamenti per una programmazione dichiarativa basata sulla teoria degli insiemi. In: Demo, B. (ed.) Secondo convegno nazionale di programmazione logica, GULP 1987, Torino, pp. 265\u2013276 (1987)"},{"key":"3_CR87","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/11829263_7","volume-title":"Reasoning, Action and Interaction in AI Theories and Systems","author":"E.G. Omodeo","year":"2006","unstructured":"Omodeo, E.G., Cantone, D., Policriti, A., Schwartz, J.T.: A computerized Referee. In: Stock, O., Schaerf, M. (eds.) Reasoning, Action and Interaction in AI Theories and Systems. LNCS (LNAI), vol.\u00a04155, pp. 117\u2013139. Springer, Heidelberg (2006)"},{"issue":"5-6","key":"3_CR88","doi-asserted-by":"publisher","first-page":"673","DOI":"10.1016\/S0747-7171(06)80009-X","volume":"15","author":"E.G. Omodeo","year":"1993","unstructured":"Omodeo, E.G., Parlamento, F., Policriti, A.: A derived algorithm for evaluating \u03b5-expressions over abstract sets. J. of Symbolic Computation\u00a015(5-6), 673\u2013704 (1993)","journal-title":"J. of Symbolic Computation"},{"key":"3_CR89","doi-asserted-by":"crossref","unstructured":"Omodeo, E.G., Parlamento, F., Policriti, A.: Decidability of \u2203\u2009\u2009\u2217\u2009\u2009\u2200-sentences in membership theories. Mathematical Logic Quarterly (formerly Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik)\u00a042 (1996)","DOI":"10.1002\/malq.19960420105"},{"issue":"9-10","key":"3_CR90","doi-asserted-by":"crossref","first-page":"1123","DOI":"10.1002\/cpa.3160480908","volume":"48","author":"E.G. Omodeo","year":"1995","unstructured":"Omodeo, E.G., Policriti, A.: Solvable set\/hyperset contexts: I. Some decision procedures for the pure, finite case. Comm. Pure Appl. Math.\u00a048(9-10), 1123\u20131155 (1995); Special Issue in honor of J.T. Schwartz","journal-title":"Comm. Pure Appl. Math."},{"key":"3_CR91","doi-asserted-by":"crossref","unstructured":"Omodeo, E.G., Policriti, A.: The Bernays-Sch\u00f6nfinkel-Ramsey class for set theory: semidecidability. J. of Symbolic Logic (2010)","DOI":"10.2178\/jsl\/1268917490"},{"key":"3_CR92","unstructured":"Omodeo, E.G., Policriti, A., Rossi, G.: Che genere di insiemi\/multi-insiemi\/iper-insiemi incorporare nella programazione logica? In: Sacc\u00e0, D. (ed.) GULP 1993, pp. 55\u201370 (1993)"},{"key":"3_CR93","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/3-540-45632-5_9","volume-title":"Computational Logic: Logic Programming and Beyond","author":"E.G. Omodeo","year":"2002","unstructured":"Omodeo, E.G., Schwartz, J.T.: A \u2018Theory\u2019 mechanism for a proof-verifier based on first-order set theory. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol.\u00a02408, pp. 214\u2013230. Springer, Heidelberg (2002)"},{"key":"3_CR94","first-page":"85","volume":"63","author":"E.G. Omodeo","year":"2008","unstructured":"Omodeo, E.G., Tomescu, A.I.: Using \u00c6tnaNova to formally prove that the Davis-Putnam satisfiability test is correct. Le Matematiche\u00a063, 85\u2013105 (2008); A preliminary version was presented at CILC 2007 (Messina)","journal-title":"Le Matematiche"},{"key":"3_CR95","doi-asserted-by":"crossref","unstructured":"Papadimitriou, C.: On the complexity of integer programming. J. of the ACM\u00a028 (1981)","DOI":"10.1145\/322276.322287"},{"key":"3_CR96","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1002\/cpa.3160410206","volume":"XLI","author":"F. Parlamento","year":"1988","unstructured":"Parlamento, F., Policriti, A.: Decision procedures for elementary sublanguages of set theory. IX: Unsolvability of the decision problem for a restricted subclass of the \u03940-formulas in set theory. Comm. Pure Appl. Math.\u00a0XLI, 221\u2013251 (1988)","journal-title":"Comm. Pure Appl. Math."},{"issue":"2","key":"3_CR97","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00243810","volume":"7","author":"F. Parlamento","year":"1991","unstructured":"Parlamento, F., Policriti, A.: Decision procedures for elementary sublanguages of set theory: XIII. Model graphs, reflection and decidability. J. Automated Reasoning\u00a07(2), 271\u2013284 (1991)","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"3_CR98","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF00881916","volume":"15","author":"L.C. Paulson","year":"1995","unstructured":"Paulson, L.C.: Set Theory for Verification. II: Induction and Recursion. J. Automated Reasoning\u00a015(2), 167\u2013215 (1995)","journal-title":"J. Automated Reasoning"},{"issue":"3","key":"3_CR99","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1006\/jsco.1995.1053","volume":"20","author":"A. Policriti","year":"1995","unstructured":"Policriti, A., Schwartz, J.T.: T-theorem proving.\u00a0I. J. of Symbolic Computation\u00a020(3), 315\u2013342 (1995)","journal-title":"J. of Symbolic Computation"},{"key":"3_CR100","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/321021.321023","volume":"7","author":"D. Prawitz","year":"1960","unstructured":"Prawitz, D., Prawitz, H., Voghera, N.: A mechanical proof procedure and its realization in an electronic computer. J. of the ACM\u00a07, 102\u2013128 (1960); Reprinted in [112]","journal-title":"J. of the ACM"},{"key":"3_CR101","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, Warsaw, pp. 92\u2013101 (1929)"},{"issue":"1","key":"3_CR102","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A. Quaife","year":"1992","unstructured":"Quaife, A.: Automated Deduction in von Neumann-Bernays-G\u00f6del Set Theory. J. Automated Reasoning\u00a08(1), 91\u2013147 (1992)","journal-title":"J. Automated Reasoning"},{"key":"3_CR103","first-page":"291","volume-title":"29th Annual Symposium on Foundations of Computer Science (FOCS 1988)","author":"J. Renegar","year":"1988","unstructured":"Renegar, J.: A faster PSPACE algorithm for deciding the existential theory of the reals. In: 29th Annual Symposium on Foundations of Computer Science (FOCS 1988), Los Angeles, Ca., USA, pp. 291\u2013295. IEEE Computer Society Press, Los Alamitos (1988)"},{"issue":"1","key":"3_CR104","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. of the ACM\u00a012(1), 23\u201341 (1965); Reprinted in [112]","journal-title":"J. of the ACM"},{"key":"3_CR105","unstructured":"Robu, J.: Geometry Theorem Proving in the Frame of the Theorema Project. Technical Report 02-23, RISC Report Series, University of Linz, Austria. PhD Thesis (2002)"},{"key":"3_CR106","unstructured":"Rossi, G., Jayaraman, B. (eds.): Proc. of the Workshop on Declarative Programming with Sets, DPS 1999, Paris. Technical Report N. 200, Dipartimento di Matematica, Universit\u00e0 di Parma, Italy (1999)"},{"key":"3_CR107","unstructured":"Schwartz, J.T.: Instantiation and decision procedures for certain classes of quantified set-theoretic formulae. Technical Report 78-10, Institute for Computer Applications in Science and Engineering, NASA Langley Research Center, Hampton, Virginia (1978)"},{"key":"3_CR108","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-9575-1","volume-title":"Programming with sets: An introduction to SETL","author":"J.T. Schwartz","year":"1986","unstructured":"Schwartz, J.T., Dewar, R.K.B., Dubinsky, E., Schonberg, E.: Programming with sets: An introduction to SETL. Texts and Monographs in Computer Science. Springer, Heidelberg (1986)"},{"key":"3_CR109","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45610-4_1","volume-title":"Rewriting Techniques and Applications","author":"N. Shankar","year":"2002","unstructured":"Shankar, N., Rue\u00df, H.: Combining Shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 1\u201318. Springer, Heidelberg (2002)"},{"issue":"2","key":"3_CR110","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R.E. Shostak","year":"1979","unstructured":"Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. J. of the ACM\u00a026(2), 351\u2013360 (1979)","journal-title":"J. of the ACM"},{"key":"3_CR111","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. J. of the ACM\u00a031, 1\u201312 (1984)","journal-title":"J. of the ACM"},{"key":"3_CR112","volume-title":"Automation of Reasoning I and II","author":"J. Siekmann","year":"1983","unstructured":"Siekmann, J., Wrightson, G.: Automation of Reasoning I and II. Springer, Heidelberg (1983)"},{"issue":"3-4","key":"3_CR113","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J.H. Siekmann","year":"1989","unstructured":"Siekmann, J.H.: Unification theory. J. of Symbolic Computation\u00a07(3-4), 207\u2013274 (1989)","journal-title":"J. of Symbolic Computation"},{"key":"3_CR114","unstructured":"Sigal, R.: Desiderata for logic programming with sets. In: Mello [78], pp. 127\u2013141"},{"issue":"4","key":"3_CR115","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M.E. Stickel","year":"1985","unstructured":"Stickel, M.E.: Automated deduction by theory resolution. J. Automated Reasoning\u00a01(4), 333\u2013355 (1985)","journal-title":"J. Automated Reasoning"},{"key":"3_CR116","doi-asserted-by":"crossref","first-page":"203","DOI":"10.4064\/fm-41-2-203-271","volume":"41","author":"W. Szmielew","year":"1954","unstructured":"Szmielew, W.: Elementary properties of Abelian groups. Fundamenta Mathematicae\u00a041, 203\u2013271 (1954)","journal-title":"Fundamenta Mathematicae"},{"key":"3_CR117","doi-asserted-by":"crossref","first-page":"45","DOI":"10.4064\/fm-6-1-45-95","volume":"VI","author":"A. Tarski","year":"1924","unstructured":"Tarski, A.: Sur les ensembles fini. Fundamenta Mathematicae\u00a0VI, 45\u201395 (1924)","journal-title":"Fundamenta Mathematicae"},{"key":"3_CR118","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Berkeley University Press (1951)","DOI":"10.1525\/9780520348097"},{"key":"3_CR119","first-page":"164","volume-title":"The philosophy of mathematics \u2014 Oxford readings in philosophy","author":"A. Tarski","year":"1969","unstructured":"Tarski, A.: What is elementary geometry? In: Hintikka, J. (ed.) The philosophy of mathematics \u2014 Oxford readings in philosophy, pp. 164\u2013175. Oxford University Press, Oxford (1969); First published in 1959"},{"issue":"1","key":"3_CR120","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/S0304-3975(01)00332-2","volume":"290","author":"C. Tinelli","year":"2003","unstructured":"Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theoretical Computer Science\u00a0290(1), 291\u2013353 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"3_CR121","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C. Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Automated Reasoning\u00a034(3), 209\u2013238 (2005)","journal-title":"J. Automated Reasoning"},{"key":"3_CR122","doi-asserted-by":"crossref","unstructured":"Vaught, R.L.: On a theorem of Cobham concerning undecidable theories. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Proc. of the 1960 International Congress on Logic, Methodology, and Philosophy of Science, pp. 14\u201325. Stanford University Press (1962)","DOI":"10.1016\/S0049-237X(09)70566-X"},{"issue":"1","key":"3_CR123","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/BF00245023","volume":"5","author":"L. Wos","year":"1989","unstructured":"Wos, L.: The problem of finding an inference rule for set theory. J. Automated Reasoning\u00a05(1), 93\u201395 (1989)","journal-title":"J. Automated Reasoning"},{"key":"#cr-split#-3_CR124.1","unstructured":"Wu, W.-T.: On the decision problem and the mechanization of theorem-proving in elementary geometry. Scientia Sinica??21(2), 159???172 (1978);"},{"key":"#cr-split#-3_CR124.2","unstructured":"Also in Selected works of Wen-Ts??n Wu. World Scientific Publishing, Singapore (2008)"},{"key":"3_CR125","unstructured":"Zarba, C.G.: Combining lists with integers. In: Gor\u00e9, R., Leitsch, A., Nipkov, T. (eds.) International Joint Conference on Automated Reasoning, IJCAR 2001 (Short Papers), Technical Report DII 11\/01, pp. 180\u2013189. University of Siena, Italy (2001)"},{"key":"3_CR126","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-45620-1_30","volume-title":"Automated Deduction - CADE-18","author":"C.G. Zarba","year":"2002","unstructured":"Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, p. 363. Springer, Heidelberg (2002)"},{"key":"3_CR127","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45988-X_9","volume-title":"Frontiers of Combining Systems","author":"C.G. Zarba","year":"2002","unstructured":"Zarba, C.G.: Combining sets with integers. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol.\u00a02309, p. 103. Springer, Heidelberg (2002)"},{"key":"3_CR128","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/3-540-45616-3_22","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"C.G. Zarba","year":"2002","unstructured":"Zarba, C.G.: A tableau calculus for combining non-disjoint theories. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 315\u2013329. Springer, Heidelberg (2002)"},{"key":"3_CR129","doi-asserted-by":"crossref","unstructured":"Zarba, C.G.: Combining sets with elements. In: Dershowitz [45], pp. 762\u2013782","DOI":"10.1007\/978-3-540-39910-0_33"},{"issue":"1","key":"3_CR130","doi-asserted-by":"publisher","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. Automated Reasoning\u00a034(1), 1\u201329 (2005)","journal-title":"J. Automated Reasoning"},{"issue":"3-4","key":"3_CR131","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s10817-004-6243-3","volume":"33","author":"C.G. Zarba","year":"2004","unstructured":"Zarba, C.G., Cantone, D., Schwartz, J.T.: A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions, I: The two-level case. J. Automated Reasoning\u00a033(3-4), 251\u2013269 (2004)","journal-title":"J. Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","A 25-Year Perspective on Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14309-0_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,30]],"date-time":"2021-10-30T01:17:34Z","timestamp":1635556654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14309-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642143083","9783642143090"],"references-count":134,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14309-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}