Унификация и резолюция в логике предикатов

Когда предложение j представлено в виде множества дизъюнктов, приходится работать с переменными и сколемовскими функциями. С помощью семантических деревьев можно определить, выполнима ли данная формула на соответствующем эрбрановском универсуме. Эта процедура требует значительных затрат времени. Более того, ее нельзя представить в виде хорошо структурированного алгоритма, который можно было бы реализовать на компьютере. В логике высказываний был применен метод резолюций, позволяющий за конечное число шагов выяснить, является ли данное множество дизъюнктов противоречивым. В логике предикатов роль элементарных высказываний играют атомы, т.е. предикаты различной арности. При этом одноименные предикаты, которые могли бы участвовать в резолюции, могут иметь отличающиеся аргументы. Поэтому к ним нельзя применить метод резолюции непосредственно. Чтобы преодолеть это затруднение, в логике предикатов используют алгоритм унификации, основанный на подстановке термов вместо переменных, там, где это возможно.

Пусть j - формула без кванторов, и q - подстановка. Запись jq обозначает результат замены каждого терма t в формуле j на tq.

Алгоритм унификации должен найти такие подстановки термов в атомы дизъюнктов, которые сделают эти атомы тождественными. Например, чтобы атомы P(x) и P(a) стали тождественными, достаточно выполнить подстановку q={x/a}. В общем случае при выполнении подстановок необходимо соблюдать некоторые правила, которые будут рассмотрены ниже.

Дата добавления: 2014-11-08; просмотров: 426; Нарушение авторских прав

Мы поможем в написании ваших работ!