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

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

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

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

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

 

 

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

 

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

 

Дисциплина Математика

 

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

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

                                                          

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

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

 

Комиссия:      ............................/                  /

                     ............................/                  /

                     ............................/                  /

 

 

Дата защиты

Оценка

 

 

Курган 2009

 

Содержание.

Содержание ……………………………………………………………………..2

Введение…………………………………………………………………………3

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

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

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

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

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

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

Заключение……………………………………………………………………..39

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

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

Введение.

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

В октябре 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=L D_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₁ равносильна