computer-science - Fitch Format Proofs - 周围有自动求解器吗？

Question

Closed. This question does not meet Stack Overflow guidelines 。它目前不接受答案。












想改善这个问题吗？更新问题，使其成为 Stack Overflow 的 on-topic。

6年前关闭。



Improve this question




是否有任何软件使用 Fitch 格式(在 Language, Proof and Logic 中使用)，允许人们放置一组特定的前提和目标，并向我们展示解决问题所需的完整步骤列表？

最佳答案

简短的回答:没有。

中等答案:虽然可以很容易地编写一个程序来检查给定证明的有效性，但实际上并不能做到。在命题逻辑的情况下，自动找到证明的问题是 NP 完全的(尽管它是可判定的!)，并且在一阶逻辑中存在证明者永远不会停止的真定理。 (不可判定)(通过哥德尔的不完备性证明)

如果你对写这样的东西感兴趣，你可以尝试一下，也许让它在一些较小的情况下工作，但一般来说这是不可行的。

如果您正在寻找这样的东西来获得家庭作业的答案，请停止尝试。 (a) 你不会找到它和 (b) 那本书中的问题很简单，而且很有趣!尝试一下，并在需要时寻求帮助。而且，当然，(c) 如果你作弊，你将不会学到任何东西。

关于computer-science - Fitch Format Proofs - 周围有自动求解器吗？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/3138918/

上一篇：sql - 是否可以使用 SQL 更新 CLOB 内的数据？

下一篇：crc - 如何确定使用哪个 CRC？

相关文章：

logic - 如何将 Coq 设置为一阶逻辑的定理证明器

mysql - 从表中获取符合条件的多条记录

java - 选择的 boolean 值问题

mysql - 如何从列的逗号分隔值中找到子部分并插入mysql中的新行？

types - 类型为 Mercury 等逻辑编程语言带来什么好处？

algorithm - 如何设计/词动态规划子问题？

c - 这个链表程序中每一行的作用是什么？

prolog - 一阶逻辑 Prolog 匿名变量

computer-science - 开发人员要点 - 资源和项目尝试

nlp - 将句子转换为一阶逻辑

Answer 1

简短的回答:没有。

中等答案:虽然可以很容易地编写一个程序来检查给定证明的有效性，但实际上并不能做到。在命题逻辑的情况下，自动找到证明的问题是 NP 完全的(尽管它是可判定的!)，并且在一阶逻辑中存在证明者永远不会停止的真定理。 (不可判定)(通过哥德尔的不完备性证明)

如果你对写这样的东西感兴趣，你可以尝试一下，也许让它在一些较小的情况下工作，但一般来说这是不可行的。

如果您正在寻找这样的东西来获得家庭作业的答案，请停止尝试。 (a) 你不会找到它和 (b) 那本书中的问题很简单，而且很有趣!尝试一下，并在需要时寻求帮助。而且，当然，(c) 如果你作弊，你将不会学到任何东西。