Modular proof development in ACL2
The ACL2 theorem prover combines a first-order dialect of LISP with an automated proof engine for first-order logic. While ACL2 is logically quite powerful, it can be difficult to build and maintain large models due to its ad hoc systems for modularity, namespace management, logical encapsulation, a...
| Published: |
|
|---|---|
| Online Access: | http://hdl.handle.net/2047/d20002853 |