1

快速复审：

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

问题：
给定一个输入目标（例如A AND B,C），假设我们首先在 上应用规则 AND A AND B，然后得到两个新的子目标，第一个是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 *)
4

1 回答 1

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的编码方式。在实践中，将有许多选项可用，您可能希望遍历它们。

于 2014-08-30T12:52:55.090 回答