{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T01:38:17Z","timestamp":1648863497445},"reference-count":42,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3742,"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":[[2003,5]]},"DOI":"10.1016\/s1571-0661(04)80936-8","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"153-174","source":"Crossref","is-referenced-by-count":1,"title":["A graphical approach to relational reasoning1 1This research was partially funded by the Italian CNR (coordinated project log(SETA)); by MURST PGR-2000; by the EC TMR Network GETGRATS; and by Esprit Working Group APPLIGRAPH."],"prefix":"10.1016","volume":"44","author":[{"given":"Andrea.","family":"Formisano","sequence":"first","affiliation":[]},{"given":"Eugenio G.","family":"Omodeo","sequence":"additional","affiliation":[]},{"given":"Marta","family":"Simeoni","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB1","unstructured":"Behnke R., R. Berghammer and P. Schneider, Machine support of relational computations: The Kiel RELVIEW system, Tech. Rep. Bericht Nr. 9711, Institut f\u00fcr Informatik und Praktische Mathematik, Christian-Albrechts-Universit\u00e4t Kiel, Kiel, Germany (1997)."},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB2","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1023\/A:1006050629424","article-title":"Computer proofs in G\u00f6del's class theory with equational definitions for composite and cross","volume":"22","author":"Belinfante","year":"1999","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB3","doi-asserted-by":"crossref","unstructured":"Brown C. and G. Hutton, Categories, allegories and circuit design, in: Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, Paris, France, 1994, pp. 372\u2013381.","DOI":"10.1109\/LICS.1994.316052"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB4","first-page":"56","article-title":"Allegories of circuits","author":"Brown","year":"1994","journal-title":"Proc. Logic For Computer Science"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB5","unstructured":"Cantone D., 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\u201350."},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB6","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\u2013-2nd AMAST Workshop Algebraic Methods in Language Processing (AMILP 2000), TWLT 16, University of Twente, 2000."},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB7","unstructured":"Chiacchiaretta A., A. Formisano and E. G. Omodeo, Benchmark #1 for equational set theory, in: Giornata \u201cAnalisi Sperimentale di Algoritmi per l'Intelligenza Artificiale\u201d, Roma, 1999."},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB8","unstructured":"Chiacchiaretta A., A. Formisano and E. G. Omodeo, Map reasoning through existential multigraphs, Tech. Rep. 05\/00, Dipartimento di Matematica Pura ed Applicata, Universit\u00e0 di L'Aquila (2000)."},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB9","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)80936-8_NEWBIB10","doi-asserted-by":"crossref","unstructured":"Corradini A., U. Montanari, F. Rossi, H. Ehrig, R. Heckel, and M. L\u00f6we, Algebraic approaches to graph transformation I: Basic concepts and double pushout approach, in: Rozenberg [37] pp. 163\u2013246.","DOI":"10.1142\/9789812384720_0003"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB11","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/0167-6423(95)00025-9","article-title":"Proofs with graphs","volume":"26","author":"Curtis","year":"1996","journal-title":"Science of Computer Programming"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB12","doi-asserted-by":"crossref","unstructured":"Dougherty D. and C. Guti\u00e9rrez, Normal forms and reduction for theories of binary relations, in: L. Bachmair, editor, Rewriting Techniques and Applications, 11th International Conference, RTA2000, Norwich, UK, July 2000, Proc., LNCS 1833 (2000), pp. 95\u2013109.","DOI":"10.1007\/10721975_7"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB13","unstructured":"B. Dwyer, LIBRA: a Lazy Interpreter of Binary Relational Algebra, Tech. Rep. 95-10, Department of Computer Science University of Adelaide, 1995."},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB14","doi-asserted-by":"crossref","unstructured":"Ehrig H., R. Heckel, M. Korff, M. L\u00f6we, L. Ribeiro, A. Wagner and A. Corradini, Algebraic approaches to graph transformation II: Single pushout approach and comparison with double pushout approach, in: Rozenberg [37] pp. 247\u2013312.","DOI":"10.1142\/9789812384720_0004"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB15","series-title":"\u201cA Mathematical Introduction to Logic\u201d","author":"Enderton","year":"1972"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB16","series-title":"Handbook of Graph Grammars and Computing by Graph Transformation, vol. 2: Applications, Languages and Tools","article-title":"The Agg approach: Language and environment","author":"Ermel","year":"1999"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB17","series-title":"Automated Deduction in Classical and Non-Classical Logics 175\u2013190","article-title":"An equational re-engineering of set theories","author":"Formisano","year":"2000"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB18","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)80936-8_NEWBIB19","unstructured":"Formisano, A. and M. Simeoni, Graphs and maps: rewriting techniques at work, Tech. Rep. TU-Berlin 2001-01, Technische Universit\u00e4t Berlin, (2001)"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB20","series-title":"\u201cLogic machines and diagrams\u201d","author":"Gardner","year":"1982"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB21","first-page":"189","article-title":"Tarski's Development of Logic and Mathematics based on the Calculus of Relations","volume":"vol. 54","author":"Givant","year":"1991"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB22","series-title":"\u201cThe Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory\u201d","author":"G\u00f6del","year":"1940"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB23","unstructured":"Guti\u00e9rrez C., \u201cThe arithmetic and geometry of allegories,\u201d Ph.D. thesis, Wesleyan University, Middletown, CT (1999)."},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB24","series-title":"Stanford Encyclopedia of Philosophy","article-title":"Peirce's Logic","author":"Hammer","year":"1999"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB25","series-title":"AMAST '93","first-page":"405","article-title":"RALF - A relation-algebraic formula manipulation system and proof checker. Notes to a system demonstration","author":"Hattensperger","year":"1994"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB26","series-title":"\u201cStudies in the Logic of Charles Sanders Peirce,\u201d","year":"1997"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB27","series-title":"\u201cLectures in abstract algebra: I. basic concepts\u201d","author":"Jacobson","year":"1951"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB28","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BF02483728","article-title":"Varieties of relation algebras","volume":"15","author":"J\u00f3nsson","year":"1982","journal-title":"Algebra Universalis"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB29","series-title":"Graph Theoretic Concepts in Computer Science, WG '96","first-page":"224","article-title":"Algebraic graph derivations for graphical calculi","author":"Kahl","year":"1997"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB30","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/S0020-0255(99)00018-3","article-title":"Relational matching for graphical calculi of relations","volume":"119","author":"Kahl","year":"1999","journal-title":"Information Sciences"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB31","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","article-title":"Depth-first iterative-deepening: An optimal admissible tree search","volume":"27","author":"Korf","year":"1985","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB32","series-title":"\u201cIntroduction to axiomatic set theory\u201d","author":"Krivine","year":"1971"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB33","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)80936-8_NEWBIB34","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0304-3975(93)90068-5","article-title":"Algebraic approach to single-pushout graph transformation","volume":"109","author":"L\u00f6we","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB35","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1007\/BF00370681","article-title":"The origin of relation algebras in the development and axiomatization of the calculus of relations","volume":"50","author":"Maddux","year":"1991","journal-title":"Studia Logica"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(95)00082-8","article-title":"Relation-algebraic semantics","volume":"160","author":"Maddux","year":"1996","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB37","series-title":"\u201cHandbook of Graph Grammars and Computing by Graph Transformation, vol. I: Foundations,\u201d","year":"1997"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB38","doi-asserted-by":"crossref","unstructured":"Schmidt G. and T. Str\u00f6hlein, \u201cRelations and graphs,\u201d Monographs on Theoretical Computer Science, Springer-Verlag, Berlin, 1993.","DOI":"10.1007\/978-3-642-77968-8"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB39","unstructured":"Schr\u00f6der E., \u201cVorlesungen \u00fcber die Algebra der Logik (exakte Logik), vol.1\u20133\u201d B. Teubner, Leipzig, 1891\u201395, [Reprinted by Chelsea Publishing Co., New York, 1966.]."},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB40","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0743-1066(84)90023-2","article-title":"Negation as failure: A comparison of Clark's completed data base and Reiter's closed world assumption","volume":"1","author":"Shepherdson","year":"1984","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/S1571-0661(04)80936-8_NEWBIB41","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)80936-8_NEWBIB42","unstructured":"Ullman, J. D., \u201cDatabase and Knowledge-base Systems, vol.1,\u201d Principles of Computer Science 49, Computer Science Press, Stanford University, 1988."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104809368?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104809368?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:10:47Z","timestamp":1585897847000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104809368"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S1571066104809368"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80936-8","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}