Преимущества и недостатки метода резолюций




Лабораторная работа №1. Логические модели представления знаний. Метод резолюций.

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

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

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

 

Теоретическая часть

 

Правило резолюций

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

Введем следующие определения.

Литера – либо буква, либо ее отрицание ().

Дизъюнкт – дизъюнкция литер ().

Единичный дизъюнкт - одна литера .

Контрарная пара – литера и ее отрицание ().

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

Правило резолюций. Из дизъюнктов и выводим дизъюнкт . Или другими словами, дизъюнкт является логическим следствием дизъюнктов и . Если =1 и =1, то =1.

Доказательство правила резолюций. Пусть =1 и =1. Тогда, если (F)=1, то и = 1. Если же (F)=0, то (X) должно быть равно 1, поскольку =1. Но тогда =0. Следовательно, (G)=1, так как =1. Но если (G)=1, то и = 1.

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

1. Заменим импликацию

2. Заменим отрицание по правилу де Моргана

3. Заменим отрицание по правилу де Моргана

 

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

 

Пример работы правила резолюций. Допустим, имеется следующая КНФ: .

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

1) Возьмем первые 2 дизъюнкта и сопоставим их к виду дизъюнктов правила резолюций :

Тогда, на основании правила резолюций следует, что .

2) Возьмем первый и третий дизъюнкты и сопоставим их к виду дизъюнктов правила резолюций :

Тогда, на основании правила резолюций следует, что .

3) Возьмем второй и третий дизъюнкты и сопоставим их к виду дизъюнктов правила резолюций :

Тогда, на основании правила резолюций следует, что .

 

Пример работы правила резолюций, когда формула содержит пустой дизъюнкт. Допустим, имеется следующая КНФ: .

Проведем назначение кандидатов на X, F и G.

1) Возьмем первые 2 дизъюнкта и сопоставим их к виду дизъюнктов правила резолюций :

Тогда, на основании правила резолюций следует, что .

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

Тогда, на основании правила резолюций следует, что .

 

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

 

Метод резолюций

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

Для выяснения тождественной истинности или тождественной ложности любой формулы существует 2 основных подхода:

1. Вычислять на всех наборах, что не эффективно в случае большого количества переменных, так как количество вычислений растет в арифметической прогрессии (например, для n переменных число вычислений , при этом вычисления могут быть не только простыми).

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

 

КНФ – конъюнктивная нормальная форма, представляющая собой конъюнкцию дизъюнкций. С целью упрощения, КНФ в методе резолюций будет представляться списком дизъюнктов S.

 

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

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

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

Рассмотрим работу метода резолюций. Допустим, имеется 2 дизъюнкта:

Где - литера;

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

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

Если дизъюнкты не содержат контрарных литер, то резольвенты у них не существует!

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

Допустим, была некая формула в КНФ:

Заменяем согласно правила резолюций две скобки (дизъюнкты) на , что приводит к упрощению формулы:

Допустим, что мы свели первый дизъюнкт к , а второй дизъюнкт к , то есть получили контрарную пару, что говорит о том, что КНФ равна нулю.

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

Применив правило резолюции, получится пустой дизъюнкт #.

 

Особенно удобен метод резолюций, когда логическая проблема представлена в следующем виде:

Доказать, что из посылок (формул) , следует некоторое следствие В» . Данная задача эквивалентна следующей записи .

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

1. Заменим импликацию

2. Заменим отрицание по правилу де Моргана

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

 

Алгоритм построения вывода методом резолюций :

1. Привести формулу к виду .

2. Применить правило отрицания к исходной формуле .

3. Преобразовать формулу к виду .

4. Доказываем тождественную ложность данной формулы (противоречие) .

5. Привести все формулы к КНФ.

6. Составить множество дизъюнктов S формул .

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

8. Процесс продолжается до тех пор, пока не получится пустой дизъюнкт #, либо не выведется два дизъюнкта представляющих собой контрарную пару литер (что тоже является #).

9. Если процесс заканчивается пустым дизъюнктом, то вывод обоснован.

 

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

В процессе осуществления резолютивного вывода возможны следующие ситуации:

1. Среди множества дизъюнктов нет содержащих контрарные литеры. Это означает, что формула не выводима из множества формул .

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

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

 

При построении интеллектуальных систем основанных на методе резолюций решается алгоритмическая задача «Каким образом формировать резольвенты для быстрого получения контрарной пары и до каких пор формировать резольвенты?».

 

Преимущества и недостатки метода резолюций

1. Метод резолюций легко поддается алгоритмизации. Это позволяет использовать его в логических языках.

2. Недостатком этого метода является необходимость представления формул в КНФ.

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

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

5. Применение метода резолюций в доказательстве теорем и при планировании действий.

 

Пример. Доказать методом резолюций (истинность если известно, что истинны посылки ), что эквивалентно записи .

Доказательство методом резолюций основывается на доказательстве несовместимости отрицания исходной формулы.

1. Следовательно, применяется отрицание к исходной формуле , что после преобразования эквивалентно записи .

2. Приводим формулы к КНФ:

3. Опускается знак конъюнкции, и выписываются только дизъюнкты

4. К дизъюнктам применяется правило резолюций:

4.1. Возьмем первые 2 дизъюнкта и сопоставим их к виду дизъюнктов правила резолюций :

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

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

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

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

 

Общая постановка задачи

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



Поделиться:




Поиск по сайту

©2015-2024 poisk-ru.ru
Все права принадлежать их авторам. Данный сайт не претендует на авторства, а предоставляет бесплатное использование.
Дата создания страницы: 2017-06-12 Нарушение авторских прав и Нарушение персональных данных


Поиск по сайту: