定理证明：如何优化包含"useless rule AND"的向后证明搜索

Question

快速回顾：

• 推理规则=结论+规则+前提
• 证明树=结论+规则+子树
• 反向证明搜索：给定一个输入目标，尝试通过自下而上的方式应用推理规则来构建证明树（例如，目标是最终结论，应用规则后，它会在前提上生成一个新的子目标列表）

问题：
给定一个输入目标（例如A AND B,C），假设我们首先在A AND B上应用规则AND，然后得到两个新的子目标，第一个是A,C，第二个是B,C
问题是A和B是无用的，这意味着我们可以只使用C来构建一个完整的证明树。然而，我们有两个子目标，然后我们必须证明C两次，所以它确实是低效的。

问题：
例如，我们有A AND B,C AND D,E AND F,G,H AND I。在这种情况下，我们只需要D和G来构建一个完整的证明树。那么，如何选择正确的规则来应用呢？

这是Ocaml:中的一个示例代码

(* conclusion -> tree *)
let rec prove goal =                                          (* the function builds a proof tree from an input goal *)
  let rule      = get_rule goal in                            (* get the first rule *)
  let sub-goals = apply_rule goal in                          (* apply a rule *)
  let sub-trees = List.map (fun g -> prove g) sub-goals in    (* prove sub-goals recursively *)
  (goal, rule, sub-trees)                                     (* return proof tree *)

Answer 1

如果你想要最短（最浅）的证明，在这种情况下使用析取引入并避免连词引入，那么你可以考虑迭代深化等技术。例如，您可以按如下方式更改代码：

let rec prove n goal =
  if n=0 then failwith "No proof found" else
  let rule      = get_rule goal in
  let sub-goals = apply_rule goal in
  let sub-trees = List.map (fun g -> prove (n-1) g) sub-goals in
  (goal, rule, sub-trees)
let idfs maxn goal =
  let rec aux n =
    if n > maxn then None else
    try 
      Some (prove n goal)
    with Failure _ -> aux (n+1) in
  aux 1

如果你想避免为已经出现的子目标重新做证明，那么你可以使用某种形式的记忆（实际上是一种狭义的引理推测/应用）。例如，请参阅这个问题的答案，尤其是第二个答案，因为prove是自然递归的。

这些建议没有涉及如何选择要应用的规则，也就是get_rule的编码方式。在实践中，将有许多选项可用，并且您希望对它们进行迭代。