Skip to main content
PRL Project

Nuprl as Logical Framework for Automating Proofs in Category

by Christoph Kreitz

Published in Logic and Program Semantics:
Essays Dedicated to Dexter Kozen on the Occasion of his 60th Birthday

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

cite link