Title:

Term Equational Systems and Logics

Abstract:

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.