Chung-Kil Hur (허충길), Term Equational Systems and Logics

Term Equational Systems and Logics
Chung-Kil Hur (허충길)
Computer Laboratory, University of Cambridge, Cambridge, UK.
2008/08/11 Mon, 4PM-5PM

Equational reasoning is fundamental in automated theorem proving (that is, the proving of mathematical theorems by a computer program), and rewriting is a powerful method for equational reasoning. Category theory is a mathematical 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 synthesize a sound and complete rewriting system for it.

Existing systems arising in this framework include:

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


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.


Comments are closed.