Matt Kaufmann
ACL2 Seminar, April 5, 2019

Title:
ACL2: Implementation of a Computational Logic

Abstract:

[This is a dry run of a talk that I will be giving to mathematical
logicians in late May.  I'll try to adapt it to the audience attending
the ACL2 seminar.]

ACL2 ("A Computational Logic for Applicative Common Lisp") is a
programming language, a first-order logic, and a software system for
proving theorems in that logic.  In this talk I will provide a sense
of what ACL2 is, what can be done with it, and especially what sorts
of logical issues can arise when attempting to build a powerful yet
sound mechanized reasoning system.