1

簡単なレビュー：

  • 推論規則＝結論＋規則＋前提
  • 証明木 = 結論 + ルール + サブツリー
  • 後方証明検索: 入力ゴールが与えられた場合、ボトムアップ方式で推論ルールを適用して証明ツリーを構築しようとします (たとえば、ゴールは最終的な結論であり、ルールを適用した後、新しいサブゴールのリストが生成されます)敷地内）

問題:
入力目標 (例: A AND B,C) が与えられた場合、最初に に AND ルールを適用すると、A AND B2 つの新しいサブ目標が得られます。最初の目標はA,Cで、2 番目の目標は ですB,C。
問題は、AとBが役に立たないことです。つまり、 のみを使用して完全な証明木を構築できCます。ただし、サブゴールが 2 つあり、C2 回証明する必要があるため、非常に非効率的です。

質問:
たとえば、 があり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自然に再帰的であるため2番目の回答を参照してください。

これらの提案は、適用するルールをどのように選択するかという主題には触れません。つまり、正確get_ruleにコード化する方法です。実際には、多くのオプションが利用可能であり、それらを反復したいと思うでしょう。

于 2014-08-30T12:52:55.090 に答える