.. 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

Для того чтобы быть уверенным, что построенное исчисление благоприятных наборов является эквивалентным исходному секвенциальному исчислению сформулируем теорему о полноте:

Исходная формула Ф выводима тогда и только тогда, когда в исчислении благоприятных наборов получен вывод.

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

В обратную сторону, теорема следует из того, что при наличии вывода в исчислении благоприятных наборов мы по крайней мере дважды должны применить правило Б для получения пустого благоприятного набора. Но любое применение правила Б соответствует "получению" в секвенциальном выводе некоторого дизъюнкта исходной формулы Ф. При этом возможно получение не всех дизъюнктов исходной формулы. Например, для приведенной формулы Ф правило Б не будет применяться к литерам дизъюнкта под номером 7 (к числам с номером 7), а это значит, что будет получен вывод более сильной формулы Ф* без последнего дизъюнкта формулы Ф. Значит при получении пустого набора будет получено доказательство формулы Ф*, которая не слабее формулы Ф. Теорема доказана.

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

С другой стороны, процесс построения вывода утратил свойство "нормальности" секвенциальных исчислений и приобрел более творческий характер. В процессе построения выводов возможно порождение кусков дерева, которые не приводят к успеху. При применении правила Б возможно порождение множества благоприятных наборов, которые избыточны для построения выводов. Возникает проблема повышения эффективности предложенной общей схемы обратного метода.

Возможны следующие подходы решения проблемы повышения эффективности предложенной "заготовки" исчисления:

1. Модификация предложенной схемы за счет "подключения" различного рода эвристик и допустимых правил вывода, которые повышают мощность первоначальной "заготовки" исчисления. В этом случае "сфера действия" правила Б расширяется.

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