Статья 486

Видно, что самая верхняя секвенция основная. Формула входит в левую и правую часть секвенции. Этот факт отметим, поставив крестик над формулой.
Заметим, что, прежде чем применять какое-либо правило к секвенции, следует проверить, не является ли она основной.
Описанная процедура поиска доказательства является полной, секвенция доказуема тогда и только тогда, когда соответствующее ей дерево поиска доказательства замкнуто. Хао Ван специально подчеркивает - и, как мы видели выше, он прав, что имеется логическая теория поиска доказательств - инференциальный анализ
Описанный выше алгоритм поиска доказательств является разрешающей процедурой для ряда классов формул. Легко видеть, что проблема разрешения для исчисления высказываний разрешима. Каждое правило вывода, примененное снизу вверх, уменьшает длину формулы. Поскольку число логических знаков в формуле конечно, то процесс поиска доказательств оборвется.