On the mathematical synthesis of equational logics
arXiv:1107.3031 · doi:10.2168/LMCS-7(3:12)2011
Abstract
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.
Final version for publication in Logical Methods in Computer Science