{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:34Z","timestamp":1725488614559},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540671909"},{"type":"electronic","value":"9783540465089"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_12","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:02:03Z","timestamp":1186156923000},"page":"175-190","source":"Crossref","is-referenced-by-count":6,"title":["An Equational Re-engineering of Set Theories"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Formisano","sequence":"first","affiliation":[]},{"given":"Eugenio","family":"Omodeo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"P. B. Andrews, D. Miller, E. Longini Cohen, and F. Pfenning. Automating higher-order logic. In W. W. Bledsoe and D. W. Loveland eds., Automated theorem proving: After 25 years, 169\u2013192. American Mathematical Society, Contemporary Mathematics vol.29, 1984.","DOI":"10.1090\/conm\/029\/09"},{"issue":"3","key":"12_CR2","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/BF00881874","volume":"11","author":"S. C. Bailin","year":"1993","unstructured":"S. C. Bailin and D. Barker-Plummer. $$ \\mathcal{Z} $$ -match: An inference rule for incrementally elaborating set instantiations. J. Automated Reasoning, 11(3):391\u2013428, 1993. (Errata in J. Automated Reasoning, 12(3):411\u2013412, 1994).","journal-title":"J. Automated Reasoning"},{"key":"12_CR3","first-page":"10","volume":"34","author":"J. G. F. Belinfante","year":"1996","unstructured":"J. G. F. Belinfante. On a modification of G\u00f6del\u2019s algorithm for class formation. AAR Newsletter No.34, 10\u201315, 1996.","journal-title":"AAR Newsletter"},{"issue":"3","key":"12_CR4","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF02328452","volume":"2","author":"R. Boyer","year":"1986","unstructured":"R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos. Set theory in first-order logic: Clauses for G\u00f6del\u2019s axioms. J. Automated Reasoning, 2(3):287\u2013327, 1986.","journal-title":"J. Automated Reasoning"},{"key":"12_CR5","unstructured":"D. Cantone, A. Cavarra, and E. G. Omodeo. On existentially quantified conjunctions of atomic formulae of $$ \\mathcal{L}^ + $$ . In M. P. Bonacina and U. Furbach, eds., Proc. of the FTP97 International workshop on first-order theorem proving, RISC-Linz Report Series No.97-50, pp. 45\u201352, 1997."},{"key":"12_CR6","unstructured":"D. Cantone, A. Ferro, and E. G. Omodeo. Computable set theory. Vol. 1. Int. Series of Monographs on Computer Science. Oxford University Press, 1989."},{"key":"12_CR7","volume-title":"Set Theory and the continuum hypothesis","author":"P. J. Cohen","year":"1966","unstructured":"P. J. Cohen. Set Theory and the continuum hypothesis. Benjamin, New York, 1966."},{"key":"12_CR8","doi-asserted-by":"crossref","first-page":"321","DOI":"10.3233\/FI-1994-2143","volume":"21","author":"I. D\u00fcntsch","year":"1994","unstructured":"I. D\u00fcntsch. Rough relation algebras. Fundamenta Informaticae, 21:321\u2013331, 1994.","journal-title":"Fundamenta Informaticae"},{"key":"12_CR9","unstructured":"A. Formisano, E. G. Omodeo, and M. Temperini. Plan of activities on the map calculus. In J. L. Freire-Nistal, M. Falaschi, and M. Vilares Ferro, eds., Proc. of the AGP98 Joint Conference on Declarative Programming, pp. 343\u2013356, A Coru\u00f1a, Spain, 1998."},{"issue":"3","key":"12_CR10","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1093\/jigpal\/5.3.1","volume":"5","author":"M. F. Frias","year":"1997","unstructured":"M. F. Frias, A. M. Haeberer, and P. A. S. Veloso. A finite axiomatization for fork algebras. J. of the IGPL, 5(3):311\u2013319, 1997.","journal-title":"J. of the IGPL"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"S. R. Givant. The Structure of Relation Algebras Generated by Relativization, volume 156 of Contemporary Mathematics. American Mathematical Society, 1994.","DOI":"10.1090\/conm\/156"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"D. Gries and F. B. Schneider. A logical approach to discrete math. Texts and Monographs in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4757-3837-7"},{"key":"12_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/BFb0039715","volume-title":"Proc. of the International Conference on Formal Methods in Programming and their Applications","author":"A. M. Haeberer","year":"1993","unstructured":"A. M. Haeberer, G. A. Baum, and G. Schmidt. On the smooth calculation of relational recursive expressions out of first-order non-constructive specifications involving quantifiers. In Proc. of the International Conference on Formal Methods in Programming and their Applications. LNCS 735:281\u2013298. Springer-Verlag, 1993."},{"key":"12_CR14","volume-title":"Set theory","author":"T. J. Jech","year":"1978","unstructured":"T. J. Jech Set theory, Academic Press, New York, 1978."},{"key":"12_CR15","unstructured":"B. J\u00f3nsson and A. Tarski. Representation problems for relation algebras. Bull. Amer. Math. Soc., 54, 1948"},{"key":"12_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-010-3144-8","volume-title":"Introduction to axiomatic set theory","author":"J.-L. Krivine","year":"1971","unstructured":"J.-L. Krivine Introduction to axiomatic set theory, Reidel, Dordrecht. Holland, 1971."},{"issue":"3","key":"12_CR17","doi-asserted-by":"publisher","first-page":"707","DOI":"10.2307\/1969375","volume":"51","author":"R. C. Lyndon","year":"1950","unstructured":"R. C. Lyndon The representation of relational algebras. Annals of Mathematics, 51(3):707\u2013729, 1950.","journal-title":"Annals of Mathematics"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"W. W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL-94\/6, Argonne National Laboratory, 1994. (Revision A, august 1995).","DOI":"10.2172\/10129052"},{"issue":"1","key":"12_CR19","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/BF00881863","volume":"10","author":"Ph. A. J. No\u00ebl","year":"1993","unstructured":"Ph. A. J. No\u00ebl. Experimenting with Isabelle in ZF set theory. J. Automated Reasoning, 10(1):15\u201358, 1993.","journal-title":"J. Automated Reasoning"},{"issue":"9\u201310","key":"12_CR20","doi-asserted-by":"publisher","first-page":"1123","DOI":"10.1002\/cpa.3160480908","volume":"48","author":"E. G. Omodeo","year":"1995","unstructured":"E. G. Omodeo and A. Policriti. Solvable set\/hyperset contexts: I. Some decision procedures for the pure, finite case. Comm. Pure App. Math., 48(9\u201310):1123\u20131155, 1995. Special Issue in honor of J.T. Schwartz.","journal-title":"Comm. Pure App. Math."},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"E. Orlowska. Relational semantics for nonclassical logics: Formulas are relations. In Wolenski, J. ed. Philosophical Logic in Poland, pages 167\u2013186, 1994.","DOI":"10.1007\/978-94-015-8273-5_11"},{"issue":"4","key":"12_CR22","doi-asserted-by":"publisher","first-page":"1230","DOI":"10.2307\/2275470","volume":"56","author":"F. Parlamento","year":"1991","unstructured":"F. Parlamento and A. Policriti. Expressing infinity without foundation. J. Symbolic Logic, 56(4):1230\u20131235, 1991.","journal-title":"J. Symbolic Logic"},{"issue":"3","key":"12_CR23","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L. C. Paulson","year":"1993","unstructured":"L. C. Paulson. Set Theory for verification: I. From foundations to functions. J. Automated Reasoning, 11(3):353\u2013389, 1993.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"12_CR24","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF00881916","volume":"15","author":"L. C. Paulson","year":"1995","unstructured":"L. C. Paulson. Set Theory for verification. II: Induction and recursion. J. Automated Reasoning, 15(2):167\u2013215, 1995.","journal-title":"J. Automated Reasoning"},{"issue":"3","key":"12_CR25","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/BF00283132","volume":"17","author":"L. C. Paulson","year":"1996","unstructured":"L. C. Paulson and K. Grabczewski. Mechanizing set theory. J. Automated Reasoning, 17(3):291\u2013323, 1996.","journal-title":"J. Automated Reasoning"},{"issue":"1","key":"12_CR26","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A. Quaife","year":"1992","unstructured":"A. Quaife. Automated deduction in von Neumann-Bernays-G\u00f6del Set Theory. J. Automated Reasoning, 8(1):91\u2013147, 1992.","journal-title":"J. Automated Reasoning"},{"key":"12_CR27","unstructured":"A. Quaife. Automated development of fundamental mathematical theories. Kluwer Academic Publishers, 1992."},{"key":"12_CR28","volume-title":"Set theory and its logic","author":"W. V. Quine","year":"1971","unstructured":"W. V. Quine. Set theory and its logic. The Belknap Press of Harvard University Press, Cambridge, Massachussetts, revised edition, 3rd printing, 1971."},{"key":"12_CR29","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0012-365X(85)90064-0","volume":"54","author":"G. Schmidt","year":"1985","unstructured":"G. Schmidt and T. Str\u00f6hlein. Relation algebras: concepts of points and representability. Discrete Mathematics, 54:83\u201392, 1985.","journal-title":"Discrete Mathematics"},{"key":"12_CR30","unstructured":"J. R. Shoenfield. Mathematical logic. Addison Wesley, 1967."},{"key":"12_CR31","doi-asserted-by":"crossref","first-page":"45","DOI":"10.4064\/fm-6-1-45-95","volume":"6","author":"A. Tarski","year":"1924","unstructured":"A. Tarski. Sur les ensembles fini. Fundamenta Mathematicae, 6:45\u201395, 1924.","journal-title":"Fundamenta Mathematicae"},{"issue":"3","key":"12_CR32","doi-asserted-by":"publisher","first-page":"73","DOI":"10.2307\/2268577","volume":"6","author":"A. Tarski","year":"1941","unstructured":"A. Tarski. On the calculus of relations. Journal of Symbolic Logic, 6(3):73\u201389, 1941.","journal-title":"Journal of Symbolic Logic"},{"key":"12_CR33","doi-asserted-by":"crossref","unstructured":"A. Tarski and S. Givant. A formalization of set theory without variables, volume 41 of Colloquium Publications. American Mathematical Society, 1987.","DOI":"10.1090\/coll\/041"},{"key":"12_CR34","unstructured":"L. Wos. Automated reasoning. 33 basic research problems. Prentice Hall, 1988."},{"issue":"1","key":"12_CR35","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/BF00245023","volume":"5","author":"L. Wos","year":"1989","unstructured":"L. Wos. The problem of finding an inference rule for set theory. J. Automated Reasoning, 5(1):93\u201395, 1989.","journal-title":"J. Automated Reasoning"},{"key":"12_CR36","unstructured":"E. Zermelo. Untersuchungen \u00fcber die Grundlagen der Mengenlehre I. In From Frege to G\u00f6del-A source book in Mathematical Logic, 1879\u20131931, pages 199\u2013215. Harvard University Press, 1977."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Classical and Non-Classical Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46508-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T12:22:18Z","timestamp":1587817338000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}