Date: Mon, 7 Apr 2003 13:29:53 -0500
From: John Erickson
Subject: This Week in ACL2


Hello, this week I'll be talking about the project I've been working
on for a semester or so now.  Below is a brief description of the
project.  

We present a technique for automatically generating proofs based on
generalizing finite cases.  The proofs are mechanically verified
using the ACL2 theorem prover.  We demonstrate a theorem that would
have required human intervention in ACL2 and show how our technique
automatically proves it.

Typically, when a human sits down to prove a theorem about an
infinite structure, he plays with some small examples in his head to
understand the problem.  Most theorem provers do not.  They
typically lunge headlong into the proof, attempting to guess an
appropriate induction hypothesis by examining the definitions
involved and then rewriting the theorem in the same way as any
other.  Our goal in this project was to allow the theorem prover to
exploit examples in the same way that humans do.

John