Доказательство корректности этой леммы можно получить из допустимости правила исключения однолитерных дизъюнктов в секвенциальном исчислении.

Для минимизации числа "новых" благоприятных наборов, полученных по правилу Б можно предложить следующую лемму, которую можно назвать леммой о нормализации вывода:

ЛЕММА 3
При наличии среди уже имеющихся благоприятных наборов такого благоприятного набора, который является подмножеством некоторого вновь полученного благоприятного набора, использование этого нового благоприятного набора для получения вывода избыточно.

Данная лемма определяет целый класс эффективных стратегий построения выводов, так как сильно ограничивает число (вид) благоприятных наборов, участвующих в выводе: из процесса построения исключаются все наднаборы некоторого набора. На основании этого возможна не только нормализация вывода, но и дальнейшая модификация исходной "заготовки" исчисления следующим образом: "искусственное" введение в процесс построения выводов некоторых наборов — допущений, которые, например, одночленны (заметим, что этот подход близок идеологии систем натурального вывода, в которых использование допущений является существенной чертой при построении выводов). Тогда на основании лемм 1 и 2 возможно существенное сокращение исходных благоприятных наборов. Использование при построении выводов одночленных наборов — допущений связано с моделированием метода расщеплений. При моделировании правила расщеплений в секвенциальных исчислениях его можно трактовать как последовательное добавление к исходной формуле новых однолитерных дизъюнктов, полученных в результате "расщепления" некоторых дизъюнктов исходной формулы. Это является эквивалентным преобразованием формулы. За счет действия правила исключения однолитерных дизъюнктов количество дизъюнктов сокращается и вывод строится быстрее. В обратном методе возможно моделирование не только правила расщепления по некоторому дизъюнкту, но и моделирование нового правила расщепления по некоторому исходному благоприятному набору (см. правило Б). Технически это осуществлено в моей работе [14] (см. вставку (=ДОПОЛНЕНИЕ=) из этой работы ниже; ).

— данный текст дополнен фрагментом из работы: Катречко С.Л. Моделирование правила расщеплений в обратном методе С.Ю.Маслова //Логические методы в компьютерных науках. М., ИФ РАН, 1991). Здесь нам потребуется понятие набора с зависимостью, которое мы ввели ранее.



ДОПОЛНЕНИЕ ===== ** вставка из работы [14]

Моделирование правила расщепления в обратном методе



Использование при построении выводов одночленных наборов — допущений связано с моделированием метода расщеплений. При моделировании правила расщеплений в секвенциальных исчислениях его можно трактовать как последовательное добавление к исходной формуле новых однолитерных дизъюнктов, полученных в результате "расщепления" некоторых дизъюнктов исходной формулы. После этого исходная секвенция ® Ф разбивается на две (® Ф1 и ® Ф2), в которых исходная формула Ф упрощается (до Ф1 и Ф2, соответственно) за счет применения правила исключения однолитерных дизъюнктов (см. выше лемму 2). Это является эквивалентным преобразованием формулы.

Классическое правило расщепления (1) в секвенциальном исчислении выглядит так:

® Ф1 (C) ® Ф2 (~C)

® Ф, C ® Ф, ~C

® Ф, C & ~C

® Ф

Здесь Ф1 (Ф2) — результат применения леммы 2 к формуле Ф Ъ C (Ф Ъ ~C).

Отметим при этом, что в секвенциальном исчислении правило расщепления структурно (как и ранее — правило Б ОМ) соответствует контрприменению правила сечения, или является аналогом контрприменения правила резолюции.

Такое представление правила расщепления позволяет предложить еще одно допустимое — за счет идеологии правила Б обратного метода — правило вывода, в котором происходит «расщепление» не по противоречивому дизъюнкту C & ~C как в оригинальном правиле расщепления, а по некоторому дизъюнкту исходной формулы Ф (допустимость этого правила основана на том, что приписывание к исходной формуле Ф любого числа ее дизъюнктов — это сделано на втором уровне секвенциального дерева (см. ниже)— является эквивалентном преобразованием формулы). Правило расщепления (2) по некоторому дизъюнкту формулы Ф выглядит так:

® Ф1 (C) ® Ф2 (B)

® Ф, C ® Ф, B

® Ф, C & B

® Ф

Установив сходство правила расщепления и правила Б мы можем промоделировать правило расщепления (1) и (2) за счет «расширения» сферы действия тривиального применения правила Б обратного метода (вернее, тривиального применения правила Б* с учетом моделирования правила резолюций). Назовем его правилом Б**:

ТРИВИАЛЬНЫМ ПРИМЕНЕНИЕМ ПРАВИЛО Б* назовем такое его применение к некоторому благоприятному набору с зависимостью, в результате которого некоторое число с индексом (на обязательно с индексом ноль как в исходном тривиальном правиле Б — см.