***** KAIST Discete Math Semianr *****
DATE: August 11, Monday
TIME: 4PM-5PM
PLACE: E6-1, ROOM 1409
SPEAKER: Chung-Kil Hur (허충길), University of Cambridge, UK
TITLE: Term Equational Systems and Logics
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 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 synthesise 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.
----------------------------------------------
Informations on future talks can be found at :
http://mathsci.kaist.ac.kr/~sangil/seminar/
Please email to sangil (at) kaist.edu if you wish to receive this
announcements in the future by email.