ACL2 Seminar 10/18/06

Matt Kaufmann

TITLE:

Some Logical Foundations of ACL2 with a Focus on
Conservativity of the Defchoose Event

ABSTRACT:

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.