Метод резолюций в исчислении предикатов

Если матрица формулы в результате приведения к виду ПНФ не будет содержать свободных переменных и сколемовских функций, то для вывода заключения полностью пpименим алгоритм метода резолюций, рассмотренный в исчислении высказываний. Этот алгоритм основан на том, что если две формулы состоящие из дизъюнкции атомов (в дальнейшем такие формулы будем называть дизъюнктами) связаны конъюнкцией, и в них имеются два одинаковых или приводимых к одинаковым (унифицируемых) атома с разными знаками, то из них можно получить третий дизъюнкт, который будет логическим следствием первых двух, и в нем будут исключены эти два атома. Однако, если в результате приведения к виду ССФ аргументы атомов содержат сколемовские функции, то для поиска контрарных атомов необходимо выполнить подстановки термов вместо предметных переменных и получить новые формулы дизъюнктов, которые допускают их унификацию при формировании контрарных пар. Множество подстановок нужно формировать последовательно, просматривая каждый раз только одну предметную переменную.

Например, если даны два дизъюнкта (P ₁(x)Ú ) и ( Ú P ₃(y)), то для получения контрарной пары атомов возможна подстановка

В результате склеивания этих дизъюнктов может быть получена резольвента: Ú ( Ú P ₃(y))º( Ú P ₃(y)).

Если пара дизъюнктов имеет вид и Ú P ₃(y), то никакая подстановка не позволит сформировать резольвенту.

Пример. Даны две формулы и . Выполнить унификацию контрарных атомов.

1) ;

2) ;

3) .

В результате получены два контрарных атома: и . Если в эти формулы атомов вместо предметной переменной y сделать подстановку предметной постоянной b, т.е.

то получим два контрарных высказывания.

Пример. Даны две формулы и . Выполнить унификацию контрарных формул.

1) ;

2) ;

3) ;

4) .

В результате получены две контрарных формулы: и .

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

Линейным выводом из множества дизъюнктов S называется последовательность дизъюнктов D ₁, D ₂,... D_n, где каждый член D_i Î S, а каждый D_i ₊₁является резольвентой центрального дизъюнкта (или предшествующей резольвенты) и бокового дизъюнкта из множества S.

Упорядоченным дизъюнктом называется дизъюнкт с заданной последовательностью атомов. Атом P_j старше атома P_i в упорядоченном дизъюнкте тогда и только тогда, когда j > i. Например, в упорядоченном дизъюнкте (P ₁Ú P ₂Ú P ₃Ú P ₄) младшим считается атом P ₁, а старшим – P ₄. При наличии в упорядоченном дизюънкте двух одинаковых атомов по закону идемпотенции следует удалить старший атом, сохранив на прежнем месте младший.

Другим усилением метода резолюции является использование информации о резольвируемых атомах. Обычно при выполнении процедуры унификации происходит удаление резольвируемых атомов. Однако они несут полезную информацию. Поэтому вместо удаления резольвируемых атомов при унификации предлагается удалять только старший атом, а младший – сохранить в резольвенте, выделив какой-либо рамкой. Если за обрамленным атомом в резольвенте не следует никакой другой атом, то обрамленный атом удалить. Если за обрамленным атомом резольвенты следует какой-либо необрамленный атом, то его следует оставить для последующего исследования. И, наконец, если последний необрамленный атом резольвенты унифицируется с отрицанием атома боковой ветви, то его следует обрамить и удалить вместе с литерой боковой ветви. Используя резольвенты на последующих этапах, можно получить обрамленными все атомы последней резольвенты, т. е. получить пустой дизъюнкт.

Пример. Суждение «Преподаватели принимали зачеты у всех студентов, не являющихся отличниками. Некоторые аспиранты и студенты сдавали зачеты только аспирантам. Ни один из аспирантов не был отличником. Следовательно, некоторые преподаватели были аспирантами». Пусть P ₁(x)=«x – отличник», P ₂(x)=«x – аспирант», P ₃(x)=«x – студент», P ²₄ (x, y)=«x сдает зачет y», P ₅(x)=«x – преподаватель». Формулы этого рассуждения имеют вид: