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 270904b9443d8c2843cfd5c7cb7c86025f8e29c0 by David Wheeler on Tuesday August 29, 2017.