7 hours ago
- Dracula provides a programming environment for the ACL2 language and theorem prover.
- Installation is done via Racket's 'raco pkg install dracula' command.
- To use Dracula, select ACL2 in the Dracula category in DrRacket and use the Definitions and Interactions windows.
- Theorems are proved by clicking Start, then using Admit/All buttons; accepted expressions turn green, rejected ones red.
- Uninstall or update Dracula using 'raco pkg update dracula' or 'raco pkg remove dracula'.
- The project has been used in a first-year undergraduate logic course at Northeastern University.