ACL2 Seminar 10/18/06
Some Logical Foundations of ACL2 with a Focus on
Conservativity of the Defchoose Event
This talk will discuss some of the logical foundations of ACL2, in
particular for the defchoose event. The goal is to give a sense of
the foundational issues for correctness of ACL2 and, in particular, of
a so-called "forcing" argument for the admissibility of defchoose
events. In order to fit the talk into about 70 minutes, it will avoid
some technical details, instead pointing to additional reading for
those interested in such details. The intention is to provide enough
baCkground and motivation so that those interested in such details
will find that reading to be accessible.
IMPORTANT NOTE ON PREREQUISITES:
I will start with a very brief, very fast review of first-order logic
so that we are all on the same page. Those who have not seen
first-order logic may wish to contact me for a primer before the talk,
or at least read Section 1 of the notes,
"Review of first-order logic".
The rest of the talk is intended to be self-contained. But if you
first take a look at :doc
defchoose, that might help in absorbing the talk in real time.