{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,19]],"date-time":"2023-01-19T06:49:15Z","timestamp":1674110955331},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2004,10,1]],"date-time":"2004-10-01T00:00:00Z","timestamp":1096588800000},"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":[[2004,10]]},"DOI":"10.1007\/s10817-004-6243-3","type":"journal-article","created":{"date-parts":[[2005,3,8]],"date-time":"2005-03-08T14:23:45Z","timestamp":1110291825000},"page":"251-269","source":"Crossref","is-referenced-by-count":3,"title":["A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions, I: The Two-Level Case"],"prefix":"10.1007","volume":"33","author":[{"given":"Calogero G.","family":"Zarba","sequence":"first","affiliation":[]},{"given":"Domenico","family":"Cantone","sequence":"additional","affiliation":[]},{"given":"Jacob T.","family":"Schwartz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,2,28]]},"reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings, Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Beckert, B. and Hartmer, U.: A tableau calculus for quantifier-free set theoretic formulae, in H. C. M. de Swart (ed.), Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Comput. Sci. 1397, Springer, 1998, pp. 93?107.","DOI":"10.1007\/3-540-69778-0_16"},{"key":"CR3","unstructured":"Cantone, D., Ferro, A. and Omodeo, E. G.: Computable Set Theory, International Series of Monographs on Computer Science 6, Clarendon Press, 1989."},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"Cantone, D., Omodeo, E. G. and Policriti, A.: Set Theory for Computing. From Decision Procedures to Logic Programming with Sets, Monographs in Computer Science, Springer, 2001.","DOI":"10.1007\/978-1-4757-3452-2"},{"key":"CR5","unstructured":"Cantone, D., Schwartz, J. T. and Zarba, C. G.: A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions, in I. Dahn and L. Vigneron (eds.), First-Order Theorem Proving, Electron. Notes in Theoret. Comput. Sci. 86.1, Elsevier, 2003."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Cantone, D. and Zarba, C. G.: A tableau calculus for integrating first-order reasoning with elementary set theory reasoning, in R. Dyckhoff (ed.), Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Comput. Sci. 1847, Springer, 2000, pp. 143?159.","DOI":"10.1007\/10722086_14"},{"key":"CR7","first-page":"130","volume":"33","author":"A. Ferro","year":"1978","unstructured":"Ferro, A. and Omodeo, E. G.: An efficient validity test for formulae in extensional two-level syllogistic, Le Matematiche 33 (1978), 130?137.","journal-title":"Le Matematiche"},{"issue":"5","key":"CR8","doi-asserted-by":"crossref","first-page":"599","DOI":"10.1002\/cpa.3160330503","volume":"33","author":"A. Ferro","year":"1980","unstructured":"Ferro, A., Omodeo, E. G. and Schwartz, J. T.: Decision procedures for elementary sublanguages of set theory, I: Multi-level syllogistic and some extensions, Comm. Pure Appl. Math. 33(5) (1980), 599?608.","journal-title":"Comm. Pure Appl. Math."},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Ferro, A., Omodeo E. G. and Schwartz, J. T.: Decision procedures for some fragments of set theory, in W. Bibel and R. A. Kowalski (eds.), 5th Conference on Automated Deduction, Lecture Notes in Comput. Sci. 87, Springer, 1980, pp. 88?96.","DOI":"10.1007\/3-540-10009-1_8"},{"issue":"2","key":"CR10","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G. and Oppen, D. C.: Simplification by cooperating decision procedures, ACM Trans. on Programming Languages and Systems 1(2) (1979), 245?257.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"Schwartz, J. T., Dewar, R. B. K., Dubinsky, E. and Schonberg, E.: Programming with Sets: An Introduction to SETL, Springer, 1986.","DOI":"10.1007\/978-1-4613-9575-1"},{"key":"CR12","unstructured":"Spivey, J. M.: Understanding Z: A Specification Language and Its Formal Semantics, Cambridge Tracts in Theoretical Computer Science 3, Cambridge University Press, 1988."},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"Tinelli, C. and Zarba, C. G.: Combining decision procedures for sorted theories, in J. J. Alferes and J. A. Leite (eds.), Logics in Artificial Intelligence, Lecture Notes in Comput. Sci. 3229, Springer, 2004, pp. 641?653.","DOI":"10.1007\/978-3-540-30227-8_53"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Zarba, C. G.: Combining multisets with integers, in A. Voronkov (ed.), Automated Deduction ? CADE-18, Lecture Notes in Comput. Sci. 2392, Springer, 2002, pp. 363?376.","DOI":"10.1007\/3-540-45620-1_30"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Zarba, C. G.: Combining sets with integers, in A. Armando (ed.), Frontiers of Combining Systems, Lecture Notes in Comput. Sci. 2309, Springer, 2002, pp. 103?116.","DOI":"10.1007\/3-540-45988-X_9"},{"key":"CR16","unstructured":"Zarba, C. G.: Combining sets with elements, in N. Dershowitz (ed.), Verification: Theory and Practice, Lecture Notes in Comput. Sci. 2772, Springer, 2004, pp. 762?782."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-6243-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-004-6243-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-6243-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T07:17:13Z","timestamp":1586157433000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-004-6243-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,10]]},"references-count":16,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2004,10]]}},"alternative-id":["6243"],"URL":"https:\/\/doi.org\/10.1007\/s10817-004-6243-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,10]]}}}