ACL2 Sedan

The ACL2 Sedan theorem prover (ACL2s) is an Eclipse plug-in that provides a modern IDE, supports several modes of interaction, provides a powerful termination analysis engine, includes a rich support for "types" and seamlessly integrates semi-automated bug-finding methods with interactive theorem proving.

Application domain/field

Theorem proving

Type of tool

Theorem prover

Expected input

Format:

ACL2s/Lisp file

Internals

Uses ACL2

Comments

ACL2s has been developed because ACL2 had a steep learning curve. The idea being that ACL2s should be easier to use for new users.