Since Automath, proof assistants such as HOL, Nuprl and Isabelle have brought formalization to substantial parts of mathematics in areas such as logic, set theory, and analysis. However, the popular use of informal diagrammatic methods in more `geometric' areas makes formalization difficult. In this talk (and with respect to a few specific examples) I'll make this problem precise and attempt to persuade the listener that "higher-dimensional equational logic" provides an appropriate language for the formaliztion of (at least some) geometric ideas. This language will turn out to be a conservative extension of rewriting logic and therefore realizable in systems such as CafeOBJ and Maude.
| Duraid Madina |
| Master Student, UNSW |
| Date: | Thu Jan 27 2005 |
| Time: | 1 to 2pm |
| Location: | Level 1 Seminar Room, CSE Bldg (K17), UNSW |
Last updated by tbourke at Thu Jan 20 16:59:53 2005 GMT+1100