正如标题中所写，我的问题是关于创建一个程序的可能性，该程序在给定假设和论文的情况下，尝试以某种方式演示该定理并在可证明的情况下打印给用户。
问问题
82 次
1 回答
3
一般来说，这取决于您考虑的理论。例如，如果您考虑 FOL（一阶逻辑），那么这个问题被认为是无法解决的（Entscheidungsproblem），而如果您考虑命题逻辑，那么答案是肯定的（因为它是可判定的）。有关可判定性的更多信息，请参见： https ://en.wikipedia.org/wiki/Decidability_(logic)#Some_decidable_theories
于 2017-04-03T18:17:50.900 回答