ФАКУЛЬТАТИВНЫЙ КУРС "СИСТЕМА АВТОМАТИЗАЦИИ ПРОЦЕССА РЕШЕНИЯ ЗАДАЧ" Часть 1. Элементы математической логики

Дмитриева Марина Валерьевна Павлова Марианна Владимировна

ФАКУЛЬТАТИВНЫЙ КУРС "СИСТЕМА АВТОМАТИЗАЦИИ ПРОЦЕССА РЕШЕНИЯ ЗАДАЧ" Часть 1. Элементы математической логики

Введение.

Математическая логика - наука о правильных математических рассуждениях, о математическом мышлении. Впервые правила рассуждений систематизировал Аристотель. Однако как наука математическая лотка сложилась лишь в середине XIX века, когда Джордж Буль ввел логические связки и исчисление высказываний. Современная математическая логика изучает: а) структуру математических высказываний, б) исходные постулаты математики (аксиомы и правила вывода), в) математические доказательства (выводы), г) истинные математические утверждения (теоремы, леммы).

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

В данной работе описывается система, позволяющая автоматически находить решения для определенного класса задач. Теоретическая база, на которую опирается система, это в основном работа [4], полезны также книги [1,2,3,8,9]. При описании системы поиска доказательств было решено выделить и описать отдельно три независимые части. В первой части приводятся основные понятия математической логики: формулы исчисления высказываний, равнозначность формул, построение конъюнктивно - нормальной формы. Вводится понятие логического следствия и формулируются теоремы о логическом следствии. Вторая часть посвящена проблеме форматизации процесса доказательства. Вводится понятие резольвенты. Описывается метод резолюций. Приводятся и обосновываются правила сокращения множества дизъюнктов. Третья часть содержит общее описание системы и несколько примеров ее использования. Все определения, теоремы и методы иллюстрируются различными примерами.

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

Данная работа выполнена при поддержке Федеральной целевой программы "Государственная поддержка интеграции высшего образования и фундаментальной науки на 1997-2000 г.г."

Основные определения и обозначения.

В обычной жизни человек принимает решения в зависимости от конкретной ситуации. Предположим, что нам известны некоторые факты (или ранее уже доказанные утверждения) Б), р2,.. Рп и, предположим, что нас интересует, следует ли некоторое утверждение О из утверждений Р|, р2,.. Рп. Утверждение, что в логически следует из утверждений Р], Б^,» Рп называют теоремой, а рассуждения, позволяющие установить, что теорема верна, называют доказательством этой теоремы.

Математическая логика и автоматические методы доказательства теорем являются наиболее бурно развивающимися областями искусственного интеллекта. Сложность поиска доказательства зависит от того, какие средства используются для задания утверждений Р1, р2,.. Рп и й. В представленной работе для описания утверждений будут использоваться формулы исчислений высказываний [3,8,9]. Каждое высказывание либо истинно, либо ложно. Можно строить составные высказывания, используя логические связки: отрицание (~), конъюнкцию (&), дизъюнкцию (V), импликацию (=>) и эквивалентность (о). Логические константы "истина" и "ложь" будем обозначать буквами "И" и "Л" соответственно.

Унарная связка ~ меняет значение высказывания на противоположное.

Ниже приводится таблица истинности для рассматриваемых бинарных логических связок.

А в А&В AvB А=>В А«В

И и И И И И

И л Л и Л Л

Л и Л и И л

л л л л И и

В исчислении высказываний логические константы и логические переменные -¿зываются атомами и считаются простейшими логическими формулами. Кроме атомов, :гической формулой считается отрицание логической формулы, а также (Е[ФЕ2), где -логические формулы, а знак обозначает одну из бинарных логических связок. 1ругих формул в исчислении высказываний нет. Мы видим, что при построении сложных тгических формул появляется большое количество круглых скобок. Для сокращения их числа можно использовать старшинство логических связок. Самой старшей является унарная :^язка отрицание, которая выполняется в первую очередь и применяется к непосредственно следующей за ней формуле. Бинарные логические связки, приведенные выше в таблице -стинности, перечислены в ней по убыванию их старшинства. Связки одного старшинства рименяюгся в порядке их следования слева направо. Если учитывать старшинство операций, то часть скобок можно опустить. Например, формула (((р&^)=>г)=>(р&г)) может быть писана вообще без скобок р&~ц=>г=>р&г.

Если мы зададим значения всех входящих в формулу переменных, то сможем вычислить жачение всей формулы. В этом случае говорят, что мы задали интерпретацию. В исчислении высказываний каждой формуле соответствует конечное число интерпретаций. Формулы бывают •пождественно-истинными (или общезначимыми) - это формулы истинные в любой интерпретации. Тождественно-ложными (или противоречивыми) называются формулы ложные = любой интерпретации. Наконец, выполнимыми называются формулы, дня которых можно хазать интерпретацию, в которой эта формула истинна. Если две формулы имеют одинаковые значения на любых возможных интерпретациях, то говорят, что они равнозначны или эквивалентны. Равнозначность формул обозначают знаком "<-»". Обозначим знаком "" любую общезначимую формулу, и знаком "" любую противоречивую формулу. Наиболее распространенные равнозначные формулы приведем в следующей таблице.

АоВо

(А=>В) <-> ~AvB

Ау(ВуС) <-> (АуВ)уС А&(В&С) о- (А&В)&С

АуВ оВуА А&В <-> В&А

Ау

~(~А) А

А v ~А <->  А & ~А<->а

А v  <-» А А &

А v  <-»  А & Я «-»А

~(АуВ) <-» ~А &~В ~(А&В) <-> ~Av~B

Определение. Пусть даны формулы Г^ р2,— ,ГП и формула в. Говорят, что в логическое следствие формул ^ Ь^,... ,РП (или в следует из Р2,... ,ГП) тогда и только тогда, когда для всякой интерпретации I, в которой истинны утверждения Р^ Г2,... ,Рп, утверждение С также истинно. Утверждения Р|, Г2,... ,РП называют аксиомами (постулатами или посылками), утверждение С-следствием.

В качестве примеров мы будем использовать в основном задачи из книг Раймонда М.Смаллиана [5,6,7], в которых математическая логика используется при раскрытии преступлений, поиске сокровищ, выборе пути на загадочные острова и в других необычных ситуациях.

Пример. На складе совершено хищение. Подозрение пало на трех человек: А, В, и С, они были доставлены для допроса. Установлено следующее:

1. Никто, кроме А, В, С, не был замешан в деле.

2. А никогда не ходит на дело без, по крайней мере, одного соучастника.

3. С не виновен.

Виновен ли В?

Обозначим через А утверждение - "А виновен", через В - "В виновен", через С - "С виновен". Запишем утверждения 1-3 с помощью формул Р^з исчисления высказываний:

Рх: АуВУС

Р2: А=>ВуС Р3: ~С

Предполагаемый ответ - "В - виновен" обозначим через в. Проверим, является ли формула О логаческим следствием формул Р2, Рз- С помощью таблицы переберем все интерпретации и для каждой из них укажем значение каждой из формул , Р2, Р3 в этой интерпретации.

N0 А в с АуВУС ¥2: А=>ВУС Р3: ~С 0:В

1 И и и И И Л

2 И и л И И и И

3 И л и и И л

4 и л л и Л и

5 л и и и и л

6 л и л и и и И

7 л л и и и л

8 л л л л и и

Нас интересуют только те интерпретации, в которых все посылки (формулы Р], ¥2, Рз) истинны. Таких интерпретаций только две - вторая и шестая. В этих интерпретациях и значение формулы в истинно. Следовательно, формула в - логическое следствие, то есть В виновен.

Теоремы о логическом следствии.

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

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

сказав равнозначность формул А=>В и ~АуВ, а также формул А«В и (А&В)у(~А&~В), лучим то, что требуется. Некоторые часто используемые правила получили специальные -¿звания, например:

Закон двойного отрицания: —А <-> А.

Закон контрапозиции: А=>В ~В=>~А.

Законы де Моргана: ~(АуВ) <-» -А&-В и ~(А&В) <-» ~Ау~В.

Теорема 1. (о логическом следствии). Пусть даны формулы Рд, Р2,— ,РП и формула О. Тогда формула в является логическим следствием формул Р2,„. ,РП тогда и гатько тогда, когда формула Р] &Р2&...&РП=>С общезначима.

Пример. Предположим, что меня спрашивают: "А верно ли, что если вы любите Елу, то вы также любите и Маргарет?". А я отвечаю: "Если это правда, то я люблю Еву, и гели я люблю Еву, то это правда". Люблю ли я Маргарет?

Продемонстрируем решение задачи на основании теоремы 1. Пусть через Е обозначено гверждение - "Я люблю Еву", через М - "Я люблю Маргарет". Утверждение "Если вы .тюбите Еву, то вы любите Маргарет" запишется формулой: Е=>М. Утверждение: "Если это правда, то я люблю Еву, и если я люблю Еву, то это правда" запишется так: Е=>М)=>Е)&(Е=>(Е=>М)). Предположим, ответ будет "Я люблю Маргарет". Тогда по -гореме 1 формула (((Е=>М)=>Е)&(Е=>(Е=>М)) =>М) должна быть общезначимой. Проверим это, выполнив эквивалентные преобразования формул: ((Е=>М)=>Е)&(Е=>(Е=>М)) =>М ~(~(~ЕУМ)УЕ)У~(~ЕУ~Е\/М)\/М ~Е&М\/ЕУ~ЕУМ ЕУ~Е

Последняя формула общезначима, следовательно, справедливо утверждение, что "Я люблю Маргарет".

Теорема 2. (о логическом следствии). Пусть даны формулы Р^ Г2,— и формула в. Тогда формула в является логическим следствием формул Р2,... ,РП тогда и только тогда, когда формула Г^&Р2&...&ГП&~С противоречива.

Пример. Рассмотрим предьщущий пример и ответим на вопрос: "Люблю ли я Еву?". Нд основании теоремы 2 о логическом следствии нас интересует вопрос, является ли тготиворечивой формула: ((Е=>М)=>Е)&(Е=>(Е=>М)) &~Е.

Убедимся в этом, выполнив эквивалентные преобразования: ((Е=>М)=>Е)&(Е=>(Е=>М))&~Е (Е&~М)у Е) &(Е=>(Е=>М)) &~Е Е&(~М\/Е)&(~ЕУМ)& ~Е Е& ~Е

Последняя формула противоречива, следовательно, справедливо утверждение "Я тюблю Еву".

Рассмотрим еще один пример. На некотором острове, населенном рыцарями и ххецами (рыцари говорят только правду, лжецы только ложь), разнесся слух о том, что на -ем зарыты сокровища. Вы прибываете на остров и спрашиваете одного из местных жителей (Назовем его А): "Есть ли на острове золото?". В ответ на ваш вопрос А заявляет: "Сокровища на этом острове есть в том и только в том случае, если я рыцарь".

а) можно ли определить, кто такой А - рыцарь или лжец?

б) можно ли определить, есть ли сокровища на острове?

Ответим на второй вопрос. Обозначим через А утверждение "А-рыцарь", через Б -Сокровища на острове есть". Тогда высказывание жителя А "Сокровища на острове есть 5 том и только в том случае, если я рыцарь" запишется формулой: (АоБ). Тогда, если А

- рыцарь, то его высказывание истинно, если лжец - то ложно. Таким образом, наша посылка есть формула вида (А<=>( А<=>8)). Для того чтобы доказать, что утверждение 5 следствие нашей посылки, то есть сокровища на острове есть, нам достаточно на основании теоремы 2 доказать, что формула (А<=>(А<=>8))&~8 противоречива. Проверим это, перебрав все интерпретации и вычислив значения формул в каждой из них.

А 8 (Ао8) (А«=>( АоБ)) (А<=>( А<=>8))&~8

И И И И Л

И Л Л Л Л

Л и л И Л

л л и Л л

Формула (А<=>( Ао8))&~8 ложна в любой интерпретации, следовательно, она противоречива, и поэтому верно утверждение, что сокровища на острове есть.

Конъюнктивно-нормальная форма и ее построение.

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

Теорема. По любой формуле Г может быть построена эквивалентная ей формула g, находящаяся в КНФ.

Алгоритм построения формулы % поясним на примере, рассмотрев формулу £ от трех переменных. Возьмем в качестве формулы £ формулу (х=>у)<=»г. Приведем таблицу, в которой перечислим интерпретации и значение формулы в каждой из интерпретаций. Правый столбец таблицы будем использовать для построения дизъюнктов конъюнктивно-нормальной формы, соответствующей формуле.

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

N0 X У ъ (х=>у)<=>г. Дизъюнкты формулы §

1 И и и И

2 и и л л -\v~yvz

3 и л и л

4 и л л и

5 л и и и

6 л и л л xv~yvz

7 л л и и

8 л л л л хуууг

гжлючаем в дизъюнкт эту переменную, в противном случае включаем переменную с ~т*щанием. Тогда по построению в интерпретациях, в которых значение f ложно, значение

1 также ложно. В нашем случае g - конъюнкция построенных формул: (~х\/~у\/г)&(~х\/ . -г)&(х\/~у\/г)&(х\/у\/г). Формулы Г и g равнозначны и g имеет КНФ. Равнозначность

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

Заметим, что КНФ формулы f можно получить, выполняя последовательно жвивалентные преобразования формулы Г (избавляясь от логической эквивалентности, •хлликации, подтягивая логическое отрицание к атомам, применяя правила де Моргана и 1Г>тие законы). Продемонстрируем в качестве примера преобразования для формулы 1=>у)ог:

Полученная формула §1: (хуг)&(~ууг)&(~хууу~г) эквивалентна исходной формуле находится в конъюнктивно-нормальной форме и не совпадает с g. Мы видим, что для гсрмулы f построены две равнозначные ей формулы g и gl, которые различны и обе -¿лодятся в конъюнктивно-нормальной форме.

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

- на основании определения логического следствия рассмотреть все интерпретации, :- которых истинны посылки Р1-Рт, и проверить, истинно ли значение в в этих гтерпретациях;

- на основании теоремы 1 о следствии исследовать, является ли формула

- &Р2&....&РП1=>0 общезначимой;

- на основании теоремы 2 о следствии исследовать, является ли формула

- &р2&....&рт&~0 противоречивой.

Мы можем преобразовать формулу р]&р2&....&рт&~0 к КНФ, получив гавнозначную формулу 81&82&...&8П, рассматриваемую как множество дизъюнктов 51 .52,...,8п}. Как по утвержденям получать новые утверждения и строить доказательство, >(ы рассмотрим в следующей части.

Литература.

Н. Дж. Нильсон. Принципы искусственного интеллекта. М.: Радио и связь, 1985.

2 Н. Дж. Нильсон. Искусственный интеллект. Методы поиска решений. М.: Мир, 1973.

3 С.Клини. Математическая логика М.: Мир, 1973.

- Ч.Чень, Р.Ли. Математическая логика и автоматическое доказательство теорем. Наука, 1983. с Р.Смаллиан. Как же называется эта книга? М.: Мир, 1981.

Р.Смаллиан. Принцесса или тигр? М.: Мир, 1985. г Р.Смаллиан. Алиса в стране смекалки. М. Мир, 1987.

^ Н.К. Косовский. Элементы математической логики и ее применение к теории ->брекурсивных алгоритмов. Изд-во ЛГУ, 1981.

И МИ И АНТОНЫ

I !

Дмитриева Марина Валерьевна, доцент кафедры информатики Санкт-Петербургского государственного университета.

Павлова Марианна Владимировна, старший преподаватель кафедры информатики СПбГУ, преподаватель школы-лицея N9 419.