В данном случае "сфера действия" правила Б ограничивается.

Отметим, что данные подходы противоречат друг другу, но лишь отчасти.

МОДИФИКАЦИИ ОБЩЕЙ СХЕМЫ ОБРАТНОГО МЕТОДА.
МОДЕЛИРОВАНИЕ ПРАВИЛА РЕЗОЛЮЦИЙ



Как было отмечено выше, исчисления благоприятных наборов являются удобным базисом для моделирования различных правил вывода и эвристик, соответствующим разным методам автоматического теорем. Как известно из литературы [12], важным средством повышения мощности (эффективности) систем поиска вывода является моделирование в них правила сечения. Для сформулированного выше секвенциального исчисления правило сечения является допустимым. Сравним правило сечения с правилом Б исчисления благоприятных наборов. Для этого запишем их следующим образом:

правило вывода Б исчисления правило сечения

® A, X ® B, Y ® A, C ® B, ~C

® A, B, X & Y ® A, B, C & ~C

® A, B (F) ® A, B

Здесь X & Y можно исключить правилу Здесь C & ~C можно исключить по правилу

вывода исчисления, при условии, что сечения, так как C & ~C — противоречие и его

X & Y образуют формулы Ф. удаление не нарушает выводимости ® A, B

Как видно из приведенного рисунка "механизм работы" этих двух правил аналогичен, т.е. налицо структурное сходство. Правило Б можно понимать как аналог правила сечения, который при своем применении сверху вниз, также как и правило сечения позволяет исключать некоторые литеры, которые встречались в верхней части правил. Если правило сечения исключает те литеры, которые образуют контрарные пары, то правило Б — литеры, которые образуют некоторый дизъюнкт исходной формулы Ф. И в том, и в другом случае преобразования сохраняют эквивалентность формул.

Для моделирования правила сечения можно предложить следующую модификацию правила Б:

ПРАВИЛО Б*: При образовании благоприятных наборов разрешено выбрасывать не только те числа с индексами, которые составляют полную совокупность по некоторому числу, но и те числа с индексами, которые образуют один из исходных благоприятных наборов.

"Сфера действия" двухпосылочного правила Б расширяется: теперь при "склеивании" благоприятных наборов разрешается выбрасывать контрарные пары литер. Такая модификация правила Б и соответствует моделированию правила сечения относительно формулы Ф, поскольку применение правила Б по некоторому исходному благоприятному набору и соответствует выбрасыванию из состава формулы контрарных пар литер. При этом, возможности исходного исчисления расширяются. Теперь эти исчисления можно использовать для установления ложности формул: если при построении вывода применять правило Б только по исходным благоприятным наборам, то получение пустого благоприятного набора позволяет сделать вывод о том, что в составе исходной формулы Ф содержатся только противоречивые дизъюнкты и, следовательно, формула Ф тождественно — ложна. Для сохранения теоремы о полноте исчисления необходимо потребовать хотя бы однократного применения правила Б в старой формулировке (применение правила Б по некоторому числу). Более строгое доказательство такой модификации дано в [13].

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

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

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

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

В нашем примере, без потери выводимости можно исключить следующие исходные благоприятные наборы 33 71 и 62 71

На основании леммы 1 возможно "подключить" к предложенной выше схеме исчисления следующую модификацию:

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

Формулировка