Проблемы в исчислении предикатов

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

Принцип резолюции

В логике предикатов вывод определяется так же, как в исчислении высказываний. Все правила вывода логики высказываний включены в множество правил логики предикатов.

Метод дедуктивного вывода

Эти правила определяют схему вывода и позволяют использовать правила подстановки, введения и удаления кванторов и делать вывод об истинности заключения.

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

_xò ^f(х)(P₁(x)ÚùP₂(x))=(P₁(f(x))ÚùP₂(f(x))) и

_xò ^f(х)(ùP₁(f(x))ÚP₃(y))= (ùP₁(f(x))ÚP₃(y)).

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

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

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

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

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

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