2. Алгоритмы унификации

3. Структура пролог-программы

4. Организация повторов

5. Ветвление-выбор

6. Стандартные математические предикаты

7. Списки и операции над ними

8. Сортировка списков

9. Выборка элементов из списков

10. Слияние списков

11. Множества в Прологе

12. Реализация деревьев в Прологе

13. Функциональный подход программирования

14. Методы обработки списков (ЛИСП)

15. Определение универсальной функции

16. Предикаты и истинность в ЛИСПе

17. Отображения и функционалы

18. Имена, определения и контексты в ЛИСП 180

19. Prog выражения и циклы в ЛИСП

20. Списки свойств атомов и структура списков

21. Числа и мультиоперации

22. Функционалы - общее понятие

23. Безымянные функции

24. Экспертные системы. Реализация в Пролог и Лисп

1. ПОНЯТИЯ ПРЕДИКАТА.

2. АЛГОРИТМЫ УНИФИКАЦИИ

Унификация позволяет отождествлять формулы логики первого порядка путем замены свободных переменных на термы.

Подстановка Y называется унификатором простых выражений A и B, если AY=BY. Про A и B в такой ситуации говорят, что они унифицируемы. Унификация используется в Прологе для композиции и декомпозиции структур данных. Унификатор называют наиболее общим (или простейшим) унификатором простых выражений A и B, если он является более общей подстановкой, чем все другие унификаторы простых выражений A и B.

АЛГОРИТМ ПОИСКА наиболее общего унификатора.:

Шаг 1. Полагаем k=0, .

Шаг 2. Если - одноэлементное множество, останавливаем алгоритм, - наиболее общий унификатор для S. В противном случае строим множество рассогласований и переходим к третьему шагу.

Шаг 3. Если в существуют переменная x и терм t такие, что x не входит в t, то полагаем что . Увеличиваем на единицу k, переходим ко второму шагу. Иначе останавливаем алгоритм, множество S не унифицируемо.

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

МЕТОД РЕЗОЛЮЦИЙ.

Алгоритм, дающий ответ на вопрос, может ли быть выведено некоторое заключение из множества имеющихся посылок. Известно, что в общем случае даже для логики первого порядка такой алгоритм невозможен. Однако Робинсон решил, что правила вывода, используемые компьютером при автоматическом выводе, не обязательно должны совпадать с правилами вывода, используемыми при "человеческом" выводе. В частности, он предложил вместо правила вывода "modus ponens", которое утверждает, что из A и A B выводится B, использовать его обобщение, правило резолюции, которое сложнее понимается человеком, но эффективно реализуется на компьютере. Давайте попробуем разобраться с этим правилом.

ПРАВИЛО РЕЗОЛЮЦИИ для логики высказываний можно сформулировать следующим образом.

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

Графически это правило можно изобразить так:

Здесь A P и B ¬P — родительские дизъюнкты, P и ¬P — контрарные литералы, A B — резольвента.

Если родительские дизъюнкты состояли только из контрарных литералов, то резольвентой будет пустой дизъюнкт.

Пример. Правило вывода "modus ponens" получается из правила резолюции, если взять в качестве родительских дизъюнктов C₁=A, C₂=¬A B( A B). Контрарными литералами в применении этого правила будут A и ¬A, резольвентой — формула B.

Сформулируем правило резолюции для логики первого порядка.

Пусть имеется два дизъюнкта C₁ и C₂, у которых нет общих переменных, L₁ — литерал, входящий в дизъюнкт C₁, L₂ — литерал, входящий в дизъюнкт C₂. Если литералы имеют наибольший общий унификатор θ, то дизъюнкт (C₁θ–L₁θ)(C₂θ–L₂θ) называется резольвентой дизъюнктов C₁ и C₂. Литералы L₁ и L₂ называются контрарными литералами. То же правило записывается в графическом виде как

(A P₂, B ¬P₂)/(A B)θ

Здесь P₁ и P₂ — контрарные литералы, (A B)θ — резольвента, полученная из дизъюнкта (A B) применением унификатора θ, A P₁ и B P₂ — родительские дизъюнкты, а θ — наибольший общий унификатор P₁ и P₂.

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

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

Возможны, вообще говоря, три случая:

1. Этот процесс никогда не завершается.

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

3. На очередном шаге получена пустая резольвента. Это означает, что множество дизъюнктов невыполнимо и, следовательно, начальная формула выводима.

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

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

В сущности, метод резолюций несовершенен и приводит к "комбинаторному взрыву". Однако некоторые его разновидности (или стратегии) довольно эффективны. Одной из самых удачных стратегий является линейная или SLD-резолюция для хорновских дизъюнктов (Linear resolution with Selection function for Definition clauses), то есть дизъюнктов, содержащих не более одного положительного литерала. Их называют предложениями или клозами.

Если дизъюнкт состоит только из одного положительного литерала, он называется фактом. Дизъюнкт, состоящий только из отрицательных литералов, называется вопросом (или целью или запросом). Если дизъюнкт содержит и позитивный, и негативные литералы, он называется правилом. Правило вывода выглядит примерно следующим образом ¬A₁ ¬A₂...¬A_n B. Это эквивалентно формуле A₁ A₂... A_n B, которая на Прологе записывается в виде

B:–A₁,A₂,...,A_n.

Логической программой называется конечное непустое множество хорновских дизъюнктов (фактов и правил).

При выполнении программы к множеству фактов и правил добавляется отрицание вопроса, после чего используется линейная резолюция. Ее специфика в том, что правило резолюции применяется не к произвольным дизъюнктам из программы. Берется самый левый литерал цели (подцель) и первый унифицируемый с ним дизъюнкт. К ним применяется правило резолюции. Полученная резольвента добавляется в программу в качестве нового вопроса. И так до тех пор, пока не будет получен пустой дизъюнкт, что будет означать успех, или до тех пор, пока очередную подцель будет невозможно унифицировать ни с одним дизъюнктом программы, что будет означать неудачу.

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

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

.

.