Abstract, 10/23/03.

At the next ACL2 seminar, Matt Kaufmann will discuss the ACL2 logic as it
fits into the framework of first-order logic.  The notions of "conservative
extension" and "soundness" will be defined carefully, and will both be shown
to be critical for ACL2, and it will be argued informally that these
properties are satisfied by the ACL2 logic.  Matt will discuss the notion of
an ACL2 model, along with the potential existence of so-called "bad" objects
permitted by the "open universe" logic (and type system) of ACL2.  He might
also touch on the notion of "non-standard" numbers and how an ACL2 universe
could contain them.

Seminar attendees are invited, even begged, to ask questions during the talk
(even seemingly very basic ones) about ACL2 logical issues.