A Computational Logic
for Applicative Common Lisp


Software Name ACL2
Summary ACL2 is a programming language and logic in which you can model computer systems as well as a tool to help you prove properties of those models.

The ACL2 logic is a first-order, quantifier-free logic of recursive functions providing mathematical induction on the ordinals up to epsilon0 and two extension principles: one for recursive definition and one for constrained introduction of new function symbols, here called encapsulation.

Point of Contact: J Stother Moore
Department of Computer Science
University of Texas
Austin, TX 78712

Technology
Description
Educational
Description : NA
Platform(s) Architecture
compliance
Supporting software
dependencies
Availability Support User
Experiences

This page is URL http://www.computationallogic.com/software/caeti/acl2/acl2.html