Скачать 13.21 Кбайт
Обратный метод С.Ю. Маслова
Узлам дерева вывода соответствуют конечные множества чисел с индексами, "расщепляемым" по правилу ® & (для наглядности они помечены квадратными скобками). "Расщепляемым" дизъюнктам исходной формулы — числа без индексов в круглых скобках. В корне дерева записана пустое множество, рядом с которым в фигурных скобках записаны номера всех дизъюнктов исходной формулы:
Полученное после прополки дерево является примером дерева вывода Ф в исчислении благоприятных наборов.
Введем исчисление благоприятных наборов явным образом. Еще раз отметим, что такое исчисление строится для каждой формулы, выводимость которой необходимо установить, по приведенной общей схеме ОМ:
НАБОРОМ называется последовательность чисел с индексами, где графически равные члены сокращаются до одного и порядок записи чисел с индексами несущественен. Набор записывается в строчку без скобок.
НАБОРОМ С ЗАВИСИМОСТЬЮ называется набор, справа от которого в круглых скобках приписана некоторая последовательность чисел без индексов (в зависимости порядок записи числе также несущественен и графически равные члены сокращаются до одного).
ПРАВИЛО А (задает базис исчисления): если двухчленный набор с зависимостью содержит два числа с индексами, которые соответствуют контрарной паре литер, то такой набор с зависимостью называется исходным благоприятным набором. Зависимость исходных благоприятных наборов пустая (круглые скобки справа вообще не пишутся).
Примерами аксиом (по правилу А) формулы Ф являются двухчленные наборы в "прополотом дереве вывода", а также следующие наборы: 52 63, 32 42, 33 71, 62 71
ПРАВИЛО Б (единственное правило вывода данного исчисления, которое задает механизм образования новых благоприятных наборов): если наборы с зависимостями An ... B1 (X, …) ,..., Сm ... Вp (У, …) являются благоприятными наборами с зависимостями и B1, ..., Вp составляют полную совокупность литер некоторого дизъюнкта исходной формулы (дизъюнкта под номером B), то набор с зависимостью Аn … Сm … (Х, .., У, .., B) также является благоприятным (в зависимость этого набора добавляется номер B).
Тривиальным применением правила Б называется перенесение числа с индексом ноль в зависимость этого набора (уже без индекса).
Правило Б позволяет получать новые благоприятные наборы, из состава которых исключены те числа с индексами, которые образуют полную совокупность всех чисел с индексами некоторого числа без индекса.
Примерами "новых" благоприятных наборов полученных по правилу Б являются множества в квадратных скобках в "прополотом дереве вывода" (см. рис.3), а также следующие наборы: [33] — получен из исходного благоприятного набора 1033 тривиальным применением правила Б); [62] — получен из исходного благоприятного набора 1062 тривиальным применением правила Б); [21 63] — получен из исходных благоприятных наборов 21 51 и 63 52, так как 52 и 52 образуют дизъюнкт 5 формулы Ф; [22 42] — получен из благоприятных наборов 32 42, 22 31, [33], так как числа 31, 32 и 33 образуют полную совокупность литер третьего (3) дизъюнкта Ф.
ВЫВОДОМ называется линейная последовательность благоприятных наборов с зависимостями, последним членом которой является пустой (нольчленный) благоприятный набор (на рис.3 он обозначен знаком ).
Примером вывода исчисления благоприятных наборов является полученное по алгоритму прополки "прополотое дерево вывода" на рис.3.
Другим примером вывода является следующая линейная последовательность наборов с анализом. Под анализом будем понимать указание около каждого "нового" благоприятного набора его предшественников, т.е. номеров тех строчек, из которых получен данный набор.
1. 10 33 8. 22 61
2. [33] из 1 9. [22] из 5, 7, 8
3. 32 63 10. 21 51
4. 31 22 11. 42 52
5. [22 63] из 2, 3, 4 12. [21 42] из 10, 11
6. [10 62] 13. 21 41
7. [62] из 6 14. [21] из 12, 13
15. из 9, 14
Для того чтобы быть уверенным, что построенное исчисление благоприятных наборов является эквивалентным исходному секвенциальному исчислению сформулируем теорему о полноте:
Исходная формула Ф выводима тогда и только тогда, когда в исчислении благоприятных наборов получен вывод.
Доказательство этой теоремы в одну сторону практически было проведено, когда был сформулирован алгоритм прополки: из любого вывода в секвенциальном исчислении можно получить вывод исчисления благоприятных наборов.
В обратную сторону, теорема следует из того, что при наличии вывода в исчислении благоприятных наборов мы по крайней мере дважды должны применить правило Б для получения пустого благоприятного набора.
Полученное после прополки дерево является примером дерева вывода Ф в исчислении благоприятных наборов.
Введем исчисление благоприятных наборов явным образом. Еще раз отметим, что такое исчисление строится для каждой формулы, выводимость которой необходимо установить, по приведенной общей схеме ОМ:
НАБОРОМ называется последовательность чисел с индексами, где графически равные члены сокращаются до одного и порядок записи чисел с индексами несущественен. Набор записывается в строчку без скобок.
НАБОРОМ С ЗАВИСИМОСТЬЮ называется набор, справа от которого в круглых скобках приписана некоторая последовательность чисел без индексов (в зависимости порядок записи числе также несущественен и графически равные члены сокращаются до одного).
ПРАВИЛО А (задает базис исчисления): если двухчленный набор с зависимостью содержит два числа с индексами, которые соответствуют контрарной паре литер, то такой набор с зависимостью называется исходным благоприятным набором. Зависимость исходных благоприятных наборов пустая (круглые скобки справа вообще не пишутся).
Примерами аксиом (по правилу А) формулы Ф являются двухчленные наборы в "прополотом дереве вывода", а также следующие наборы: 52 63, 32 42, 33 71, 62 71
ПРАВИЛО Б (единственное правило вывода данного исчисления, которое задает механизм образования новых благоприятных наборов): если наборы с зависимостями An ... B1 (X, …) ,..., Сm ... Вp (У, …) являются благоприятными наборами с зависимостями и B1, ..., Вp составляют полную совокупность литер некоторого дизъюнкта исходной формулы (дизъюнкта под номером B), то набор с зависимостью Аn … Сm … (Х, .., У, .., B) также является благоприятным (в зависимость этого набора добавляется номер B).
Тривиальным применением правила Б называется перенесение числа с индексом ноль в зависимость этого набора (уже без индекса).
Правило Б позволяет получать новые благоприятные наборы, из состава которых исключены те числа с индексами, которые образуют полную совокупность всех чисел с индексами некоторого числа без индекса.
Примерами "новых" благоприятных наборов полученных по правилу Б являются множества в квадратных скобках в "прополотом дереве вывода" (см. рис.3), а также следующие наборы: [33] — получен из исходного благоприятного набора 1033 тривиальным применением правила Б); [62] — получен из исходного благоприятного набора 1062 тривиальным применением правила Б); [21 63] — получен из исходных благоприятных наборов 21 51 и 63 52, так как 52 и 52 образуют дизъюнкт 5 формулы Ф; [22 42] — получен из благоприятных наборов 32 42, 22 31, [33], так как числа 31, 32 и 33 образуют полную совокупность литер третьего (3) дизъюнкта Ф.
ВЫВОДОМ называется линейная последовательность благоприятных наборов с зависимостями, последним членом которой является пустой (нольчленный) благоприятный набор (на рис.3 он обозначен знаком ).
Примером вывода исчисления благоприятных наборов является полученное по алгоритму прополки "прополотое дерево вывода" на рис.3.
Другим примером вывода является следующая линейная последовательность наборов с анализом. Под анализом будем понимать указание около каждого "нового" благоприятного набора его предшественников, т.е. номеров тех строчек, из которых получен данный набор.
1. 10 33 8. 22 61
2. [33] из 1 9. [22] из 5, 7, 8
3. 32 63 10. 21 51
4. 31 22 11. 42 52
5. [22 63] из 2, 3, 4 12. [21 42] из 10, 11
6. [10 62] 13. 21 41
7. [62] из 6 14. [21] из 12, 13
15. из 9, 14
Для того чтобы быть уверенным, что построенное исчисление благоприятных наборов является эквивалентным исходному секвенциальному исчислению сформулируем теорему о полноте:
Исходная формула Ф выводима тогда и только тогда, когда в исчислении благоприятных наборов получен вывод.
Доказательство этой теоремы в одну сторону практически было проведено, когда был сформулирован алгоритм прополки: из любого вывода в секвенциальном исчислении можно получить вывод исчисления благоприятных наборов.
В обратную сторону, теорема следует из того, что при наличии вывода в исчислении благоприятных наборов мы по крайней мере дважды должны применить правило Б для получения пустого благоприятного набора.
|
|