Доказательство теорем: как оптимизировать обратный поиск доказательства, содержащий бесполезное правило И

Быстрый просмотр:

  • Правило вывода = заключение + правило + посылки
  • Дерево доказательств = заключение + правило + поддеревья
  • Обратный поиск доказательств: с учетом входной цели попробуйте построить дерево доказательств, применяя правила вывода снизу вверх (например, цель - это окончательный вывод, после применения правила будет сгенерирован список новых подцелей. на территории)

Проблема:
Учитывая входную цель (например, A AND B,C), предположим, что мы применяем правило И сначала к 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 *)

functional-programming theorem-proving ocaml proof proof-system
person Hoang-Mai Dinh    schedule 29.08.2014    source источник
comment
Вы имеете в виду, как мы можем найти самое короткое (самое неглубокое) дерево доказательств или как избежать повторного выполнения одного и того же доказательства для подцели, которая дважды появлялась при поиске доказательства?   -  person Nikos    schedule 30.08.2014

Ответы (1)


arrow_upward
1
arrow_downward

Если вам нужно кратчайшее (самое поверхностное) доказательство, которое в данном случае использует введение дизъюнкции и избегает введения конъюнкции, вы можете изучить такие методы, как итеративное углубление. Например, вы можете изменить свой код следующим образом:

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. На практике будет доступно множество опций, и вы захотите перебрать их.

person Nikos    schedule 30.08.2014