{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:34:20Z","timestamp":1753889660892,"version":"3.41.2"},"reference-count":21,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,9,8]],"date-time":"2011-09-08T00:00:00Z","timestamp":1315440000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We provide a mathematical theory and methodology for synthesising equational\nlogics from algebraic metatheories. We illustrate our methodology by means of\ntwo applications: a rational reconstruction of Birkhoff's Equational Logic and\na new equational logic for reasoning about algebraic structure with\nname-binding operators.<\/jats:p>","DOI":"10.2168\/lmcs-7(3:12)2011","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T13:45:24Z","timestamp":1415972724000},"source":"Crossref","is-referenced-by-count":0,"title":["On the mathematical synthesis of equational logics"],"prefix":"10.46298","volume":"Volume 7, Issue 3","author":[{"given":"Marcelo","family":"Fiore","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2011,9,8]]},"reference":[{"key":"10.2168\/LMCS-7(3:12)2011_Birkhoff35","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100013463"},{"key":"10.2168\/LMCS-7(3:12)2011_Burroni","unstructured":"A. Burroni. Alg\u00e8bres graphiques (sur un concept de dimension dans les langages formels).Cahiers de topologie et g\u00e9om\u00e9trie diff\u00e9rentielle, XXII(3):249-265, 1981."},{"key":"10.2168\/LMCS-7(3:12)2011_CloustonPitts07","doi-asserted-by":"crossref","unstructured":"R. Clouston and A. Pitts. Nominal equational logic. In L. Cardelli, M. Fiore, and G. Winskel, editors,Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin, volume 172 ofElectronic Notes in Theoretical Computer Science, pages 223-257. Elsevier, 2007.","DOI":"10.1016\/j.entcs.2007.02.009"},{"key":"10.2168\/LMCS-7(3:12)2011_Ehresmann","unstructured":"C. Ehresmann. Esquisses et types des structures alg\u00e9briques.Bul. Inst. Polit. Iasi, XIV, 1968."},{"key":"10.2168\/LMCS-7(3:12)2011_FG07","doi-asserted-by":"crossref","unstructured":"M. Fern\u00e1ndez and M. J. Gabbay. Nominal rewriting.Information and Computation, 205 (6): 917-965, 2007.","DOI":"10.1016\/j.ic.2006.12.002"},{"key":"10.2168\/LMCS-7(3:12)2011_FGM04","doi-asserted-by":"crossref","unstructured":"M. Fern\u00e1ndez, M. J. Gabbay, and I. Mackie. Nominal rewriting systems. InProceedings of the Sixth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'04), pages 108-119. ACM, 2004.","DOI":"10.1145\/1013963.1013978"},{"key":"10.2168\/LMCS-7(3:12)2011_Fiore08","doi-asserted-by":"crossref","unstructured":"M. Fiore. Second-order and dependently-sorted abstract syntax. InProceedings of the Twenty-Third Annual Symposium on Logic in Computer Science (LICS'08), pages 57-68. IEEE Computer Society, 2008.","DOI":"10.1109\/LICS.2008.38"},{"key":"10.2168\/LMCS-7(3:12)2011_FioreHur08","doi-asserted-by":"crossref","unstructured":"M. Fiore and C.-K. Hur. Term equational systems and logics. InProceedings of the Twenty-Fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS'08), volume 218 ofElectronic Notes in Theoretical Computer Science, pages 171-192. Elsevier, 2008.","DOI":"10.1016\/j.entcs.2008.10.011"},{"key":"10.2168\/LMCS-7(3:12)2011_FioreHurSOEqLog","doi-asserted-by":"crossref","unstructured":"M. Fiore and C.-K. Hur. Second-Order Equational Logic. InProceedings of the 19th EACSL Annual Conference on Computer Science Logic (CSL 2010), volume 6247 ofLecture Notes in Computer Science, pages 320-335. Springer-Verlag, 2010.","DOI":"10.1007\/978-3-642-15205-4_26"},{"key":"10.2168\/LMCS-7(3:12)2011_FioreHurTCS","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.12.052"},{"key":"10.2168\/LMCS-7(3:12)2011_FioreMahmoud","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15155-2_33"},{"key":"10.2168\/LMCS-7(3:12)2011_GabbayMathijssen06","unstructured":"M. J. Gabbay and A. Mathijssen. Nominal algebra. InProceedings of the Eighteenth Nordic Workshop on Programming Theory (NWPT'06), 2006."},{"key":"10.2168\/LMCS-7(3:12)2011_GabbayMathijssen07","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73445-1_12"},{"key":"10.2168\/LMCS-7(3:12)2011_GabbayPitts01","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"10.2168\/LMCS-7(3:12)2011_Hamana03","doi-asserted-by":"crossref","unstructured":"M. Hamana. An initial algebra approach to term rewriting systems with variable binders.Higher-Order and Symbolic Computation, 19 (2-3): 231-262. Springer, 2006.","DOI":"10.1007\/s10990-006-8747-5"},{"key":"10.2168\/LMCS-7(3:12)2011_HurThesis","unstructured":"C.-K. Hur.Categorical Equational Systems: Algebraic Models and Equational Reasoning. PhD thesis, Computer Laboratory, University of Cambridge, 2010."},{"key":"10.2168\/LMCS-7(3:12)2011_KellyPower93","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(93)90092-8"},{"key":"10.2168\/LMCS-7(3:12)2011_Lawvere63","doi-asserted-by":"crossref","unstructured":"F. W. Lawvere.Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University, 1963.","DOI":"10.1073\/pnas.50.5.869"},{"key":"10.2168\/LMCS-7(3:12)2011_MacLaneMoerdijk92","doi-asserted-by":"crossref","unstructured":"S. Mac Lane and I. Moerdijk.Sheaves in Geometry and Logic. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0927-0"},{"key":"10.2168\/LMCS-7(3:12)2011_Power99","unstructured":"A. J. Power. Enriched Lawvere theories.Theory and Applications of Categories, 6: 83-93, 1999."},{"key":"10.2168\/LMCS-7(3:12)2011_Robinson02","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200014"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1071\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1071\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:02:53Z","timestamp":1681243373000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1071"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9,8]]},"references-count":21,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(3:12)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1107.3031","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1107.3031","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2011,9,8]]},"article-number":"1071"}}