Date: Mon, 29 Nov 2004 22:49:14 -0600 (CST)
From: "Jared C. Davis"
Subject: ACL2 Meeting Wednesday


Hi,

Our weekly ACL2 meetings will be starting again this week.  John Erickson
will be talking about improving the automation of induction by considering
example cases.  He writes:

"I will present a technique for automatically proving inductive
theorems.  The inspiration for this technique is that humans often
test a theorem with some small examples to get an idea of why it is
true before attempting to prove it.  The technique takes proofs for
finite cases of a given theorem and then generalizes these proofs to
generate a proof for the general case.  This proof is mechanically
checked using the ACL2 theorem prover.  My results show that this
technique can automatically prove many interesting theorems that
otherwise would have required human guidance."

Hope to see you there,

   Jared