dev*_*ium 5 logic computer-science fitch-proofs first-order-logic
有没有使用Fitch格式(用于语言,证明和逻辑)的软件,允许人们放置一组特定的前提和目标,并让它向我们展示解决问题所需的完整步骤列表？
简答:不.
中等答案:无法真正完成,尽管可以编写一个程序来相当容易地检查给定证明的有效性.在命题逻辑的情况下,自动查找证明的问题是NP完全的(尽管它是可判定的!),并且在一阶逻辑中存在证明永远不会停止的真正定理.(不可判定的)(通过哥德尔的不完整性证明)
如果你有兴趣写这样的东西,你可以试一试,也许可以让它适用于一些较小的情况,但一般来说这是不可行的.
如果你正在寻找这样的东西来获得你的家庭作业的答案,退出尝试.(a)你不会发现它和(b)那本书中的问题很简单,而且很有趣!试试看吧,如有需要,请寻求帮助.当然,(c)如果你作弊,你将不会学到任何东西.