命题定理证明

Question

我们如何使用广度优先搜索作为命题定理证明的策略（我看不到一个明确的问题表述：每个状态下可用的操作是什么以及状态是什么）。

我一直在网上到处寻找解释；所有文档都提到了 BFS，但都没有给出算法。

感谢您的帮助

Answer 1

状态是派生的列表。从状态到状态的转换应用推理规则，其中每个前提作为推导列表中的结论出现，并使用新推导扩展列表。

通过这些状态和转换，您可以执行通常的 BFS，直到您找到所需的结论。