Например, при применении правила вывода к исходным благоприятным наборам [10 21] и [22 42] в результате получим новый благоприятный набор [10 42], так как числа 21 и 22 образуют полную совокупность литер второго (2) дизъюнкта F, а из благоприятного набора [10 42] получается благоприятный набор [42] исключением первого (1) однолитерного дизъюнкта F. Т.е. правило вывода исчисления является "механизмом" перехода по секвенциальному дереву "сверху вниз" от концевых секвенций к корневой секвенции, который позволяет исключать из состава наборов дизъюнкты исходной формулы. Именно с этим изменением направления поиска по сравнению с направлением поиска "снизу вверх" в секвенциальных исчислениях и связано название обратного метода. Получение пустого благоприятного набора  означает построение вывода исчисления. Например, следующая последовательность наборов является выводом исчисления чисел, построенного для исходной формулы F:

1. [10 21] 4. [10 41]

2. [22 42] 5. [10] из 3, 4

3. [10 42] из 1, 2 6.  из 5

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

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

Во втором параграфе ("Модификации общей схемы обратного метода") дается ряд модификаций предложенного исчисления чисел, с целью построения практических алгоритмов поиска вывода. Для этого в параграфе сформулированы и даны "идеи" доказательств ряда лемм, что соответствует моделированию в исчислении чисел ряда известных методов поиска вывода, среди которых можно выделить два мощных метода поиска вывода — метод резолюций и метод расщеплений. Основой моделирования этих методов является структурное сходство правила Б исчисления и правила сечения:

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

® 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

Моделирование правила резолюций (расщеплений) связано с тем, что оно представляет собой применение правила сечения "сверху вниз" ("снизу вверх) в секвенциальных исчислениях.

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

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