Студопедия

Главная страница Случайная лекция


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

Порталы:

БиологияВойнаГеографияИнформатикаИскусствоИсторияКультураЛингвистикаМатематикаМедицинаОхрана трудаПолитикаПравоПсихологияРелигияТехникаФизикаФилософияЭкономика



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




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

Читайте также:
  1. Индустриальные методы строительства. Унификация, типизация и стандартизация
  2. Интерпретация в логике предикатов
  3. Исходные символы языка логики предикатов
  4. Исчисление предикатов
  5. Логика предикатов
  6. Метод резолюций в логике предикатов
  7. Общезначимые эквивалентности логики предикатов
  8. Полнота и непротиворечивость исчисления предикатов
  9. Правила вывода в исчислении предикатов
  10. Проблема разрешимости в логике предикатов

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

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

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


<== предыдущая страница | следующая страница ==>
Метод семантических деревьев | Композиция подстановок

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




Мы поможем в написании ваших работ!
lektsiopedia.org - Лекциопедия - 2013 год. | Страница сгенерирована за: 0.003 сек.