|
A Computational Logic |
| 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 |