The Proof Machine (2016)

# The Incredible Proof Machine 来源：https://incredible.pm/ ## 欢迎来到 The Incredible Proof Machine！ ### 这是什么？ 这是一个可视化完成各种逻辑（例如命题逻辑、谓词逻辑）证明的工具：你只需添加代表不同证明步骤的积木块，正确连接它们，如果结论变为绿色，就说明你创建了一个完整的证明！只需拖放即可连接两个点；如需查看一些完整证明的示例，请参阅这篇论文（https://www.joachim-breitner.de/publications/Incredible_ITP2016_preprint.pdf）。 如果想要快速了解用户界面，可以查看 Tea Leaves Programming 频道上的介绍视频（13分钟）（https://www.youtube.com/watch?v=bExGUtVWzb4）！ ### 为什么有这个工具？ The Incredible Proof Machine 的创建是为了传递做证明的乐趣，尤其是在计算机辅助下，无需先学习像Isabelle（http://isabelle.in.tum.de/）这样“真正”定理证明器的语法。 ### 可以使用哪些快捷键？ - CTRL+Z：撤销更改 - CTRL+Y：重做更改 - CTRL+A：选择所有积木块 - BACKSPACE、DELETE：删除选中的积木块 - SHIFT+鼠标左键：将积木块或区域添加到选择 ### 为什么结论不是绿色？ 因为你的证明（暂时）还不是一个正确的证明。可能的原因如下： - 某些积木块的输入（假设）没有连接到任何东西。这些输入会显示为红色。 - 某些连接连接了明显不同的命题（标记为红色并带有☠），或者它们未充分指定，无法确定它们是否不同（标记为红色并带有?）。在后一种情况下，插入一个注释积木块（✎P）可能会有所帮助。 - 证明中存在循环。这些循环（你猜对了）会标记为红色。 - 本地假设的连接方式错误。本地假设是指积木块左侧凹口处输出的那些内容，它们只能在连接到该凹口右侧对应输入的证明部分中使用。需要我说这些也标记为红色吗？ ### 如何输入那些有趣的字符？ 实际需要输入公式的地方很少，主要是当你使用 ✎P 积木块或定义自己的任务时。在那里，你可以使用以下缩写： 将 ∧ ∨ → ↑ ¬ ∀ ∃ ⊥ 替换为 & | -> ^ ~ ! ? False ### 如何创建一个包含多个假设或结论的自定义任务？ 只需将每个假设和结论放在单独的行上，即每个后面按回车。 ### 如何创建自定义积木块？ 你可以按住 Shift 键点击选择证明中的积木块。然后，就会出现创建一个包含你所选积木块的自定义积木块的选项。 ### 我的证明去哪儿了？ 目前，你的证明只会保存在你自己的浏览器中。这意味着当你关闭此窗口/标签页后删除本地存储，或者如果这是隐私浏览会话等情况下，它们会丢失。我们计划在未来的版本中将你的进度保存到我们的服务器上。 ### 这是谁做的？ 主要是Joachim Breitner（http://www.joachim-breitner.de/），并得到了一些同事和朋友的宝贵帮助（https://github.com/nomeata/incredible/graphs/contributors）。 ### 我在哪里可以了解更多？ 关于 Incredible Proof Machine 的更多信息，尤其是从学术角度，请参阅以下出版物： - Joachim Breitner：**Visual theorem proving with the Incredible Proof Machine**（https://www.joachim-breitner.de/publications/Incredible_ITP2016_preprint.pdf），ITP 2016（http://itp2016.inria.fr/）录用论文，2016年8月 - Joachim Breitner：**The Incredible Proof Machine**（https://www.joachim-breitner.de/publications/Incredible_LFMTP_2016-06-23.pdf），LFMTP 2016（http://dlicata.web.wesleyan.edu/events/lfmtp2016/program.html）特邀报告，2016年6月 - Joachim Breitner, Denis Lohner：**The meta theory of the Incredible Proof Machine**（http://isa-afp.org/entries/Incredible_Proof_Machine.shtml），Archive of Formal Proofs 中的 Isabelle 形式化，2016年5月 - **Incredible Proof Machine**（http://modellansatz.de/incredible-proof-machine），Joachim Breitner 接受 Sebastian Ritterbusch 采访，科学播客“Modellansatz”第78期，德语，2016年 ### 我可以提供帮助吗？ 当然可以！一切都是自由软件，所以你可以直接开始，获取代码（https://github.com/nomeata/incredible）并开始贡献。贡献的人越多，The Incredible Proof Machine 就会变得越不可思议。