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 <a href = https://scholar.google.com/citations?view_op=view_citation&hl=en&user=nbpafUkAAAAJ&cstart=140&sortby=pubdate&citation_for_view=nbpafUkAAAAJ:KlAtU1dfN6UC> Ontic: a Knowledge representation System for Mathematics</a>.  This system underwent considerable development by myself and my student Robert Givan through 1995.
It was eventually implemented with an inference rule compiler --- <a href = https://scholar.google.com/citations?view_op=view_citation&hl=en&user=nbpafUkAAAAJ&cstart=40&sortby=pubdate&citation_for_view=nbpafUkAAAAJ:_kc_bZDykSQC> a compiler for dymaic programming algorithms</a> expressed as bottom-up logic programs. These implementation tools were similar to, but predated, <a href = http://www.dyna.org/> Jason Eisner's Dyna language</a>. <a href = https://engineering.purdue.edu/~givan/> Robert Givan</a>, now a professor at Purdue,  maintains a version of the Ontic verifications system.