Equational Logics

d Abstract) Marcelo Fiore1 Chung-Kil Hur2,3 Computer Laboratory University of Cambridge Cambridge, UK We introduce an abstract general notion of system of equations between terms, called Term Equational System, and develop a sound logical deduction system, called Term Equational Logic, for equational reasoning. Further, we give an analysis of algebraic free constructions that together with an internal completeness result may be used to synthesise complete equational logics. Indeed, as an application, we synthesise a sound and complete nominal equational logic, called Synthetic Nominal Equational Logic, based on the category of Nominal Sets.

• Type: Conference
• Year: 1991
• Where: SAS
• Authors: Yong Sun
• Keywords: Equational Logic, Formal Methods, Nominal Equational Logic, SAS 1991, Term Equational Logic