выше) исключается из состава набора и переносится в его зависимость.

Для сохранения теоремы о полноте сформулируем следующую лемму:

ЛЕММА 4
Любой вывод с применением правила Б** соответствует выводу такой секвенции Ф*, которая получена добавлением к формуле Ф некоторых ее литер, соответствующих числам с индексами в зависимости пустого благоприятного набора.

Для более строгого обоснования допустимости применения расширенного правила Б** построим метаисчисление благоприятных наборов — исчисление зависимостей.

Объектами этого метаисчисления будут выступать пустые благоприятные наборы с зависимостями — т.е. выводы — исходного исчисления благоприятных наборов, которые будем обозначать набором чисел в круглых скобках, например: (А, …, В, С). Назовем такие объекты зависимостями.

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

ПРАВИЛО В (правило вывода метаисчисления, которое задает механизм образования новых благоприятных зависимостей): если зависимости (An ... H1), (Bp ... H2), .., (Сm ... Hp) являются благоприятными зависимостями и H1, ..., Hp составляют совокупность литер, которая либо содержит контрарную пару литер (исходное правило (1) расщепления), либо графически равна некоторому дизъюнкту исходной формуле (правило (2) расщепления), то зависимость (Аn , … Bp , …, Сm) также является благоприятной зависимостью.

ВЫВОДОМ называется линейная последовательность благоприятных зависимостей, последним членом которой является пустая благоприятная зависимость ( ) — зависимость без чисел с индексами (это — как видно — соответствует выводу в исходном исчислении благоприятных наборов; см. доказательство теоремы о полноте ниже).

ТЕОРЕМА О ПОЛНОТЕ
Любой вывод исчисления зависимостей (с учетом использования правила Б**) может быть перестроен в вывод секвенциального исчисления с правилом расщепления (правилами (1) и (2) расщепления) и наоборот.

Доказательство теоремы основано на лемме 4. Дадим здесь идею доказательства. Исходные зависимости (как это задано в правиле С метаисчисления) соответствуют выводам формул Ф* в секвенциальном исчислении, которые возможно получены из Ф приписыванием дополнительных однолитерных дизъюнктов из числа литер формулы, а применение правила В — допустимому правилу расщепления. Если получена пустая благоприятная зависимость, т.е. зависимость, содержащая в своем составе только числа без индекса, то получен вывод либо самой формулы Ф, либо более сильной формулы без некоторых дизъюнктов формулы Ф. Обратный переход секвенциальных выводов основан на алгоритме прополке (см. теорему о полноте исчисления благоприятных наборов) и структурному сходству правила Б** правилу расщепления, которое допустимо в секвенциальном исчислении.

Приведем два примера выводам в метаисчислении, которые соответствуют различным стратегиям правила расщепления — правилу (1) и правилу (2) расщепления. Т.е. в первом случае происходит расщепление исходного благоприятного набора, или расщепление по контрарной паре литер, а во втором — расщепление по дизъюнкту 2 исходной формулы Ф.

Пример 1

1. 31 (22) 1. 22 (31)

2. 33 (1) 2. 21 51

3. 32 63 3. 51 (2, 31)

4. 63 (22 ,1, 3) 4. 42 52

5. 61 (22) 5. 42 (2, 31, 5)

6. 62 (10) 6. 21 41

7.  (22 ,1, 3, 6) 7. 21 (2, 31, 5, 4)

8.  (2, 31, 5, 4)

========================================

16. (--) (1, 2, 3, 4, 5, 6)



Пример 2

1. 31 (22) 1. 41 (21)

2. 33 (1) 2. 51 (21)

3. 32 63 3. 42 52

4. 63 (22 ,1, 3) 4. 42 (21, 5)

5. 61 (22) 5.  (21, 5, 4)

6. 62 (10)

7.  (22 ,1, 3, 6)

========================================

13. (--) (1, 2, 3, 4, 5, 6)



ЛИТЕРАТУРА:

1. Воронков А.А., Дегтярев А.Н. Автоматическое доказательство теорем //Кибернетика, 1986 No 3, 1987 No 4.

2. Логическое программирование"(сб. переводов по ред. В.Н. Агафонова). М., 1988.

3. Маслов С.Ю. Обратный метод установления выводимости для логических исчислений //Труды математического института им.