logic - Propositional Theorem Proving

Question

How can we use Breadth First Search as a strategy for propositional theorem proving (I can't see a clear problem formulation: what are the actions available at each state and what a state is).

I've been looking for explanations everywhere in the net; all documents mention BFS but none of them gives an algorithm.

Thank you for your help

Answer 1

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

使用这些状态和转换，您可以执行通常的 BFS，直到您找到您正在寻找的结论。