Automating Proofs in Category Theory


Dexter Kozen, Christoph Kreitz, Eva Richter.  
International Conference IJCAR 2006, LNAI 4130, pp. 392407, Springer Verlag, 2006. 

Abstract 

We introduce a semiautomated proof system for basic
categorytheoretic reasoning. It is based on a firstorder sequent
calculus that captures the basic properties of categories, functors
and natural transformations as well as a small set of proof tactics
that automate proof search in this calculus. We demonstrate our
approach by automating the proof that the functor categories
Fun[CxD,E] and Fun[C,Fun[D,E]] are naturally isomorphic.

(Preprint) 
Back to overview of papers 

Bibtex Entry 

@InProceedings{inp:KozenKreitzRichter06a, author = "Dexter Kozen and Christoph Kreitz and Eva Richter", title = "Automating Proofs in Category Theory", booktitle = "IJCAR 2006", year = "2006", editor = "U. Furbach and N. Shankar", volume = "4130", series = "Lecture Notes in Artificial Intelligence", pages = "392407", publisher = "Springer Verlag" } 