SHPORA.net :: PDA

[ Back ]

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



предикатов), который сводится к следующему.

Пусть нужно установить выводимость Г ├ G.

Каждая формула множества Г и формула<*>G независимо преобразуются в множество предложений (при этом используется в исчислении



предикатов клазуальное представление, а в исчислении высказываний КНФ). В полученном совокупном множестве предложений S



отыскиваются резольвируемые предложения, к ним применяется правило резолюций и резольвента добавляется в множество до тех



пор, пока не будет получено пустое предложение. При этом возможны три случая.

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



выводима из множества формул Г.

2. в результате очередного применения правила резолюции получено пустое предложение. Это означает, что теорема доказуема, то



есть Г ├ G.

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



Это ничего не означает.

(исчисление предикатов является полуразрешением теорем, а метод резолюций является частичным алгоритмом автоматического



доказательства теорем. Для исчисления высказываний все будет завершаться.).