Nuprl as Logical Framework for Automating Proofs in Category
by Christoph Kreitz
We describe the construction of a semi-automated proof system for elementary category theory using the Nuprl proof development system as logical framework. We have used Nuprl’s display mechanism to implement the basic vocabulary and Nuprl’s rule compiler to implemented a first-order proof calculus for reasoning about categories, functors and natural transformations. To automate proofs we have formalized both standard techniques from automated theorem proving and reasoning patterns that are specific to category theory and used Nuprl’s tactic mechanism for the actual implementation. We illustrate our approach by automating proofs of natural isomorphisms between categories.
bibTex ref: Kre12