欢迎来到不可思议的证明机！这是什么？这是一个可视化地在各种逻辑中进行证明的工具（例如：命题逻辑、谓词逻辑）：您只需添加表示各种证明步骤的块，正确连接它们，如果结论变为绿色，则您已创建一个完整的证明！只需拖放即可连接两个点；有关完成证明的示例，请参见此论文。要快速了解用户界面，请查看Tea Leaves Programming频道上的介绍视频（13分钟）！ 为什么会出现这个？不可思议的证明机是为了传达进行证明的乐趣和喜悦，尤其是在计算机辅助的情况下，而无须首先学习像Isabelle这样的“真正”的定理证明器的语法。 我可以使用哪些键盘快捷键？ CTRL+Z: 撤消更改 CTRL+Y: 重做更改 CTRL+A: 选择所有块 BACKSPACE, DELETE: 删除选定的块 SHIFT+MOUSE1: 将块或区域添加到选择中 为什么结论没有变为绿色？因为您的证明还不是证明。这可能有以下原因：您的一些块具有未连接到任何事物的输入（假设）。这些是红色的。您的一些连接连接了明显不同的命题（标记为红色并标记有☠），或者它们未被充分指定，并且不清楚它们是否可能不同（标记为红色并带有？）。在后一种情况下，插入注释块（✎P）可能会有所帮助。您在证明中有循环。这些（您猜对了）标记为红色。您错误地连接了局部假设。局部假设是那些在块的凹陷左侧输出的内容，可以仅在连接到相应输入的证明部分中使用，该输入在凹陷右侧。 我需要提到这些是标记为红色的吗？我如何输入这些有趣的字符？实际上，您只有少数地方需要输入公式，主要是如果您想使用✎P块或定义您自己的任务。在那里，您可以使用以下缩写：可以用& | -> ^ ~ ! ? False代替∧ ∨ → ↑ ¬ ∀ ∃ ⊥。 我如何创建具有多个假设或结论的自定义任务？只需将每个假设和结论单独放在一行，即在每个假设或结论后按一下Enter键。 我如何创建自定义块？您可以通过点击块同时按住Shift选择证明中的块。然后，创建一个包装您选择的块的自定义块的选项将出现。 我的证明去哪了？目前，您的证明将仅保存在您自己的浏览器中。这意味着当您关闭此窗口/选项卡后删除本地存储时，或如果这是私人浏览会话或类似情况时，它们将会丢失。我们计划在未来的版本中将您的进度保存在我们的服务器上。 谁做的？主要是Joachim Breitner，得到了其他一些同事和朋友的宝贵帮助。 我可以在哪里阅读更多信息？有关不可思议的证明机的更多信息，特别是从学术角度出发，请参阅以下出版物： Joachim Breitner: 与不可思议的证明机的可视化定理证明，ITP 2016上接收的论文，2016年8月； Joachim Breitner: 不可思议的证明机，LFMTP 2016上的邀请讲座，2016年6月； Joachim Breitner, Denis Lohner: 不可思议的证明机的元理论，Archive of Formal Proofs中的Isabelle形式化，2016年5月； 不可思议的证明机，Joachim Breitner接受Sebastian Ritterbusch采访，科学播客“Modellansatz”的第78集，德语，2016年。 我可以帮助吗？当然可以！一切都是自由软件，因此您可以直接参与，获取代码并开始贡献。贡献的人越多，不可思议的证明机就变得越不可思议。