Опровержение методом резолюции

Опровержение методом резолюции – это алгоритм автоматического доказательства теорем в прикладном исчислении предикатов, который сводится к следующему. Пусть установлена выводимость .

Каждая формула множества S и формула ` G (это отрицание целевой теоремы) независимо преобразуются в множества предложений. В полученном совокупном множестве предложений отыскиваются резольвируемые предложения. К ним применяется правило резолюций и резольвента добавляется в множество предложений до тех пор, пока не будет получено пустое предложение. При этом возможны 3 случая:

1) Среди текущего множества предложений нет резольвируемых. Это означает, что теорема опровергнута, т.е. формула G не выводима из множества формул S.

2) В результате очередного применения правила получено пустое предложение – это означает, что теорема доказана, т.е. .

3) Процесс не заканчивается, т.е. множество предложений пополняется все новыми резольвентами, среди которых нет пустых. Это ничего не означает.