On the mathematical synthesis of equational logics

Marcelo Fiore; Chung-Kil Hur

doi:10.2168/LMCS-7(3:12)2011

Marcelo Fiore ; Chung-Kil Hur - On the mathematical synthesis of equational logics

lmcs:1071 - Logical Methods in Computer Science, September 8, 2011, Volume 7, Issue 3 - https://doi.org/10.2168/LMCS-7(3:12)2011

On the mathematical synthesis of equational logicsArticle

Authors: Marcelo Fiore ; Chung-Kil Hur

We provide a mathematical theory and methodology for synthesising equational logics from algebraic metatheories. We illustrate our methodology by means of two applications: a rational reconstruction of Birkhoff's Equational Logic and a new equational logic for reasoning about algebraic structure with name-binding operators.

Comment: Final version for publication in Logical Methods in Computer Science

https://doi.org/10.2168/LMCS-7(3:12)2011

Source: arXiv.org:1107.3031

Volume: Volume 7, Issue 3

Secondary volumes: Selected Papers of the 9th Conference on Typed Lambda Calculi and Applications (TLCA 2009)

Published on: September 8, 2011

Imported on: May 15, 2010

Keywords: Computer Science - Logic in Computer Science, Mathematics - Category Theory, Mathematics - Logic, D.3.1, F.3.1, F.3.2, F.4.1, I.2.3

Licence: arXiv.org - Non-exclusive license to distribute