{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T15:32:15Z","timestamp":1720625535653},"reference-count":37,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2001,6,1]],"date-time":"2001-06-01T00:00:00Z","timestamp":991353600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T00:00:00Z","timestamp":1416441600000},"content-version":"vor","delay-in-days":4920,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2001,6]]},"DOI":"10.1016\/s1571-0661(04)00147-1","type":"journal-article","created":{"date-parts":[[2004,2,5]],"date-time":"2004-02-05T10:34:35Z","timestamp":1075977275000},"page":"1-28","source":"Crossref","is-referenced-by-count":7,"special_numbering":"C","title":["Layered map reasoning"],"prefix":"10.1016","volume":"48","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"}]},{"given":"Marco","family":"Temperini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB1","unstructured":"Aureli F., A. Formisano, E. G. Omodeo and M. Temperini, Map calculus: Initial application scenarios and experiments based on Otter, Technical Report 466, IASI-CNR (1998)."},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB2","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/BF00881874","article-title":"Z-match: An Inference Rule for Incrementally Elaborating Set Instantiations","volume":"11","author":"Bailin","year":"1993","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB3","first-page":"10","article-title":"On a modification of G\u00f6del's algorithm for class formation","volume":"34","author":"Belinfante","year":"1996","journal-title":"AAR Newsletter"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB4","series-title":"Models and Ultraproducts: An Introduction (third revised printing)","author":"Bell","year":"1974"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB5","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF02328452","article-title":"Set theory in first-order logic: Clauses for G\u00f6del's axioms","volume":"2","author":"Boyer","year":"1986","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB6","unstructured":"D. Cantone, A. Cavarra and E. G. Omodeo, On existentially quantified conjunctions of atomic formulae of L+, in: M. P. Bonacina and U. Furbach, editors, Proceedings of the FTP97 International workshop on first-order theorem proving, 1997, pp. 45\u201352, RISC-Linz Report Series No. 97-50."},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB7","series-title":"\u201cComputable Set Theory Vol. 1\u201d","author":"Cantone","year":"1989"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB8","unstructured":"Cantone D., A. Formisano, E. G. Omodeo and C. G. Zarba, Compiling dyadic first-order specifications into map algebra, in: Proceedings, of the 16th Twente Workshop on Language Technology\u20142nd AMAST Workshop Algebraic Methods in Language Processing (AMILP 2000) TWLT 16, University of Twente, 2000, pp. 35\u201354."},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB9","doi-asserted-by":"crossref","unstructured":"Cantone D., E. G. Omodeo and A. Policriti, \u201cSet Theory for Computing \u2014 From decision procedures to declarative programming with sets,\u201d Springer-Verlag, 2001, Texts and Monographs in Computer Science.","DOI":"10.1007\/978-1-4757-3452-2"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB10","unstructured":"Chiacchiaretta A., A. Formisano and E. G. Omodeo, Benchmark #1 for equational set theory, in: Giomata \u201cAnalisi Sperimentale di Algoritmi per l'Intelligenza Artificiale\u201d, Roma, 1999. URL http:\/\/www.dis.uniroma1.it\/~rcra\/roma99."},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB11","unstructured":"Chiacchiaretta A., A. Formisano and E. G. Omodeo, Map reasoning through existential multigraphs, Technical Report 05\/00, Dipartimento di Matematica Pura ed Applicata, Universit\u00e0 di L'Aquila (2000)."},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB12","first-page":"341","article-title":"Distributive and modular laws in relation algebras","volume":"1","author":"Chin","year":"1951","journal-title":"University of California Publications in Mathematics"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB13","series-title":"\u201cSet Theory and the Continuum Hypothesis\u201d","author":"Cohen","year":"1966"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB14","doi-asserted-by":"crossref","DOI":"10.3233\/FI-1994-2143","article-title":"Rough relation algebras","volume":"21","author":"D\u00fcntsch","year":"1994","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB15","series-title":"Automated Deduction in Classical and Non-Classical Logics, LNCS 1761 (LNAI)","first-page":"175","article-title":"An equational re-engineering of set theories","author":"Formisano","year":"2000"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB16","unstructured":"Formisano A. and E. G. Omodeo, Equational set-reasoning by automated map calculus, Technical Report 16\/00, Dipartimento di Matematica Pura ed Applicata, Universit\u00e0 di L'Aquila (2000)."},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB17","doi-asserted-by":"crossref","DOI":"10.1006\/jsco.1999.0362","article-title":"Goals and benchmarks for automated map reasoning","volume":"29","author":"Formisano","year":"2000","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB18","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1093\/jigpal\/5.3.1","article-title":"A finite axiomatization for fork algebras","volume":"5","author":"Frias","year":"1997","journal-title":"Journal of the IGPL"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB19","series-title":"Formal Methods in Programming and Their Applications, LNCS 735","first-page":"281","article-title":"On the smooth calculation of relational recursive expressions out of first-order non-constructive specifications involving quantifiers","author":"Haeberer","year":"1993"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB20","first-page":"80","article-title":"Representation problems for relation algebras","volume":"54","author":"J\u00f3nsson","year":"1948","journal-title":"Bull. Amer. Math. Soc"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB21","unstructured":"Kwatinetz, M. K., \u201cProblems of expressibility in finite languages,\u201d Ph.D. thesis, University of California, Berkeley (1981)."},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB22","doi-asserted-by":"crossref","first-page":"707","DOI":"10.2307\/1969375","article-title":"The representation of relational algebras","volume":"51","author":"Lyndon","year":"1950","journal-title":"Ann. of Math., Ser 2"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB23","series-title":"\u201cOTTER 3.0 Reference Manual and Guide\u201d","author":"McCune","year":"1994"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB24","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/BF00881863","article-title":"Experimenting with Isabelle in ZF set theory","volume":"10","author":"No\u00ebl","year":"1993","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB25","doi-asserted-by":"crossref","first-page":"1123","DOI":"10.1002\/cpa.3160480908","article-title":"Solvable set\/hyperset contexts: I. Some decision procedures for the pure, finite case","volume":"48","author":"Omodeo","year":"1995","journal-title":"Comm. Pure App. Math"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB26","series-title":"Philosophical Logic in Polland","first-page":"167","article-title":"Relational semantics for nonclassical logics: Formulas are relations","author":"Orlowska","year":"1994"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB27","doi-asserted-by":"crossref","first-page":"1230","DOI":"10.2307\/2275470","article-title":"Expressing Infinity without Foundation","volume":"56","author":"Parlamento","year":"1991","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB28","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00881873","article-title":"Set Theory for Verification: I. From Foundations to Functions","volume":"11","author":"Paulson","year":"1993","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB29","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF00881916","article-title":"Set Theory for Verification. II: Induction and Recursion","volume":"15","author":"Paulson","year":"1995","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB30","series-title":"\u201dAutomates development of fundamental mathematical theories\u201d","author":"Quaife","year":"1992"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB31","series-title":"Set theory and its logic","author":"Quine","year":"1971"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB32","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0012-365X(85)90064-0","article-title":"Relation algebras: Concept of points and representability","volume":"54","author":"Schmidt","year":"1985","journal-title":"Discrete Mathematics"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB33","doi-asserted-by":"crossref","first-page":"45","DOI":"10.4064\/fm-6-1-45-95","article-title":"Sur les ensembles fini","volume":"VI","author":"Tarski","year":"1924","journal-title":"Fundamenta Mathematicae"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB34","doi-asserted-by":"crossref","unstructured":"Tarski A. and S. Givant, \u201cA formalization of Set Theory without variables,\u201d Colloquium Publications 41, American Mathematical Society, 1987.","DOI":"10.1090\/coll\/041"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB35","series-title":"\u201cAutomated Reasoning. 33 basic research problems\u201d","author":"Wos","year":"1988"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB36","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/BF00245023","article-title":"The problem of finding an inference rule for set theory","volume":"5","author":"Wos","year":"1989","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)00147-1_NEWBIB37","series-title":"From Frege to G\u00f6del - A source book in Mathematical Logic, 1879-1931","first-page":"199","article-title":"Untersuchungen \u00fcber die Grundlagen der Mengenlehre I","author":"Zermelo","year":"1977"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001471?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001471?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,30]],"date-time":"2020-03-30T12:30:41Z","timestamp":1585571441000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104001471"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,6]]},"references-count":37,"alternative-id":["S1571066104001471"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00147-1","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,6]]}}}