Using LEGO to formalise proof-theoretic symmetry arguments

James Molony

I have implementated some work in LEGO that has helped me to formulate symmetry and other arguments as correspondences between proof search spaces viewed as kripke structures. Modal mu-calculus provides a suitable language for describing a range of properties that are preserved within search spaces by various transformations and quotient operations. I have implemented the all various structures and logics in LEGO and will motivate and discuss the derived theorems using a simple object-level proof system (also in LEGO) as an example.

Healfdene Goguen

Last modified: Mon Jul 14 16:24:00 BST 1997