Logic with a black tie and tails

I've had lots of fun with formal logic and theorem provers. This is a partial list of what I have done.


Just after graduate school, when I was working at the University of Kansas, I discovered PVS, a formal verification system. PVS lets you write a formal specification of a system, then prove theorems about that system. After learning my way around the system, I made a number of contributions, including:


My use of PVS petered out around 2007. Fast forward to 2016. After reading an article about metamath, I decided to give it a try. It's fun! I've been formalizing the material in N. J. Cutland's book, Computability: An introduction to recursive function theory. I've gotten through Definition 2.3 on page 27, in chapter 2. If you would like to see it, look here. This is based on the develop branch of the set.mm git repository, on top of commit 861bee2e48966dfaf0d0b8da6ffdac850001927d by Norm Megill on Saturday February 4, 2017.