Title: 

Term Equational Systems and Logics

Abstract:

Equational reasoning is fundamental in automated theorem proving
(that is, the proving of mathematical theorems by a compuer program),
and rewriting is a powerful method for equational reasoning.
Category theory is a mathemtical theory that deals in an abstract way
with mathematical structures and relationships between them.

Using category theory, we have developed a framework for equational reasoning.
A Term Equational System (TES) is given by a semantic universe and
an abstract notion of syntax; and given this, we automatically derive 
a sound logical deduction system, called Term Equational Logic (TEL).
Furthermore, we provide an algebraic free construction for the system,
which may be used to synthesise a sound and complete rewriting system for it.

Existing systems arising in this framework include:

   - first-order equational logic and rewriting system;
   - nominal equational logics independently developed
     by Gabbay and Matheijssen, and Clouston and Pitts;
   - binding equational logic and rewriting system of Hamana;
   - combinatory reduction system of Klop.

Especially, following the above scenario in our framework,
we have newly developed a sound and complete rewriting system 
for nominal equational logic.

In this talk, rather than going into the technical details,
I will focus on explaining basic ideas of category theory
and how it can be used in practice.

This is joint work with Marcelo Fiore.