Formalizations with ACL2 and ACL2(r)

One of my research goals is the formalization of interesting (to me) theorems from mathematics and computer science. Currently, I am working on a formalization of approximation algorithms to the Set Cover problem. The following table lists some of the formalizations that I, or one of my collaborators, have done in the past.

Project Author(s) Availability
Irrationality of Square Root R. Gamboa ACL2 Books
Exponential Function R. Gamboa ACL2 Books
Trigonometric Functions R. Gamboa ACL2 Books
Fast Fourier Transform R. Gamboa ACL2 Books
Intermediate Value Theorem R. Gamboa ACL2 Books
Maximum and Minimum Theorems R. Gamboa ACL2 Books
Mean Value Theorem R. Gamboa ACL2 Books
Automatic Differentiator P. Reid
R. Gamboa
ACL2 Books
Fundamental Theorem of Calculus M. Kaufmann ACL2 Books
Taylor’s Theorem R. Gamboa
B. Middleton
Inverse Functions R. Gamboa
J. Cowles
ACL2 Books
Unique Factorization in Euclidean Domains J. Cowles
R. Gamboa
ACL2 Books
Correctness of Hardware Implementation of SQRT J. Sawada
R. Gamboa
Correctness of a Kalman Filter Implementation R. Gamboa
J. Cowles
J. Van Baalen
Cook-Levin Theorem R. Gamboa
J. Cowles
Existence of Non-Measurable Sets J. Cowles
R. Gamboa
ACL2 Books
Existence of Transcendental Numbers R. Gamboa
J. Cowles
ACL2 Books
Powerlist Data Structure R. Gamboa ACL2 Books
Red-Black Trees R. Gamboa DrACuLa Distribution
Quantum Circuits L. Helms
R. Gamboa
ACL2 Books
Medina’s Approximation to Arctangent R. Gamboa
J. Cowles
ACL2 Books
Equivalence of Traditional and Non-Standard Approach to Calculus J. Cowles
R. Gamboa
ACL2 Books
Sierpinski and Riesel Numbers J. Cowles
R. Gamboa
ACL2 Books
Vickrey’s Theorem R. Gamboa
J. Cowles
ACL2 Books

Leave a Reply