Принцип резолюции Джона Робинсона

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

Пример.

…

Берем для доказательства формулы ее отрицания, т.е. заменяем x₃ на и пытаемся получить противоречие. Если удастся, то исходное будет доказано. По способу представления 1-4 является дизъюнктами. Любую логическую формулу можно заменить 1 или несколькими дизъюнктами. Рассмотрим дизъюнкты 1-2. Видим, что в первый x входит без отрицания а во второй с отрицанием, тогда говорят что дизъюнкты содержат контрарную пару переменных x _i = . В методе резолюций всегда берут 2 дизъюнкта, содержащих контрарную пару и находят логическое следствие для них (резольвент).

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

Метод Ковальского

….

Здесь для каждого дизъюнкта строят вершину и соединяют ребрами по контрарным парам переменных. Резольвенты строят таким образом: выбирают любое ребро связывающее 2 литеры (x₁ и не x₁) строят резольвенту дизъюнктов D₁ и D₂ по контрарной паре литер, добавляем резольвенту в форме новой вершине графа, а ребро (x₁, не x₁) удаляем, при этом действуют следующие правила:

1. Если имеется вершина в которой действует не соединенная с другими буква, то такая вершина удаляется со всеми несоединенными ребрами

2. Произвольно выбираем ребро и находим резольвенту по 2 вершинам данному ребру, добавляем резольвенту в граф и соединяем ее с другими вершинами, поле чего выбранное ребро удаляем из графа. Тавтологические дизъюнкты удаляем.

3. Вершины резольвенты связываются связями с другими вершинами по контрарным литерам

4. Если в графе Ковальского получены две вершины x_i и не x_i то говорят о противоречии и процесс завершается

5. Если граф Ковальского удается полностью разрушить без получения противоречия, то это говорит о том, что система не противоречива.

Метод отсечения литер

Дизъюнкты:

….

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

Включим в новую систему все формулы, представляющие собой резольвенту по x₁

 

Базовые [EB5] понятия ПРОЛОГ

1. Прикладные системы на языке Prolog. Роль языка Prolog.

Сферы применения пролога – транспорт, логистика, анализ месторождений полезных ископаемых, оценка загрязнений окружающей среды, Системы с естественно-языковым интерфейсом, НАСА использует голосовой Пролог для управления голосом аппаратурой.

2. Базовые понятия и структура программы

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

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

2. Предикаты правила

3. Стандартные предикаты. Входят в состав самого пролога и считаются истинными(write(X) – вывод на экран, nl – переход на новую строку

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

Стандартные типы данных

1. Integer

2. Char

3. String

4. Real

5. Symbol

6. Etc.

Структура программы и назначение секций:

Программа на прологе состоит из 4-х секций:

1. Domains

2. Predicates

3. Goal

4. Clauses

В секции predicates происходит объявление не стандартных предикатов, т.е. пользовательских. Объявление происходит через ключевое слово nondeterm.

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

Секция goal. Здесь задается целевой предикат программы или последовательность предикатов, которые надо доказать.

Секция clauses содержит доказательство целевого предиката.

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

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

2. Сопоставление константы и переменной (свободной, не имеющей значения) заканчивается успешно и переменная получает значение константы (становится связанной)

3. Сопоставление двух связанных переменных: сопоставление заканчивается успешно если переменные равны и неудачно в противном случае. Одна из переменных связана – другая свободна: заканчивается успешно и свободная переменная принимает значение связанной; Сопоставление двух свободных переменных успешно, если в последствии одна из переменных получает значение, то и другой переменной присваивается тоже значение.

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

Пусть некто сообщает, что он задумал шифр из 5-ти двузначных цифр. Обозначим их как X₁,.., X₅. При этом задаются следующие соотношения между цифрами. При этом

X₂+X₃+X₄<=2,

X₂+x4+X5 <=1,

X₃+X₄+X₅>=1;

X₁+X₅<=1

Пример

predicates nondeterm equation nondeterm znach(integer) goal equation. clauses   equation:- znach(X1), znach(X2), znach(X3), znach(X4), znach(X5), X2+X3+X4<=2, X2+X4+X5<=1, X3+X4+X5>=1, X1+X5<=1, write(“X1=”,X1,” X2=”,X2,” X3=”,X3,” X4=”,X4,” X5=”,X5). znach(B):-B=0; B=1.

 

Данная программа состоит из 3х секций. В секции predicates объявлены 2 предиката: equation and znach. В секции goal задается целевой предикат equation. В clauses происходит непосредственно доказательство результата equation. Для того чтобы доказать целевой предикат, система выбирает первое условие из определения предиката- znach(X1). Пролог пытается доказать это условие и ищет его определение в разделе clauses. Такое определение имеется. Происходит унификация или же согласование аргументов предикатов, т.е. X1 согласовывается с B. Т.к. B = 0, то и X1 Получает значение 0. Аналогично доказываются предикаты znach(X2 -X5). Далее выполняется проверка условий, однако X3 + X4 +X5 >=1 условие не выполняется, поэтому в силу вступает механизм ветвления-возврата. Система возвращается в точку последнего ветвления, т.е. Znach(X5). На этот раз пролог сопоставит Znach(X5) и Znach(B): B=1. Znach(X1-X4) по-прежнему нули, и вновь выполняем проверку условий. Если все успешно, то происходит вывод на экран.

Предикат fail

Инициирует неудачу в доказательстве. Пролог начинает поиск с возвратом, когда доказательство какого-либо предиката завершается неудачей. Определенной ситуации бывает необходимо инициировать поиск с возвратом, чтобы найти другое решение, для этого используется специальный предикат FAIL – неудача.

Predicates Nondeterm father(symbol,symbol) Nondeterm everybody Clauses Everybody:- Father(X,Y) Write (X,”is father”,Y), nl, Readchar(_), fail.\father(leonard, Katherine). Father(karl, nick). Father(carl,Marilyn). Goal Everybody.

 

Программа требует найти отца Y. Fail делает доказательство всегда неудачным.

Для того, чтобы вывести все решения в теле предиката everebody поставили команду fail. После того как на экран выводится значение переменных x=leonard, y=Katerina, возникает состояние искусственной неудачи (fail). Происходит возврат к ближайшей развилке, т.е. father(X,Y), т.к. этот предикат не сопоставлялся с двумя оставшимися факторами. При этом переменные X и Y становятся свободными. Теперь предикат father(X,Y) сопоставляется с фактом father(karl, nick). Переменные X, Y получают соответствующие значения и далее вывод осуществляется по аналогии.

Механизм отсечения

Пролог использует отсечения для прерывания поиска с возвратом. Обозначается как «!». Пройдя через отсечение уже невозможно произвести откат к предикатам, расположенным в обрабатываемом предложении перед отсечением, а также невозможно возвратиться к другим предложениям. Определяющим данный предикат.

 

 

r1:- a,b, !, c. r1.

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

Predicates Nondeterm buy (symbol, symbol) Nondeterm car(symbol, sumbo, integer) Nondeterm colors(symbol, symbol) Goal Buy(corevette, Y). Clauses Buy(model, Color):- Car(model, Color,Price), Colors(Color, good), !, Price < 25000, Write(Model), Readchar (_). Car (alpha romeo, green, 25000). Colors (red, good). Car(corvete, black 24000) colors(black, mean).

 

В данном примере необходимо найти корвет конкретного цвета и подходящего по цене.

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

Рекурсия

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

Пример:

Goal Like (peter, X), write(x) Clouses Like(John, carrot). Like (peter,Z):-like(John,Z)

 

Программа требует найти предмет который нравится Петру. Первый клоз заканчивается FALSE, т.к. не совпадают константы. Второй заканчивается тру и X сопоставляется с Z. Z и X получают значение carrot.

Изменим программу следующим образом:

goal like (peter, X), write(x) clauses like(John, carrot). like(peter,candies):-fail. like(peter,Z):- not(like(jhon,Z)).

Как и ранее программа требует найти то, что нравится Пете, однако теперь логика программы изменена. Пете нравится то, что не нравится Джону. Это факт мы переделали следующим образом: like(peter,Z):- not(like(Jhon,Z)). Отрицание передают предикат not, однако, следует помнить, что данные предикат не может использоваться в голове правила, т.е. недопустимо: not(like(peter,Z)):-like(Jhon,Z). Однако имеется и второе ограничение: в момент вызова предиката с отрицанием аргументы предиката уже должны иметь значения. В этом случае пролог выдаст сообщение об ошибке.

Переделаем программу следующим образом:

Predicates Like(symbol,symbol) znach(symbol)   goal like (peter, X), write(x) clauses like(John, carrot). like(peter,candies):-fail. like(peter,Z):- znach(Z), not(like(jhon,Z)).   Znach(carrot). Znach(candies).

В znach поместили carrot, доказываем like(Jhon,carrot). Доказали его в первом клозе. Далее вернулись в правило, а там стоит предикат not(like(Jhon, carrot)), отрицание истины дает ложь, следовательно, откатываемся до ближайшей развилки, а именно предиката znach, и заносим в переменную Z значение candies. Далее снова доказываем предикат like(Jhon, candies). Доказали его во втором клозе. Заходим во второй, клоз, унификация проходит успешно, однако там стоит предикат fail, который инициирует неудачу в доказательстве, следовательно предикат like(Jhon,candies) заканчивается ложью. Возвращаемся в правило, not(like(Jhon,candies)) = true (отрицание лжи = истина). Таким образом предикат like() доказан, и соответственно цель (goal) доказано, а X принимает значение candies.

 

predicates   goal fact(3,1,M) write(“fact:”, M clauses fact(1,N,M):-M=N. fact(Z,N,M):- N1=Z*N, Z1= Z- 1, Fact(Z1,N1,M)

Z- начальное значение, N – промежуточное (накапливаемое), M – окончательное.

N=1

N1=3

Z1=2

Fact(2,3,M)

N1=6

Z1= 1

Fact(1,6,M)

M=N // M= 6;

predicates   goal fact(3,M) write(“fact:”, M clauses fact(1,1. fact(N,M):- N1=N-1, Fact(N1, M1) M=M1*N

 

Fact(3,M)

N =3

N1=2

Fact(2,M1)

M=2

N1=1

Fact(1,M1)

Fact(1,1)

M=M1*N // M=1*2 = 2

M=M1*N // M = 2*3 =6

 

Сложные структуры данных в прологе. Функторы и списки

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

Domains Списочный_тип=тип*

 

Где тип – тип элемента списка. Он может быть, как стандартным, так и не стандартным, т.е. заданным пользователем и объявленным в разделе domains ранее.

Пример

Domains List=integer* Predicates Nondeterm number(list)

Кроме того, элементами списка могут быть не только числа, но и строки, а также и сами списки, например:

Doamins list=integer* // L=[1,2,3] list2=string* // L= [“vova”,”petya”] list3=list* // L=[[1,2],[3,4]]

Ввод списка с клавиатуру осуществляется через readterm(<тип>m <имя переменной>), где тип – списочный тип, который предварительно должен быть объявлен в разделе domains.

Вывод списка на экран осуществляется через предикат write(L), где L – список.

Для удобства обработки списков введены понятия головы и хвоста списка. Голова – первый элемент списка, хвост – остальная часть списка, таким образом хвост списка сам является списком.

Для представления списка в виде головы и хвоста используется следующая запись:

L=[H|T], где H – голова, T – хвост L=[X] – список из одного элемента, причем X – голова, а хвост – пустой список ([]).

Пустой список нельзя разделить на голову и хвост.

Рекомендации по работе со списками:

1. Операциями со списками практически всегда используется рекурсия

2. Обычно предикаты для реализации работы со списками имеют несколько клозов. Первый из них относится к простейшему случаю (например, к операции с пустым списком, со списком из одного элемента, с головой списка). Последующие клозы относятся к более общим случаям и имеют следующее назначение: Если список не соответствует простейшему случаю, рассмотренному в первом клозе, то его следует уменьшить на 1 элемент, например, исключить голову, и применить рекурсию к укороченному списку.

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

 

Пример

domains list=integer* predicates prinad(list,integer)   clauses prinadl([], _):-write(“Ne prinadl”). // _ - означает любое значение или не интересует prinadl([H|T],H):-write(“prinadl”). prinadl([_ | T], X):- prinadl(T,X). // [_ | T] – означает любое значение   goal prinadl([1,2,3,4],5)

Здесь мы последовательно отрываем голову от списка, и сравниваем ее с искомым числом. Если голова списка совпадает с X то, элемент принадлежит списку, в противном случае мы рекурсивно вызываем предикат prinadl с укороченным на 1 числом элементов списка

Сумма элементов списка через 2 аргумента!!!

Cписки вводят с клавиатуры