Date: Mon, 09 Oct 2006 11:56:44 -0500
From: Jared Davis
To: ACL2 MTG List

Hi,

At this week's ACL2 meeting, I'll give a demo of Isabelle.

Isabelle is a "generic" theorem prover since it can work with many different 
logics.  Of these logics, higher-order logic is the "best developed".  You may 
have seen this called Isabelle/HOL.

I'll attempt to present Isabelle/HOL from a user's perspective.  I'll show you 
its interface and walk through simple tasks like defining data types and 
functions, and proving basic theorems.  Then I'll show you a more substantial 
and more ACL2-like project, and highlight a few of the cool features of the 
system, along with a couple of gripes.  Finally, I'll try to give you an idea 
about what's involved in manually building proofs in ML, and how sophisticated 
users could extend Isabelle's automation with simplification procedures.

Thanks,
    Jared