3 hours ago
- 「不可思议的证明机」是一款可视化工具，通过拖拽连接积木块完成命题逻辑、谓词逻辑等逻辑系统的证明。
- 用户添加代表证明步骤的积木块；若结论变为绿色，则表示已构建完整证明。
- 该工具旨在传递计算机辅助证明的乐趣，无需预先了解Isabelle等定理证明器的语法知识。
- 公式输入仅限特定积木块（如¬-块），需使用缩写：&代表∧，|代表∨，->代表→，^代表↑，~代表¬，!代表∀，?代表∃，False代表⊥。
- 当前证明仅保存在浏览器本地存储中，可能丢失；未来计划支持服务器端保存。
- 该工具为自由软件，欢迎贡献；学术细节请参阅相关出版物。