Статья 490

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