Опровержение методом резолюций
Опровержение методом резолюций – это алгоритм автоматического доказательства теорем, в исчислении высказываний (в исчислении
предикатов), который сводится к следующему.
Пусть нужно установить выводимость Г ├ G.
Каждая формула множества Г и формула<*>G независимо преобразуются в множество предложений (при этом используется в исчислении
предикатов клазуальное представление, а в исчислении высказываний КНФ). В полученном совокупном множестве предложений S
отыскиваются резольвируемые предложения, к ним применяется правило резолюций и резольвента добавляется в множество до тех
пор, пока не будет получено пустое предложение. При этом возможны три случая.
1. среди текущего множества предложений нет резольвируемых. Это означает, что теорема опровергнута, то есть формула G не
выводима из множества формул Г.
2. в результате очередного применения правила резолюции получено пустое предложение. Это означает, что теорема доказуема, то
есть Г ├ G.
3. процесс не заканчивается, то есть множество предложений пополняется все новыми резольвентами, среди которых нет пустых.
Это ничего не означает.
(исчисление предикатов является полуразрешением теорем, а метод резолюций является частичным алгоритмом автоматического
доказательства теорем. Для исчисления высказываний все будет завершаться.).