Theorem Prover：如何优化包含“无用规则 AND”的后向证明搜索答案

【问题标题】：Theorem Prover: How to optimize a backward proof search containing a "useless rule AND"Theorem Prover：如何优化包含“无用规则 AND”的后向证明搜索
【发布时间】：2023-09-05 11:58:01
【问题描述】：

快速回顾：

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

问题：
给定一个输入目标（例如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 *)

【问题讨论】：

您的意思是我们如何找到最短（最浅）的证明树，或者您如何避免对在证明搜索中出现两次的子目标重新进行相同的证明？

标签： functional-programming ocaml proof theorem-proving proof-system

【解决方案1】：

如果您想要最短（最浅）的证明，在这种情况下使用析取引入并避免合取引入，那么您可以查看iterative deepening 之类的技术。例如，您可以按如下方式更改代码：

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

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

这些建议不涉及您如何选择应用规则的主题，即get_rule 的编码方式。在实践中，许多选项都可用，您可能希望遍历它们。

【讨论】：