Title:

Term equational rewrite systems and logics.

Abstract:

We introduce an abstract general notion of system of equations
and rewrites between terms, called Term Equational Rewrite
System (TERS), and develop a sound logical deduction system,
called Term Equational Rewrite Logic (TERL), to reason about
equality and rewriting.  Existing systems arising as TERSs 
and TERLs include:

   - algebraic theories and equational logic;
   - the nominal equational logics independently developed
     by Gabbay and Matheijssen, and Clouston and Pitts;
   - first-order term rewriting systems;
   - the binding term rewriting system of Hamana;
   - the nominal rewrite system of Fernandez, Gabbay, and
     Mackie; and
   - the combinatory reduction system of Klop.

We also give an analysis of algebraic free constructions that 
together with an internal completeness result may be used to 
synthetise a complete TERL.  Indeed, as an application, we 
derive a sound and complete equational logic based on Nominal 
Sets that turns out to be equivalent to Nominal Equational 
Logic.  

This is joint work with Marcelo Fiore.