Date: Tue, 13 Jul 2004 11:11:47 -0500 (CDT)
From: "Jared C. Davis"
Subject: ACL2 Meeting Update: Meeting Next Week


Hi,

There will now be a great ACL2 meeting on July 21 (one week from
tomorrow), at the usual time and place.

Ruben Gamboa will be in town, and he has agreed to speak about ACL2(r).
He writes:

"ACL2(r): The Story.

ACL2(r) is a variant of ACL2 that has support for the real and complex
irrational numbers.  It is based on the foundation of non-standard
analysis, also known as infinitesimal calculus.  Non-standard analysis
is an intuitive (but sometimes tricky) formalism for calculus, but to
those who are familiar with real analysis, as in Dedekind, Cauchy,
Weirestrass, and family, non-standard analysis seems a little strange.
We'll begin this talk by giving a very, very quick overview of
non-standard analysis, especially in the axiomatic formulation
developed by Nelson.  Then we'll give a brief overview of the features
of ACL2(r) that support non-standard analysis.  The bulk of the talk
will be devoted to the correctness of ACL2(r).  Following the lead of
Matt and J's "Structured Theory" paper, we present a "story" of ACL2(r)
that explains why ACL2(r) is sound.  That is, we will show that every
theorem of ACL2(r) is first-order derivable from the built-in theory of
ACL2(r) and its extension by definitions."

Hope to see you there,

    Jared