Roy McCasland
Automated Theorem Discovery
ACL2 Seminar, March 24, 2010

Abstract:

I will talk about and demo an automated system for not only generating
and proving, but also *identifying* mathematical Theorems.  By
"Theorems", I mean those results that are deemed by mathematicians as
being worthy of recording -- i.e., the Theorems, Corollaries, Lemmas,
etc., that one might find in a mathematics textbook.