Метод резолюций и его применение в алгебре высказываний и алгебре предикатов

Размещено на http://www.allbest.ru/

Министерство образования и науки

Российской Федерации

Курганский государственный университет

Кафедра алгебры, геометрии и методики преподавания математики

Курсовая работа

Метод резолюций и его применение в алгебре высказываний и алгебре предикатов

Студент группы №2317. /Красножон Е.А./

Специальность 010101Математика

Руководитель

Кандидат пед. наук /Чернышова А.В./

Курган 2009

Содержание

Введение

Принцип резолюций в логике высказываний

Доказательства невыполнимости, основанные на принципе резолюций

Приложения и примеры использования метода резолюций

Метод резолюций в логике предикатов

Стратегии метода резолюций

Примеры использования метода резолюций

Заключение

Список используемой литературы

Введение

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

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

В октябре 1981 года Японское министерство международной торговли и промышленности объявило о создании исследовательской организации -- Института по разработке методов создания компьютеров нового поколения (Institute for New Generation Computer Technology Research Center). Целью данного проекта было создание систем обработки информации, базирующихся на знаниях. Предполагалось, что эти системы будут обеспечивать простоту управления за счет возможности общения с пользователями при помощи естественного языка. Эти системы должны были самообучаться, использовать накапливаемые в памяти знания для решения различного рода задач, предоставлять пользователям экспертные консультации, причем от пользователя не требовалось быть специалистом в информатике. Предполагалось, что человек сможет использовать ЭВМ пятого поколения так же легко, как любые бытовые электроприборы типа телевизора, магнитофона и пылесоса. Вскоре вслед за японским стартовали американский и европейский проекты.

Появление таких систем могло бы изменить технологии за счет использования баз знаний и экспертных систем. Основная суть качественного перехода к пятому поколению ЭВМ заключалась в переходе от обработки данных к обработке знаний. Японцы надеялись, что им удастся не подстраивать мышление человека под принципы функционирования компьютеров, а приблизить работу компьютера к тому, как мыслит человек, отойдя при этом от фон неймановской архитектуры компьютеров. В 1991 году предполагалось создать первый прототип компьютеров пятого поколения.

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

В качестве основной методологии разработки программных средств для проекта ЭВМ пятого поколения было избрано логическое программирование. Логическое программирование основано на таком разделе математической логики, как исчисление предикатов. Точнее, его базис составляет процедура доказательства теорем методом резолюции для хорновских дизъюнктов.

Этот метод, разработанный американским математиком Дж. Робинсоном в 1965 году, способствовал значительному прогрессу в автоматическом доказательстве теорем. Корни этого метода лежат в исследованиях известного французского логика Ж. Эрбрана, который в 1930 году доказал очень важную теорему, послужившую основой для предложенного им механического метода доказательства теорем. Но при отсутствии в то время вычислительных машин алгоритм Эрбрана оказался весьма трудоёмким для ручных вычислений и не получил практического применения.

С появлением вычислительных машин интерес к механическому доказательству теорем резко возрос. В 1960 году эрбрановский алгоритм был реализован на ЭВМ, были сделаны попытки его усовершенствования, но полученные программы были всё же мало эффективны. Значительный прогресс в деле автоматического доказательства теорем начался с открытия Робинсоном в 1965 году принципа резолюций.

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

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

Принцип резолюций в логике высказываний

Не существует общего, по-настоящему эффективного критерия для проверки выполнимости КНФ (Конъюнктивной Нормальной Формы). Тем не менее, есть достаточно удобный метод для выявления невыполнимости множества дизъюнктов. Действительно, множество дизъюнктов невыполнимо тогда и только тогда, когда пустой дизъюнкт ? является логическим следствием из него. Таким образом, невыполнимость множества S можно проверить, порождая логические следствия из S до тех пор, пока не получим пустой дизъюнкт.

Для порождения логических следствий будет использоваться очень простая схема рассуждений. Пусть A, B и X - формулы. Предположим, что две формулы () и () - истинны. Если Х тоже истинна, то отсюда можно заключить, что В истинна. Наоборот, если Х ложна, то можно заключить, что А истинна. В обоих случаях () истинна. Получается правило:

|=

которое можно записать также в виде:

|=

В том частном случае, когда Х - высказывание, а А и В - дизъюнкты, это правило называется правилом резолюций.

Например, из дизъюнктов и выводим дизъюнкты . Обратим внимание на то, что в первых двух дизъюнктах есть еще одна пара противоположных литералов. Условимся, что можно применять правило резолюций не обязательно к самым левым литералам (поскольку мы не различаем дизъюнкты, отличающиеся порядком записи литералов). Тогда правило резолюций, примененное к Y и , даст .

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

Например, если

S={, , X},

то последовательность

D₁=, D₂=, D₃=, D₄=X, D₅=

- вывод из S. Дизъюнкт выводим из S.

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

Теорема. Множество дизъюнктов логики высказываний S невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт.

Доказательство.

Докажем вначале достаточность. Отметим, что правило резолюций сохраняет истинность. Это означает, что если j()=1 и j()=1 для некоторой интерпретации j, то j()=1. Действительно, пусть j()=1 и j()=1. Тогда если j(F)=1, то и j()=1. Если же j(F)=0, то j(ШX)=1, поскольку j()=1. Но в этом случае j(X)=0 и j(G)=1, так как j()=1. Если же j(G)=1, то и j()=1.

Пусть из S выводим пустой дизъюнкт. Предположим противное: множество S выполнимо, т.е. существует интерпретация y, при которой все дизъюнкты из S истинны. Выводимость пустого дизъюнкта из S означает, что существует последовательность дизъюнктов D₁,…,D_n=?, каждый дизъюнкт которой принадлежит S или получается из предыдущих по правилу резолюций. Если дизъюнкт D_j из этой последовательности принадлежит S, то по предположению y(D_j)=1. Если же он получается из предыдущих по правилу резолюций, то также y(D_j)=1, поскольку правило резолюций сохраняет истинность. При i=n получаем, что y(?)=1. Противоречие показывает, что предположение о выполнимости множества S - ложное предположение. Следовательно, S невыполнимо. Достаточность доказана.

Докажем необходимость. Доказательство проведем индукцией по следующему параметру: d(S)=сумма числа вхождений литералов в дизъюнкты из S минус число дизъюнктов.

Пусть множество дизъюнктов S невыполнимо. Если пустой дизъюнкт принадлежит S, то он выводим из S (вывод в этом случае состоит из одного пустого дизъюнкта) и необходимость теоремы доказана. Будем считать в силу этого, что ?S. При этом предположении каждый дизъюнкт содержит хотя бы один литерал и поэтому dі1.

База индукции: d(S)=1. Если d(S)=1, то все дизъюнкты состоят из одного литерала. Поскольку множество S невыполнимо, то в нем должна найтись пара противоположных литералов X и . В таком случае пустой дизъюнкт выводим из S, соответствующий вывод содержит три дизъюнкта: X, ,.

Шаг индукции: d(S)>1. Предположим, что для любого множества дизъюнктов Т такого, что d(Т)<d(S) необходимость теоремы доказана.

Пусть

S={D₁,D₂,…,D_k-1,D_k}.

Так как d(S)>1, то в S существует хотя бы один неодноэлементный дизъюнкт. Будем считать, что это дизъюнкт D_k, т.е. D_k=LD_k?, где L - литерал и D_k?№?. Наряду с множеством дизъюнктов S рассмотрим еще два множества дизъюнктов

S₁={D₁,D₂,…,D _k-1,L},

S₂={D₁,D₂,…,D_k-1,D_kґ}.

Ясно, что S₁ и S₂ невыполнимы и что d(S₁)<a(S) и d(S₂)<a(S). По предположению индукции из S₁ и S₂ выводим пустой дизъюнкт.

Пусть A₁,A₂,…,A_i,…,A_l-1,A_l=? - вывод пустого дизъюнкта из S₁ и B₁,B₂,…,B_j,…B_m-1,B_m=? - вывод пустого дизъюнкта из S_2. Если в первом выводе не содержится дизъюнкта L, то эта последовательность дизъюнктов будет выводом из S и необходимость теоремы доказана. Будем считать, что L содержится в первом выводе, пусть A_i=L. Аналогично предполагаем, что B_j=D_k?.

Если дизъюнкт Е получается из дизъюнктов Е₁ и Е₂ по правилу резолюций, то будем говорить, что Е непосредственно зависит от Е₁ (и от Е₂). Транзитивное замыкание отношения непосредственной зависимости назовем отношением зависимости (Другими словами, E зависит от Еґ, если существуют дизъюнкты Е₁,…,Е_2n такие, что E=E₁,…,E_n=Eґ_ и Е₁ непосредственно зависит от Е₂,…,E_n-1 непосредственно зависит от E_n). Преобразуем второй вывод следующим образом: к дизъюнкту B_j и всем дизъюнктам, которые от него зависят, добавим литерал L. Новая последовательность дизъюнктов B₁, B₂,…, B_jґ= D_kґL, Bґ_j+1,…,B_mґ (*) будет выводом из S. Если дизъюнкт B_m не зависит от B_j, то B_mґ =?. Это означает, что из S выводим пустой дизъюнкт, и необходимость теоремы доказана. Предположим, что B_m зависит от B_j. Тогда B_mґ=L. Преобразуем теперь первый вывод: на место дизъюнкта A_i (равного L) в этой последовательности подставили последовательность (*). Получим последовательность

A₁,…,A_i-1,B_1,…,Bґ,Bґ_j+1,…,B _mґ=L,A _i+1,…,A _l=?.

Эта последовательность является выводом пустого дизъюнкта из множества дизъюнктов S. Следовательно, если множество S невыполнимо, то из S выводим пустой дизъюнкт.

Теорема доказана.

Для доказательства того, что формула G является логическим следствием множества формул F₁,…,F_k метод резолюций применяется следующим образом. Сначала составляется множество формул T={F₁,…,F_k, }. Затем каждая из этих формул приводится к конъюнктивной нормальной форме и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов S. И, наконец, ищется вывод пустого дизъюнкта из S. Если пустой дизъюнкт выводим из S, то формула G является логическим следствием формул F₁,…,F_k. Если из S нельзя вывести ?, то G не является логическим следствием формул F₁,…,F_k.

Проиллюстрируем сказанное на примере. Покажем, что формула G=Z является логическим следствием формул F₁=, F₂=. Сформируем множество формул T={F₁,F₂, }. Приведем формулы F₁ и F₂ к КНФ (формула сама имеет эту форму). Мы получим, что F₁ равносильна , F₂ равносильна (YZ).

Тогда множество дизъюнктов S равно {X, , YZ, }.

Из множества S легко выводится пустой дизъюнкт: , , , YZ, Y, ?.

Следовательно, формула G является логическим следствием формул F₁, и F₂.

Общезначимость правила резолюций выражается следующей леммой.

Лемма (1). Пусть s₁ и s₂ - дизъюнкты нормальной формы S, l - литера. Если и ,то дизъюнкт является логическим следствием нормальной формы S. (Дизъюнкт r называется резольвентой дизъюнктов s₁ и s₂).

Следствие. Нормальные формы S и S эквивалентны.

Доказательства невыполнимости, основанные на принципе резолюций

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

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

При условии, что ? S:

1)выбираем l, s₁ и s₂, такие что и ;

2) вычисляем резольвенту r;

3) заменяем S на S.

В качестве примера проверим невыполнимость множества

S=.

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

1.

2.

3.

4.

Затем вычисляются и добавляются к S резольвенты. В списке, который приводится ниже, каждый дизъюнкт - резольвента некоторых из предшествующих дизъюнктов. Номера их приведены в скобках справа от соответствующей резольвенты.

5. (1,3)

6. (1,4)

7. (2,3)

8. (2,4)

9. (2,5)

10. (3,6)

11. (3,8)

12. (4,5)

13. (4,7)

14. ? (4,9)

Замечание. Алгоритм проверки невыполнимости - недетерминированный, вообще говоря, возможен не один выбор для l, s₁ и s_2. В приведённом примере мы выбирали дизъюнкты s₁ и s₂ в лексикографическом порядке номеров. Такая стратегия неоптимальна. Некоторые резольвенты оказались ненужными, а также вычислялись в некоторых случаях более одного раза. Для сравнения продемонстрируем теперь применение этого же алгоритма с минимумом резолюций:

5. (1,4)

6. (2,4)

7. (3,6)

8. ? (5,7)

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

Прежде всего, если множество S не содержит ни одной пары дизъюнктов, допускающих резольвенту, то оно выполнимо (разумеется, за исключением случая, когда оно содержит пустой дизъюнкт). Интерпретация I получается заданием l(p)=И тогда и только тогда, когда положительная литера p принадлежит одному из дизъюнктов множества S.

Во-вторых, если выполнение этого алгоритма закончилось «нормально» после порождения пустого дизъюнкта, то установлена невыполнимость исходного множества S. Это непосредственное следствие леммы 1.

Может случиться, что выполнение алгоритма не завершится, хотя число различных дизъюнктов, которые могут быть порождены с помощью резолюций, очевидно, конечно. Например, такое явление имеет место для множества . Резольвентный дизъюнкт q будет порождаться неограниченное число раз. Рассмотрим также случай невыполнимого множества . Оптимальная стратегия установит невыполнимость посредством построения резольвент q, а затем ?. Напротив, «неадекватная» стратегия приведёт к зацикливанию, которое только что было отмечено. Таким образом, можно констатировать, что стратегия влияет не только на эффективность алгоритма, но и на его завершаемость.

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

Лемма (2). Если множество дизъюнктов S невыполнимо и содержит резольвенты своих элементов, то оно обязательно содержит пустой дизъюнкт.

Число различных дизъюнктов, которые можно составить на основе конечного множества S, конечно. Таким образом, лемма 2 лаёт простое общее средство решения вопроса о выполнимости или невыполнимости конечного множества дизъюнктов.

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

Рис. 1

Второй этап состоит в том, что каждому узлу N дерева сопоставляется некоторый дизъюнкт с. Этот дизъюнкт будет зависеть од дизъюнктов с₁ и с_2, которые уже сопоставлены двум узлам, следующим за N. Две соответствующие дуги помечены двумя противоположными литерами, скажем и . Если один из дизъюнктов, например с₁ не содержит ни , ни её отрицание, то можно выбрать с= с₁, в противном случае с будет резольвентой для с₁ и с₂ по отношению к . Этот результат, полученный для множества S, иллюстрируется рисунком 2.

Рис. 2

Заметим, что каждый узел помечен дизъюнктом, при котором ложна частичная интерпретация, соответствующая этому узлу. Таким образом, корень будет помечен пустым дизъюнктом. Наконец, по построению каждый дизъюнкт является элементом S или получен из S с помощью резолюции. Число резольвент, которые надо вычислить для установления невыполнимости множества дизъюнктов S, не больше числа невисячих узлов семантического дерева. Максимальное значение этой величины равно , где n-число различных высказываний, входящих в S. Тем самым показано, что резолюция неэффективна, если применяется только что описанная простая стратегия. Отметим, что некоторые стратегии выбора приводят к лучшим реализациям.

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

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

Приложения и примеры использования метода резолюций

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

Резолюция - ещё и такой механизм, который служит основой для осуществления инструкций на языке Пролог.

В качестве примера установим Общезначимость одного расхожего метода доказательства, называемого доказательством разбором случаев. Обозначим гипотезу через h, где возможны два случая - через p и q, а заключение - через c. Требуется доказать: . Это сводится к доказательству невыполнимости множества . Тогда множество дизъюнктов, невыполнимость которого следует установить, таково: .

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

1. гипотеза

2. гипотеза

3. гипотеза

4. гипотеза

5. отрицание заключения

6. резольвента для 1 и 2

7. резольвента для 3 и 5

8. резольвента для 4 и 5

9. резольвента для 6 и 7

10. ? резольвента для 8 и 9

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

Рис. 3

Правило согласия (в оригинале - consensus(лат.)) двойственно правилу резолюций. Если его применить к конъюнкциям и , то получим конъюнкцию . Эта операция была введена в рамках булевой алгебры применительно к синтезу логических схем. Она позволяет выявлять Общезначимость ДНФ (Дизъюнктивной Нормальной Формы).

Метод резолюций в логике предикатов

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

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

Например, множество унифицируемо, так как подстановка является его унификатором.

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

Пусть даны и . Эти два множества не тождественны. Рассогласование в том, что встречается в , а переменная в . Чтобы отождествить и , мы сперва должны найти рассогласование, а затем попытаться его исключить. Для и рассогласование будет . Так как - переменная, то можно заменить на , и таким образом рассогласование будет исключено. В это и заключается идея, на которой и основан алгоритм унификации.

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

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

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

Шаг 1. Множество и .

Шаг 2. Если - единичный дизъюнкт, то остановка - наиболее общий унификатор для . В противном случае найдём множество рассогласований для .

Шаг 3. Если существуют такие элементы и в , что - переменная, не входящая в , то перейти к шагу 4. В противном случае остановка: не унифицируемо.

Шаг 4. Пусть и . (Заметим, что =.)

Шаг 5. Присвоить значение и перейти к шагу 2.

Пример 1. Найти наиболее общий унификатор для

1. и . Так как - не единичный дизъюнкт, то не является наиболее общим унификатором для .

2. Множество рассогласований . В существует переменная , которая не встречается в .

3. Пусть

=

=.

4. - не единичный дизъюнкт, так как нашли множество рассогласований

для :

5. Из мы найдём, что и

6. Пусть

=

=.

7. - не единичный дизъюнкт, так как мы нашли множество рассогласований для : . Из мы найдём, что и .

8. Пусть

,

=

=

=.

9. Так как - единичный дизъюнкт, то есть наиболее общий унификатор для .

Пример 2. Определить, унифицируемо ли множество

1. Пусть и .

2. - не единичный дизъюнкт, так как мы нашли множество рассогласований для : . Из мы знаем, что и .

3. Пусть

=.

4. - не единичный дизъюнкт, так как мы нашли множество рассогласований для : .

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

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

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

Теорема унификации. Если - конечное непустое унифицируемое множество выражений, то алгоритм унификации будет всегда кончать работу на шаге 2 и последнее будет наиболее общим унификатором для .

Доказательство. Так как унифицируемо, то обозначим любой его унификатор. Индукцией по покажем, что существует такая подстановка , что . Пусть , положим . Тогда , так как . Предположим теперь, что имеет место для . Если - единичный дизъюнкт, то алгоритм унификации остановится на шаге 2. Так как , то будет наиболее общим унификатором для . Если - не единичный дизъюнкт, то алгоритм унификации будет находить множество рассогласований для . Так как - унификатор для , то должно унифицировать . Однако так как - множество рассогласований, то в должна существовать переменная. Пусть - любой другой элемент, отличный от . Тогда, так как унифицирует , то . Затем, если встречается в , то встречается в . Однако, это невозможно, так и различны, и . Следовательно, не встречается в . Поэтому алгоритм унификации не остановится на шаге 3, а перейдёт к шагу 4 - к множеству . Пусть . Тогда, так как не встречается в , то .

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

=

=

=

= .

Значит = . Следовательно,

.

Поэтому для всех существует такая подстановка , что . Так как алгоритм унификации должен кончить работу и так как он не окончился на шаге 3, то он должен окончиться на шаге 2. Кроме того, так как для всех , то последнее

будет наиболее общим унификатором для , что и требовалось доказать.

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

Если две или более литер (с одинаковым знаком дизъюнкта) дизъюнкта имеют наиболее общий унификатор , то называется склейкой . Если - единичный дизъюнкт, то склейка называется единичной склейкой.

Например, пусть . Тогда первая и вторая литеры имеют наиболее общий унификатор . Следовательно, есть склейка .

Если и - два дизъюнкта (дизъюнкты - посылки), которые не имеют никаких общих переменных. Пусть и - две литера в и соответственно. Если и имеют наиболее общий унификатор , то дизъюнкт называется (бинарной) резольвентой и . Литеры и называют отрезаемыми литерами.

Пример 1. Пусть и . Так как входит в и , то мы заменим переменную в и пусть . Выбираем и . Так как , то и имеют наиболее общий унификатор . Следовательно,

=

= .

Таким образом, - бинарная резольвента и . и - отрезаемые литеры.

Резольвентой дизъюнктов - посылок и является одна из следующих резольвент:

1) бинарная резольвента и ;

2) бинарная резольвента и склейки ;

3) бинарная резольвента и склейки ;

4) бинарная резольвента склейки и склейки .

Пример 2. Пусть и . Склейка есть . Бинарная резольвента и есть . Следовательно есть резольвента и .

Правило резолюций есть правило вывода, которое порождает резольвенты для множества дизъюнктов. Это правило было введено в 1965 году Робинсоном. Метод резолюций полон, то есть при помощи правила резолюций для любого невыполнимого множества дизъюнктов можно породить пустой дизъюнкт ?. Рассмотрим один пример из планиметрии.

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

Чтобы доказать эту теорему, мы сперва аксиоматизируем её. Пусть обозначает, что - трапеция с верхней левой вершиной , верхней правой вершиной , нижней правой вершиной и нижней левой вершиной .

Пусть обозначает, что отрезок параллелен отрезку , и пусть

означает, что угол равен углу . Тогда мы имеем следующие аксиомы:

определение трапеции,

[ внутренние накрест ] лежащие углы для параллельных линий равны, дана на рис.

Из этих аксиом мы должны уметь вывести, что истинно, то есть

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

{ }.

Эта стандартная форма есть множество из четырёх дизъюнктов. Теперь методом резолюций докажем, что множество невыполнимо:

(1) дизъюнкт в ,

(2) дизъюнкт в ,

(3) дизъюнкт в ,

(4) дизъюнкт в ,

(5) резольвента (2) и (4),

(6) резольвента (1) и (5),

(7) ? резольвента (3) и (6).

Так как последний выведенный из дизъюнкт пустой, то мы заключаем, что невыполнимо.

Стратегии метода резолюций

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

Стратегия насыщения уровней. Наиболее простой с идейной точки зрения способ выбора дизъюнктов для получения резольвенты состоит в организации полного перебора возможных вариантов. Этот перебор можно организовать следующим образом. Пусть S₀=S - исходное множество дизъюнктов. Будем считать, что S₀ упорядочено. Пусть D₂ пробегает по порядку множество дизъюнктов S₀, начиная со второго. В качестве D₁ берем последовательно дизъюнкты из S₀, предшествующие D₂ начиная с первого, и формируем последовательность S₁, состоящее из всевозможных резольвент дизъюнктов D₁ и D₂. (Порядок на S₀ определяется порядком добавления дизъюнктов в S₁.) Предположим, что получены последовательности дизъюнктов S₀, S₁,…,S_n-1 и n>1. Тогда последовательность S_n получается следующим образом. В качестве D₂ берутся по порядку дизъюнкты из S_n-1, а в качестве D₁ - дизъюнкты из S₀S₁…S_n-1, предшествующие D₂. Последовательность S_n будет состоять из всевозможных резольвент дизъюнктов D₁ и D₂. Процесс порождения резольвент прекращается, как только получается пустой дизъюнкт. Описанная стратегия называется стратегией насыщения уровней. (Уровни - это последовательности S₀, S₁,…,S_n,…) Проследим, как она работает на примере множества дизъюнктов S={XY, ШXЪШY, XZ, ШXЪZ, ШZ}:

S₀: (1) XY, S₂: (13) XY из (1) и (6),

(2) , (14) из (2) и (6),

(3) XZ, (15) XY из (1) и (7),

(4) Z, (16) из (2) и (7),

(5) , (17) XZ из (3) и (7),

S₁: (6) Y из (1) и (2), (18) Z из (4) и (7),

(7) X из (1) и (2), (19) XZ из (1) и (8),

(8) Z из (2) и (3), (20) Z из (6) и (8),

(9) YZ из (1) и (3), (21) Z из (2) и (9),

(10) Z из (3) и (4), (22) YZ из (6) и (9),

(11) X из (3) и (5), (23) Z из (8) и (9),

(12) из (4) и (5), (24) ? из (5) и (10).

Мы видим, что порождено много лишних дизъюнктов. Так, (6) и (7)-тождественно истинные дизъюнкты. Удаление или добавление тождественно истинного дизъюнкта не влияет на выполнимость множества дизъюнктов, поэтому такие дизъюнкты должны быть удалены из вывода. Далее, некоторые дизъюнкты порождаются неоднократно, например, XY, ШXШY, YZ. Это означает, что выбором дизъюнктов для получения резольвенты надо управлять.

Стратегия предпочтения (более коротких дизъюнктов). Эта стратегия является следующей модификацией предыдущей: сначала в качестве D₂ берется самый короткий дизъюнкт из S_n-1 (если таких несколько, то они перебираются по порядку), затем более длинные и т.д. Аналогичные условия налагаются и на D₁. Такая стратегия в применении к тому же множеству дизъюнктов S дает следующее:

S0: (1) XY, S2: (13) из (2) и (6),

(2) , (14) Z из (2) и (6),

(3) XZ, (15) Y из (1) и (7),

(4) Z, (16) Z из (3) и (7),

(5) (17) ? из (6) и (7).

S1: (6) X из (3) и (5),

(7) из (4) и (5)

(8) Y из (1) и (2),

(9) X из (1) и (2),

(10) Z из (2) и (3),

(11) YZ из (1) и (4),

(12) Z из (3) и (4),

Вывод оказался короче, чем в предыдущем примере, но по-прежнему содержит повторяющиеся и тождественно истинные дизъюнкты. Свободным от этих недостатков является вывод, полученный в соответствие со следующей стратегией.

Стратегия вычеркивания.

Дизъюнкт D называется расширением дизъюнкта C, если существует подстановка у такая, что у(C)D. Для логики высказываний это означает, что просто D=CD (при некоторой перестановке литералов). В случае логики предикатов ситуация не столь проста. Например, D=Q(a)P(b,y)R(u) есть расширение дизъюнкта C=P(x,y)Q(z)Q(v).

Стратегия вычеркивания, как и стратегия предпочтения является модификацией стратегии насыщения уровней. Она применяется следующим образом: после того, как получена очередная резольвента D дизъюнктов D₁ и D₂ проверяется, является ли она тождественно истинной формулой или расширением некоторого дизъюнкта C из S₀...S_n-1, и в случае положительного ответа D вычеркивается, т.е. не заносится в последовательность S_n.

Применение стратегии к прежнему множеству дизъюнктов дает следующее:

S0: (1) XY,

(2) ,

(3) XZ,

(4) Z,

(5),

S1: (6) Z из (2) и (3),

(7) YZ из (1) и (4),

(8) Z из (3) и (4),

(9) X из (3) и (5),

(10) из (4) и (5),

(11) из (5) и (6),

(12) Y из (5) и (7),

(13) ? из (5) и (8).

Рассмотренные стратегии являются полными в том смысле, что если множество дизъюнктов S невыполнимо, то из S пользуясь стратегией можно вывести пустой дизъюнкт. Для первых двух стратегий это достаточно очевидно. Полнота стратегии вычеркивания следует из того, что если D и C-дизъюнкты из S и D - расширение C, то множество S невыполнимо в том и только в том случае, когда невыполнимо множество S\{D}.

Примеры использования метода резолюций

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

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

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

Р: предварительные процентные ставки растут;

S: курс акций падает;

U: большинство людей несчастны.

Тогда имеем четыре утверждения:

(1') PS,

(2') SU,

(3') P,

(4') U.

Чтобы показать, что (4') следует из (1'), (2') и (3') мы сперва преобразуем все утверждения в стандартную форму. Таким образом, имеем

(1) ,

(2) ,

(3) P,

(4) U.

Докажем путём опровержения, что U - логическое следствие из (1), (2) и (3). Отрицаем (4) и получаем следующее доказательство:

(1) ,

(2) ,

(3) P,

(4) отрицание заключения,

(5) S резольвента (3) и (1),

(6) U резольвента (5) и (2),

(7) ? резольвента (6) и (4).

Пример 2.Допустим, что если конгресс отказывается принять новые законы, то забастовка не будет окончена, если только она не длится более года и президент фирмы не уходит в отставку. Закончится ли забастовка, если конгресс отказывается действовать, и забастовка только что началась?

Преобразуем утверждения в формулы:

Р: конгресс отказывается действовать;

Q: забастовка оканчивается;

R: президент фирмы уходит в отставку;

S: забастовка длится более года.

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

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

- конгресс отказывается действовать.

- забастовка только что началась.

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

,

(3) P из ,

(4) из ,

(5) Q отрицание заключения,

Использую резолюцию, мы получим следующее доказательство:

(6) резольвента (3) и (2),

(7) S резольвента (6) и (5),

(8) ? резольвента (7) и (4).

Пример 3. Рассмотрим следующее множество формул:

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

,

,

из .

Это множество дизъюнктов невыполнимо. Это можно доказать с помощью методе резолюций следующим образом:

(6) резольвента (3) и (2),

(7) резольвента (5) и (4),

(8) ? резольвента (7) и (6).

Таким образом, G - логическое следствие и .

Пример 4. Некоторые пациенты любят своих докторов. Ни один пациент не любит знахаря. Следовательно, никакой доктор не является знахарем. Обозначим:

P(x): x - пациент,

D(x): x - доктор,

Q(x): x - знахарь,

L(x, y): x любит y.

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

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

(3) из ,

.

Используя метод резолюций, получим следующее доказательство:

(6) резольвента (4) и (2),

(7) резольвента (3) и (1),

(8) резольвента (5) и (7),

(9) ? резольвента (6) и (8).

Метод резолюций совершенно естествен. Попытаемся перевести предыдущее доказательство на русский язык:

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

(b) Предположим, что заключение неверно, то есть предположим, что - одновременно и доктор и знахарь(дизъюнкты (4) и (5)).

(c) Так как пациент любит каждого доктора, то любит(дизъюнкт (6)).

(d) Так как - пациент, то не любит никакого знахаря (дизъюнкт (7)).

(e) Однако -знахарь, значит не любит (дизъюнкт (8)).

(f) Это невозможно из-за (с). Таким образом, мы закончили доказательство.

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

Заключение. Некоторые из таможенников способствовали провозу наркотиков.

Пусть Е(х) означает «х въезжал в страну», V(x) означает «х был высокопоставленным лицом», S(x,y) означает «у обыскивал х», С(х) означает «х был таможенником», Р(х) означает «х способствовал провозу наркотиков».

Посылки представятся следующими формулами:

а заключение - формулой

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

(1)

(2)

(3) Р(а),

(4) Е(а),

(5) ,

(6)

Отрицание заключения

(7)

Доказательство методом резолюций выглядит следующим образом:

(8) из (3) и (6),

(9) из (2) и (4),

(10) из (8) и (9),

(11) из (1) и (4),

(12) из (8) и (11),

(13) из (12) и (5),

(14) из (13) и (7),

(15) ? из (10) и (14).

Заключение доказано.

Пример 6. Посылка такая: каждый, кто хранит деньги, получает проценты. Заключение: если не существует процентов, то никто не хранит денег. Пусть S(x, y), M(x), I(x) и E(x, y) означают «х хранит деньги у», «х есть деньги», «х есть проценты» и «х получает у» соответственно. Тогда посылка записывается в виде:

а заключение - в виде

Переводя посылку в дизъюнкты, имеем:

(1)

(2)

Отрицание заключения:

(3) ,

(4) ,

(5) .

Дальнейшее доказательство на самом деле очень просто:

(6) из (3) и (1),

(7) из (6) и (4),

(8) ? из (7) и (5).

Таким образом, заключение доказано.

Пример 7. Посылка: студенты суть граждане. Заключение: голоса студентов суть голоса граждан.

Пусть S(x), C(x) и V(x, y) означают «х - студент», «х - гражданин» и «х есть голос у» соответственно. Тогда посылка и заключение запишутся следующим образом:

(посылка),

(заключение).

Стандартная форма посылки есть:

(1)

Так как

= =

=

Имеем три дизъюнкта для отрицания заключения:

(2) ,

(3) ,

(4)

Доказательство заканчивается следующим образом:

(5) из (1) и (2),

(6) из (5) и (4),

(7) ? из (6) и (3).

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

Заключение

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

Список используемой литературы

1. Чень Ч.,Ли Р. Математическая логика и автоматическое доказательство теорем, Наука, 1983.

2. Тей А.,Грибомон П.,Луи Ж. Логический подход к искусственному интеллекту. От классической логики к логическому программированию (Пермяков П.П., Гаврилов Г.П.), Мир, 1990.

3. Игошин В.И. Математическая логика и теория алгоритмов: учеб. пособие для студ. высш. учеб. заведений / В.И. Игошин. 2-е изд., стер. М.: Издательский центр «Академия», 2008.

4. Робинсон. Машинно-ориентированная логика, основанная на принципе резолюций // Кибернетический сборник, 1970, вып.7.

5. http://pgap.chat.ru/zap/zap13.htm#0.

6. http://www.intuit.ru/department/pl/plprolog/.

7. http://it.kgsu.ru/Prolog/.

Размещено на Allbest.ru

...