haskell - 自动演绎/自动定理证明的项目想法？

Question

我是第二学期的大三学生，很快就会开始我的论文，我对自动演绎和自动定理证明器很感兴趣。就像在，我想以某种方式推进艺术(我不是装腔作势，但我确实想做一些富有成效的事情)。我在谷歌上搜索的范围很广，到目前为止，几乎没有出现过有希望的想法。有一些学生项目的想法页面，但大多数看起来要么非常过时，要么过于先进(我原本打算尝试综合后现代主义思想(哈哈哈)并抽象其逻辑内容，构建一个完整且一致的模型(当然，如果可能的话) )，并尝试使其自动化，尽可能将所述模型以非标准逻辑 a la these 为基础。我的顾问认为这给了后现代主义思想太多的信任(不久前我用 Parsec 在 Haskell 中重新实现了 the Postmodernism Generator，所以这部分是想法来自)；我很想同意。)

是的。有没有人有想法？如果我在这里的方法有一些明显的差距/如果我没有适本地完成我的作业(如果有的话，请告诉我!)，我很抱歉，但在很大程度上我什至不知道从哪里开始，并且感谢您阅读所有这些内容。

Answer 1

事先承认我对这个领域不是特别了解，我一直对“不可靠”的证明助手软件的效用(和存在)感到好奇——因为没有更好的术语——“不可靠”的证明助手软件，特别是应用于一般而言，难以处理或无法解决的问题。基于启发式或统计分析的系统，可以进行“猜测”并在尝试使事情或沿着这些路线进行的事情上跌跌撞撞。当然，我们的想法是将那些不适合基于详尽搜索或严格演绎的更有条理的技术解决的问题，可能是作为交互式证明助手的一个组成部分的零碎部分。

另一方面，我不知道已经在多大程度上探索了沿着这些方向的想法，而且我不确定它是否是一种可行的技术(如果其他人确实知道更多，我会感兴趣听到它)。