My Ph.D. thesis involved the construction of a formal verification system for general mathematicsl proofs which I named Ontic. My thesis was published as a 1989 MIT press book Ontic: a Knowledge representation System for Mathematics. This system underwent considerable development by myself and my student Robert Givan through 1995. It was eventually implemented with an inference rule compiler --- a compiler for dymaic programming algorithms expressed as bottom-up logic programs. These implementation tools were similar to, but predated, Jason Eisner's Dyna language. Robert Givan, now a professor at Purdue, maintains a version of the Ontic verifications system.