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.