Главная | Обратная связь

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

Первый шаг. Приводим исходную формулу к предваренной нормальной форме. Для этого:

1. пользуясь эквивалентностью A B A B исключим импликацию;

2. перенесем все отрицания внутрь формулы, чтобы они стояли только перед атомными формулами, используя следующие эквивалентности:

3. (A B) A B

4. (A B) A B

5. ( xA) xA

6. ( xA) xA

7. A A

8. переименовываем связанные переменные так, чтобы ни одна переменная не входила в нашу формулу одновременно связанно и свободно.

9. выносим кванторы в начало формулы, используя эквивалентности:

QxA(x) B Qx(A(x) B), если B не содержит переменной x, а Q { , }

QxA(x) B Qx(A(x) B), если B не содержит переменной x, а Q { , }

xA(x) xB(x) x(A(x) B(x))

xA(x) xB(x) x(A(x) B(x))

Q₁xA(x) Q₂xB Q₁xQ₂y(A(x) B(y)), где Q { , }

Q₁xA(x) Q₂xB Q₁xQ₂y(A(x) B(y)), где Q { , }

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

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

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

Проведя этот процесс для всех кванторов существования, получим формулу, находящуюся в сколемовской нормальной форме.

Третий шаг. Элиминируем кванторы всеобщности. Полученная формула будет бескванторной и эквивалентной исходной в смысле выполнимости.

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

A (B C) (A B) (A C)

A (B C) (A B) (A C)

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

2.4) Дизъюнкты и их классификация.

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

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

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

2.5) Метод резолюции и его разновидности, пример преобразования для простой формулы.

Решаемая задача представляется в виде совокупности утверждений (аксиом), цель задачи также записывается в виде утверждения. Тогда решение задачи представляет собой выяснение логического следования из аксиом

(А1 ∧ А2 ∧ А3 ∧ ... Аn )→ В.

На практике удобно использовать доказательство от противного, т. е.доказывать невыполнимость. Если A → B истинно, то ложно и ложно.

На этом основан принцип резолюции, который требует представле-

ния формул исчисления предикатов в виде набора дизъюнктов, связанных операцией конъюнкции [конъюнктивная нормальная форма (КНФ)].

Правило резолюции имеет вид

Правило резолюции позволяет соединить две формулы, из одной удалив А, а из другой неA . В этом случае говорят, что A и неA резольвируют. Главная идея метода резолюции заключается в проверке того, содержит ли множество дизъюнктов R пустой (ложный) дизъюнкт. При положительном ответе формула, соответствующая R, невыполнима и соответствующее утверждение противоречиво. Таким образом, доказав невыполнимость формулы

можно сделать вывод, что В истинно.

Рассмотрим пример использования метода резолюции, применяя доказательство от противного.

Пусть необходимо доказать истинность выражения

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

1. Приводим посылки к нормальной форме (без → и ↔)

2. Записываем в нормальной форме отрицание заключения

3. Рассматриваем конъюнкцию пяти дизъюнктов

Первые два дизъюнкта дают P , что в сочетании с третьим дизъюнктом дает Q. Четвертый и пятый дизъюнкты дают Q .

Таким образом, имеем

Таким образом, доказано поскольку противоположное неверно.

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

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

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

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

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

 

3.1 Предметы и предикаты.

По сути, Пролог-система позволяет использовать ЭВМ как хранилище фактов и правил, и предоставляет механизм, позволяющий делать выводы, переходя от одних фактов к другим.

Именем отношения между объектами является ПРЕДИКАТ.

Например: name_predicates(О1,О2, .. ,ОN).

Это имя, которое записывается перед круглыми скобками. Вся запись типа name(O1,O2,..,O3) называется предикатной структурой или предикатным термом. Предикат является функтором некоторой структуры. Представление Пролог-программ в виде предикатных структур и предикатных термов обладает многими достоинствами, главное из которых - это единообразие записи функций и процедур.

ТЕРМ - единообразная структура для описания данных и предикатов на языке Пролог. Термы в Турбо-Прологе могут быть в двух формах:

1. Предикатные термы.

2. Термы-предикаты внутренней и внешней баз данных.

По структуре термы баз данных не отличаются от предикатных

термов.

Объекты данных в Прологе также называются термами. Терм может быть константой, переменной, списком или составным термом

(структурой).

 

Варианты объявления предметов, составные предметы.

Раздел описания доменов является аналогом раздела описания типов в обычных императивных языках программирования и начинается с ключевого слова DOMAINS.

В Турбо Прологе имеются стандартные домены, которые не нужно указывать в разделе описания доменов. Основные стандартные домены - это:

integer - целое число (из промежутка -32768...32767);

real - действительное число (лежащее между ±1e-307...±1e308);

char - символ, заключенный в одиночные апострофы;

string - последовательность символов, заключенная в двойные кавычки;

symbol - символическая константа (начинающаяся со строчной буквы последовательность букв латинского алфавита, цифр и знаков подчеркивания или последовательность любых символов, заключенная в кавычки).

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

Объявление домена имеет следующий вид:

<имя домена>=<определение домена>

или

file=<имя файлового домена1>;...;<имя файлового доменаN>

Удобно использовать описание доменов для сокращения имен стандартных доменов. Например, чтобы не писать каждый раз integer, можно написать следующее:

DOMAINS

i=integer

и далее использовать вместо ключевого слова integer односимвольное обозначение i.

Из доменов можно конструировать составные или структурныедомены (структуры). Структура описывается следующим образом:

<имя структуры>=<имя функтора>(<имя домена первой

компоненты>,...,<имя домена последней компоненты>)

[;<имя функтора>(...)]*

Каждая компонента структуры в свою очередь может быть структурой. Например, структура, описывающая точку на плоскости и имеющая две компоненты (координаты точки)

point = p(integer, integer)

может входить в качестве компоненты в более сложную структуру, описывающую треугольник:

triangle = tr(point, point, point)

В описание структуры могут входить альтернативы, разделенные символом ";" или ключевым словом "or".

Так, структуру, описывающую точку и на плоскости, и в пространстве, можно задать следующим образом:

point = p(integer, integer);p(integer, integer, integer).

Описание файлового домена имеет вид:

file = <символическое имя файла 1>;...;

<символическое имя файла N>

Для представления данных в Турбо Прологе, в отличие от стандартных алгоритмических языков программирования, используются не массивы, а списки. Списковый домен задается следующим образом:

<имя спискового домена>=<имя домена элементов списка>*

Например, список целых чисел описывается так:

list_of_integer=integer*

3.3.Объявление предикатов.

В разделе, озаглавленном зарезервированным словом PREDICATES, содержатся описания определяемых пользователем предикатов. Описание n-местного предиката имеет следующий вид:

<имя предиката>(<имя домена первого аргумента>,...,

<имя домена n-го аргумента>).

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

Например, PREDICATES

mother(string,string)

Это описание означает, что у предиката два аргумента, причем оба строкового типа.

Один предикат может иметь несколько описаний. Это используется, когда нам нужно, чтобы предикат работал с аргументами различной природы.

PREDICATES

member(integer,integer*)

member(real,real*)

member(char,char*)

member(string,string*)

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

Кроме того, при описании предиката можно указать, будет он детерминированным или недетерминированным. Детерминированный предикат возвращает только одно решение, а недетерминированный предикат при помощи поиска с возвратом может давать много решений. Детерминированные предикаты менее требовательны к оперативной памяти и выполняются быстрее. Для того чтобы указать, что предикат является детерминированным (недетерминированным), нужно перед его именем поместить зарезервированное слово determ (nondeterm). Если ни determ, ни nondeterm при описании предиката не использовались, то, по умолчанию, предикат считается детерминированным.

В Турбо Прологе имеется директива компилятора check_determ, которая принудительно включает проверку предикатов на детерминированность.

В Турбо Прологе есть так называемые стандартные (встроенные) предикаты, которые не нужно описывать в разделе описания предикатов PREDICATES. Все встроенные предикаты являются детерминированными.

3.4 Факты и правила для описания свойств предикатов.

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

Предложения бывают двух видов: факты, правила.

Предложение имеет вид

A:- B1,... , Bn.

A называется заголовком или головой предложения, а B1,..., Bn - телом.

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

Факт констатирует, что между объектами выполнено некоторое отношение. Он состоит только из заголовка. Можно считать, что факт - это предложение, у которого тело пустое.

ПРАВИЛО - это предикат определяемый через другие предикаты или самого себя.

Рассмотрим правило на русском языке:

Х является сестрой У, если

Х является женщиной и

Х и У имеют общих родителей.

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

Русифиц. Турбо-Пролог: Tурбо-Пролог:

является_сестрой(Х,У):- is_sister(X,Y) if

женщина(Х), woman(X) and

родители(X,F,M), parants(X,F,M) and

родители(У,F,M). parants(Y,F,M).

В правилах на Турбо-Прологе допускается использовать ':-' вместо 'if' , ',' вместо 'and' и ';' вместо 'or'. Это сделано для соответствия с другими версиями Пролога.

 

3.5.Понятие о цели.

ЦЕЛЬ - предикат, который надо согласовать с базой данных (с базой фактов и правил).

Раздел целей, начинающийся ключевым словом GOAL, является необязательным. Если он отсутствует, программа будет работать только под управлением системы (т.е. нельзя будет создать EXE -файл), при этом цель будет запрашиваться в диалоговом окне в виде

Goal:" и Турбо-Пролог будет ожидать до тех пор, пока цель не будет введена. Целью может являться любой предикат Пролог-программы или их последовательность, разделяемая запятыми. В последнем случае сложная цель согласуется, если согласуются все ее составляющие подцели.

ПОДЦЕЛЬ - предикат, который необходимо согласовать с базой данных, чтобы выполнить согласование предиката-цели, который определен через рассматриваемый; т. е. предикат который на определенном шаге работы программы сам становится целевым.

 

3.6. Примеры представления задач.

Рассмотрим, каким образом на ПРОЛОГе можно описать задачу о семейных отношениях.

Пусть имеются факты об отцовстве:

1) Иван – отец Игоря.

2) Иван – отец Сидора.

3) Сидор – отец Лизы.

Введем также три предиката:

Мужчина (x), означающий, что x – мужчина,

Единокровный (x,y), означающий единокровность x и y,

Брат (x,y), означающий, что x брат y.

Справедливы, очевидно, следующие правила:

1) «Все отцы – мужчины».

2) «Если у детей один отец, то они единокровны».

3) «Брат – это единокровный мужчина».

Рассмотрим вывод решения при ответе на вопрос:

«Есть ли братья у Игоря?».

Программа 3

DOMAINS

person = symbol

PREDICATES

otec(person,person)

man(person)

brat(person,person)

CLAUSES

man(X):-otec(X,_).

brat(X,Y):-otec(Z,Y),otec(Z,X),man(X),X<>Y.

otec(ivan,igor). otec(ivan,sidor). otec(sidor,lisa).

Во втором правиле программы указано условие X<>Y. Это позволя-

ет описать ПРОЛОГ-программе тот факт, что человек не может быть

собственным братом.

После запроса

goal: brat(igor,X)

Система выдаст

X = sidor

 

4.1. Содержательный смысл процесса решения задачи.

Программа на языке ПРОЛОГ содержит две составные части: факты и правила. Факты представляют собой данные, с которыми оперирует программа, а совокупность фактов составляет базу данных ПРОЛОГа, которая является не чем иным, как реляционной базой. Основная операция, выполняемая над данными, – это операция сопоставления, называемая также операцией унификации или согласования. Правила состоят из заголовка и подцелей. Выполнение программы, написанной на ПРОЛОГе начинается с запроса и состоит в доказательстве истинности некоторого логического утверждения в рамках заданной совокупности фактов и правил. Алгоритм этого доказательства (алгоритм логического вывода) и определяет принципы исполнения программы, написанной на ПРОЛОГе.

4.2. Примеры применения фактов и правил.

ФАКТЫ.

Введем отношение родитель (parent) между объектами.

parent (tom, bob).

Это факт, определяющий , что Том является родителем Боба.

parent - имя отношения, tom, bob - его аргументы.

Теперь можно записать программу, описывающую все дерево родственных отношений.

parent (pam, bob).parent (tom, bob).parent (tom, liz).

parent (bob, ann).parent (bob, pat).parent (mary, ann).parent (pat, juli).

Эта программа состоит из семи предложений (утверждений, фактов).

Каждое утверждение записано фактом в виде отношения parent.

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

Пример факта:

like (bob, pam).

Совокупность фактов в прологе называют базой данных (знаний).

ВОПРОСЫ.

К составленной базе данных можно задать вопросы.

Вопрос в обычном Прологе начинается с ?-

Вопрос записывается так же, как и факт.

Например:

? - parent (bob, pat).yes

Когда пролог получает вопрос, он пытается сопоставить его с базой данных. Такой факт находится, ответ: да (yes).

На вопрос

?-parent (bob,mary).no

Ответ будет нет (no), так как такого факта в базе данных нет.

ПЕРЕМЕННЫЕ.

Можно задать вопрос и узнать кто родитель liz:

?-parent (X, liz).

X= tom

Здесь X - переменная. Ее величина неизвестна и она может принимать значения. В данном случае ее значением будет объект, для которого это утверждение истинно.

Вопрос:

?-parent (X, bob).

X=tom X=pam

Можно задать вопрос, кто является чьим родителем.

Или найти такие X и Y, что X является родителем Y.

?-parent (X, Y).

X= pam Y= bob Y= tom X= bob и т.д.

КОНЪЮНКЦИЯ ЦЕЛЕЙ.

Можно задать более общий вопрос: кто является родителем родителя juli. Так как нет отношения grandparent, то можно разбить на два вопроса:

кто родитель juli. Предположим - Y.

кто родитель Y. Предположим - X.

Тогда составной вопрос:

?-parent (Y, juli), parent (X, Y).

X=bob

Y=pat

При поиске решения сначала находится Y , а затем по второму условию Х.

Вопрос: Кто внуки тома?:

?-parent (tom, Y), parent (Y, X).

Y=bob X=ann Y=bob X=pat

И наконец, есть ли у ann и pat общий родитель?

?-parent (Y, ann), parent(Y, pat).

Y=bob

ПРАВИЛА.

Введем отношение peбенок child, обратное к parent "родитель".

Можно было бы определить аналогично:

child (liz, tom).

Но можно использовать, что отношение child обратно к parent и записать в виде утверждения- правила:

child(Y, X):-parent (X, Y).

Правило читается так:

Для всех X и Y

Y - child X, если

X - parent Y.

Правило отличается от факта тем, что факт всегда истина, а правило описывает утверждение, которое будет истинной, если выполнено некоторое условие. Поэтому в правиле выделяют заключение и условие:

child(Y, X) :- parent (X, Y).

голова тело

Если условие parent (X, Y) выполняется, то логическим следствием из него будет утверждение child(Y, X).

Как правило используется прологом:

Зададим вопрос

?-child(liz, tom).

В программе нет данных о child, но есть правило, которое верно для всех X Y, в том числе для liz и tom. Мы должны применить правило для этих значений. Для этого надо подставить в правило вместо X- tom, a вместо Y - liz. Говорят, что переменные будут связаны, а операция будет называться подстановкой.

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

child(liz, tom):-parent (tom, liz).

Условная часть приняла вид

parent (tom, liz).

Теперь надо выяснить выполняется ли это условие. Исходная цель child(liz,tom) заменяется подцелью parent (tom, liz), которая выполняется, поэтому пролог ответит "yes".

4.3. Арифметические операции и смысл знака равенства.

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

+ — сложение

– — вычитание

* — умножение

/ — деление

** — возведение в степень

// — целочисленное деление

mod — деление по модулю, вычисление остатка от целочисленного деления

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

?- X = 1 + 2

Система Prolog "послушно" ответит:

X = 1 + 2

а не X = 3, как следовало ожидать. Причина этого проста — выражение 1 + 2 просто обозначает терм Prolog, в котором знак + является функтором, а 1 и 2 — его параметрами. В приведенной выше цели нет ничего, что могло бы вынудить систему Prolog фактически активизировать операцию сложения. Для определения этой проблемы предусмотрена специальная предопределенная операция is. Операция is вынуждает систему выполнить вычисление, поэтому правильный способ вызова арифметической операции состоит в следующем:

?- X is 1 + 2

В этом случае будет получен ответ:

X = 3

При этом операция сложения была выполнена с помощью специальной процедуры, которая связана с операцией is. Подобные процедуры принято называть встроенными процедурами.

Кроме того, в Prolog предусмотрены такие стандартные функции, как sin(x), cos(x), atan(x), log(x), exp(x) и т.д. Эти функции могут находиться справа от знака операции is.

Кроме того, при выполнении арифметических операций возникает необходимость сравнивать числовые значения. Операции сравнения:

X > Y. — X больше Y.

X < Y. — X меньше Y.

X >= Y. — X больше или равен Y.

X =< Y. — X меньше или равен Y.

X =:= Y. — Значения X и Y равны.

X =\= Y. — Значения X и Y не равны.