7 hours ago
- Dracula 为ACL2语言和定理证明器提供了一个编程环境。
- 安装通过Racket的'raco pkg install dracula'命令完成。
- 使用Dracula时，在DrRacket的Dracula类别中选择ACL2，并使用定义和交互窗口。
- 通过点击开始按钮，然后使用接受/全部按钮来证明定理；接受的表达式变绿，拒绝的变红。
- 使用'raco pkg update dracula'或'raco pkg remove dracula'卸载或更新Dracula。
- 该项目已在东北大学一年级本科逻辑课程中使用。