Опровержение методом резолюций – это алгоритм автоматического доказательства теорем в прикладном исчислении предикатов, который сводится к следующему. Пусть нужно установить выводимость
S├ G.
Каждая формула множества S и формула ØG (отрицание целевой теоремы) независимо преобразуются в множества предложений. В полученном совокупном множестве предложений C отыскиваются резольвируемые предложения, к ним применяется правило резолюций и резольвента добавляется в множество до тех пор, пока не будет получено пустое предложение. При этом возможны три случая:
- Среди текущего множества предложений нет резольвируемых. Это означает, что теорема опровергнута, то есть формула G не выводима из множества формул S.
- В результате очередного применения правила резолюции получено пустое предложение. Это означает, что теорема доказана. то есть S├ G.
Процесс не заканчивается, то есть множество предложений пополняется все новыми резольвентами, среди которых нет пустых. Это ничего не означает.