| « Поставить закладку » « Сделать стартовой » | |||
|
|||
| « Поставить закладку » « Сделать стартовой » | |||
|
|||
|
Глава 20. Формулы исчисления высказываний.
Формулы исчисления высказываний
В предыдущих главах для самострятельной работы предлагались упражнения, которые располагались в конце каждой главы. При выполнении упражнения следовало написать сценарий решения некоторой задачи. В настоящей главе изложение материала будет изменено. Упражнение может быть предложено сразу после рассмотрения теоретического материала или примера, иллюстрирующего теорию. Кроме того, упражнения не обязательно предполагают создание сценария. Отдельно формулируется задание на создание сценария. Материал этой главы посвящен введению в один из разделов искусственного интеллекта — автоматическое доказательство теорем. В обычной жизни человек принимает решения в зависимости от конкретной ситуации. Предположим, что нам известны некоторые факты (или ранее уже доказанные утверждения) F1, F2, ..., Fn, и нас интересует, следует ли некоторое утверждение G из утверждений F1, F2, ..., Fn. Утверждение, что G логически следует из утверждений F1, F2, ..., Fn называют теоремой. Доказательство теоремы — рассуждения, позволяющие установить, что теорема верна. Математическая логика — наука о правильных математических рассуждениях, о математическом мышлении. Впервые правила рассуждений систематизировал Аристотель. Однако как наука математическая логика сложилась лишь в середине XIX века, когда Джордж Буль ввел логические связки и исчисление высказываний. Математическая логика изучает:
и многое другое. Одной из задач математической логики является формализация понятия доказательства. Для описания утверждений можно использовать формулы исчисления высказываний. Каждое высказывание либо истинно, либо ложно. Можно строить составные высказывания, используя логические связки', отрицание (~), конъюнкцию (&), дизъюнкцию (у), импликацию (=>) и эквивалентность (<=>). Логические константы "истина" и "ложь" будем обозначать буквами И и Л соответственно. Логические переменные (в математической логике их называют пропозициональные переменные) будем обозначать большими буквами латинского алфавита. Унарная связка ~ меняет значение высказывания на противоположное. В табл. 20.1 представлены результаты логических связок таблицы истинности. Таблица 20.1. Таблица истинности бинарных связок
В исчислении высказываний логические константы и логические переменные называются атомами и считаются простейшими логическими формулами. Кроме атомов логической формулой считается отрицание логической формулы, а также (F1 + F2), где F1, F2— логические формулы, а знак Ф обозначает одну из бинарных логических связок. Других формул в исчислении высказываний нет. Мы видим, что при построении сложных логических формул появляется большое количество круглых скобок. Для сокращения их числа можно использовать старшинство логических связок. Самой старшей является унарная связка "отрицание", которая выполняется в первую очередь и применяется к непосредственно следующей за ней формуле.. Бинарные логические связки, приведенные выше в таблице истинности, перечислены по убыванию их старшинства. Связки одного старшинства применяются в порядке их следования слева направо. Если учитывать старшинство операций, то часть скобок можно опустить. Например, формула ((( P & ~ Q ) => R ) => ( P & R ) может быть записана вообще без скобок: P & ~ Q => R => P & R Формулу исчисления высказываний будем называть постоянной, если она не содержит переменных. Для того чтобы вычислить значение постоянной формулы И & ~ Л => И => И & И. расставим в ней скобки и получим следующую формулу: (((И & ~ Л) => И) => (И & И)). Далее, вычисляя сначала выражения в скобках по таблице истинности, получаем
значение всей формулы — истина. 1. Вычислите значение следующих формул исчисления высказываний: • ((И => Л) => И) & (И => (И => Л)) => Л; • (И <=> (И <=> Л)) & ~ Л; • (И => (Л => И)) <=> ~ (Л & И). 2. Предположим, что мы разговорились с тремя жителями А, В и С, о каждом из которых известно, что он либо рыцарь, либо лжец. Рыцари всегда говорят правду, лжецы всегда лгут. Двое из них (А и В) высказали следующие утверждения. • А: Мы все лжецы. • В: Один из нас рыцарь. Кто из трех жителей А, В и С рыцарь и кто лжец? Запишите утверждения жителей острова с помощью формул исчисления
высказываний. Вычисление значения постоянной логической формулы Создадим сценарий, который облегчает ввод постоянных пропозициональных формул. При нажатии кнопки, соответствующей логическим константам или логическим операциям, определенная операция появляется в поле ввода так, как показано на рис. 20.1. После построения формулы и нажатия кнопки Вычислить определяется значение формулы. Напомним, что при построении логических формул в языке JavaScript разрешено использовать три логические операции: отрицание (!), логическое И (&&) и логическое ИЛИ (||). При нажатии кнопки соответствующая операция появляется в текстовом поле, причем знак операции должен быть тем, который принят в языке JavaScript. Подобная формула может быть вычислена, если подать ее в качестве параметра методу eval. Если же формула содержит знаки импликации (=>) и логической эквивалентности (<=>), то требуется провести анализ формулы и вычислить ее значение с помощью определяемых программистом функций. HTML-код документа, содержащего сценарий решения задачи, представлен в листинге 20.1.
Рис. 20.1. Построитель постоянных логических форм Листинг 20.1. Значение постоянной логической формулы ? <HTML> <HEAD> <TITLE>Значение постоянной логической формулы. (Лямов К.)</TITLE> <script> <!-— // var pos = 0; var lex; var falseSym = "false"; var trueSym — "true"; var notSym = "! "; var andSym = "&&"; var orSym = "M"; var impSym = "=>"; var equSym = "<=>"; // Вычисление значения формулы function evaluateFormula() { pos = 0; document.myForm.result.value = valFormula() } function add(str) { document.myForm.logFormula.value += str} // Выбор для анализа следующего символа function nextSym() { var t = ' ' ; while (t == ' ' && pos < document.myForm.logFormula.value.length) (t = document.myForm.logFormula.value.charAt(pos++)} return t; } // Анализ очередной лексемы function nextLex() { var tmp = nextSym(); switch (tmp) { case '&' pos++; return andSym; case '|' pos++; return orSym; case '<' pos+=2; return equSym; case '=' pos++; return impSym; case 't' pos += 3; return trueSym; case 'f pos += 4; return falseSym; default: return tmp; } } // Вычисление значения логической эквивалентности function valFormula() { var left, right; left = vallmp(); while (lex = equSym) { right = vallmp(); left = ((left) == (right)); } return left; } // Вычисление импликации function vallmp() { var left, right; left = valSimple(); while (lex == impSym) { right = valSimple(); left = (! (left) || (right)) } return left; } function valSimple{) { var s = ""; while (true) { lex = nextLex(); //alert("Lex: "+lex); switch (lex) { case trueSym: case falseSym: case andSym: case orSym: case notSym: s += lex; case ')': break; case '(': var у = eval(s + valFormula()); return y; default: return eval(s); } } //while } //valSimple //-—> </script> </HEAD> <BODY bgcolor="F8F8FF"> <Н4>Значение постоянной логической формулы</Н4> <FORM name=myForm> <textarea cols=40 rows=3 name=logFormula></textarea><br> <input type'=button value="true" onClick="add('true')"> <input type=button value="false" onClick="add('false')"> <input type=button value=" ! " onClick="add('!')"> <input type=button value=" & " ondick="add(' && ')"> <input type=button value=" v " onClick="add(' || ')"> <input type=button value="=>" onClick="add(' => ')"> <input type=button value="<=>" onClick="add(' <=> ')"> <input type=button value=" ( " onClick="add('(')"> <input type=button value=" ) " onClick="add(')')"><br><br> <input type=button value="Вычислить" onClick="evaluateFormula()"> <input type=button value="Очистить" onClick=" document.myForm.logFormula.value = ''; document.myForm.result.value = '' "><br><br> <В>Значение формулы:</B> <input type=text name=result size=5> </FORM> </BODY> </HTML> Если задать значения всем входящим в формулу переменным, то можно вычислить
результат всей формулы. В этом случае говорят, что задана интерпретация.
В исчислении высказываний каждой формуле соответствует конечное число
интерпретаций. Вычисление значения формулы в заданной интерпретации Необходимо написать сценарий вычисления значения логической формулы в заданной интерпретации. Пусть при построении формулы используются только три переменные а, b, с, значения которых указывает пользователь. Для ввода логической формулы применяется построитель формул так, как показано на рис. 20.2.
Рис. 20.2. Значение формулы
В общем случае при анализе формулы следует учесть количество различных переменных, входящих в формулу. Так как каждая переменная может принимать только два значения, то число различных интерпретаций конечно. Формулы бывают тождественно истинными (или общезначимыми) — это формулы истинные в любой интерпретации. Тождественно ложными (или противоречивыми) называются формулы, ложные в любой интерпретации. Наконец, выполнимыми называются формулы, допускающие указание интерпретации, в которой эта формула истинна. Если две формулы имеют одинаковые значения при любых возможных интерпретациях, то говорят, что они равнозначны или эквивалентны. Равнозначность формул обозначают знаком о. Обозначим знаком любую общезначимую формулу и знаком П любую противоречивую формулу. Наиболее распространенные равнозначные формулы приведены в табл. 20.2. Таблица 20.2. Равнозначные формулы
Нетрудно доказать, что любую формулу исчисления высказываний можно преобразовать к равнозначной формуле, которая содержит только три логические связки: отрицание, конъюнкцию и дизъюнкцию. Действительно доказав равнозначность формул А => В и ~А v В, а также формул A<=>B и (A & B) v (~А & ~B), получим то, что требуется. Некоторые часто используемые правила получили специальные названия, например:
Пусть заданы две формулы (A => B) => С и A => (В => С). Требуется определить, эквивалентны ли они. Для того чтобы решить задачу, мы переберем все интерпретации и в каждой из интерпретаций вычислим значение формулы. Результаты приведены в табл. 20.3. Таблица 20.3. Таблица истинности для формул (А => В)
=> С и А =* (В => С)
После вычислений видно, что значения формул не совпадают в некоторых
интерпретациях, поэтому заданные формулы неравнозначны. Напишем сценарий, который для логической формулы строит таблицу истинности. В формуле разрешено использовать операции отрицания, дизъюнкции и конъюнкции; переменные представляются буквами латинского алфавита. Вид документа представлен на рис. 20.3.
Рис. 20.3. Формирование таблицы истинности для заданной формулы Если после ввода формулы нажать кнопку Таблица истинности, то будет выведена таблица, в которой указаны все возможные интерпретации и значение формулы в каждой интерпретации. Для формулы, введенной в строку на рис. 20.3, будет сформирован следующий документ, содержащий таблицу истинности (рис. 20.4).
Рис. 20.4. Таблица истинности для заданной формулы HTML-код документа, который по заданной формуле строит таблицу истинности, приведен в листинге 20.2. Листинг 20.2. Построение таблицы истинности <HTML> <HEAD> <SCRIPT language="JavaScript" src="term.js"> </SCRIPT> </HEAD> <BODY bgcolor="F8F8FF"> <FORM name=data> <Н4>Введите формулу</Н4> <input type=text size=30 name=formula value="a&bVc&b"><br> <small><i> Moжно использовать "следующие символы: <br> snbsp;[a..u,w..z,A..U,W..Z] — односимвольные перёменные<br> ! — отрицание<br> & — логическое И<br> V — логическое ИЛИ<br> <br> <input type="button" value="Таблица истинности" onclick="TABLE()"><br> </FORM><br> </BODY> </HTML> Функция, осуществляющая построение таблицы, хранится во внешнем файле.
Содержимое файла приведем позже, а пока рекомендуется написать сценарий в
качестве упражнения. Для каждой из следующих формул определите, является ли она общезначимой, противоречивой или выполнимой:
Определение выполнимой, общезначимой и противоречивой формулы Напишем сценарий, который определяет, является ли заданная формула выполнимой, общезначимой или противоречивой. Для простоты будем считать, что в формуле используются операции отрицания, конъюнкции и дизъюнкции. При анализе формулы перебираются интерпретации. Вычисляется значение формулы в начальной интерпретации, а затем, если при переходе к следующей интерпретации значение формулы изменилось на противоположное, то она выполнима. Если же при всех интерпретациях значение формулы не изменилось, то она либо общезначима, либо противоречива. Результат выполнения сценария представлен на рис. 20.5.
Рис. 20.5. Определение типа формулы Если формула выполнима, то кроме определения типа формулы требуется построить таблицу истинности. HTML-код приведен в листинге 20.3. Листинг 20.3. Формула выполнимая, общезначимая, противоречивая <HTML> <HEAD> <script language="JavaScript" src="term.js"> </SCRIPT> </HEAD> <BODY> <FORM name=data> <b>Введите формулу </b> <input type=text size=30 name=formula value="a&bVcsb"><br> <small><i> Можно использовать следующие символы:<br> [a..u,w..z,A..U,W..Z] — односимвольные переменные<br> ! — отрицание<br> & — логическое И<br> V — логическое ИЛИ<br><br> <input type="button" value="Tnn формулы" onclick="formulaType()"><br> </FORM><br> </BODY> </HTML> Как и в предыдущем случае, функция, осуществляющая анализ формулы, хранится
во внешнем файле. При решении многих задач нас интересует, следует ли некоторое утверждение из ранее доказанных или уже известных. Мы введем понятие логического следствия и с его помощью решим некоторые задачи. Пусть даны формулы F1, F2, ..., Fn и формула G. Говорят,
что G логическое следствие формул F1, F2, ..., Fn (или G следует
из F1, F2, ..., Fn) тогда и только тогда, когда для всякой
интерпретации I, в которой истинны утверждения F1, F2, ..., Fn,
утверждение G также истинно. Утверждения F1, F2, ..., Fn называют
аксиомами (постулатами или посылками), утверждение G —
следствием. Представление утверждений формулами Предположим, что некоторый человек вас спрашивает: "А верно ли, что если вы любите Бетти, то вы также любите и Джейн?" Вы отвечаете: "Если это верно, то я люблю Бетти". Вопрос звучит так: "Любите ли вы Бетти?" Запишем утверждения формулами исчисления высказываний, обозначив через В утверждение "Я люблю Бетти", через D — "Я люблю Джейн". Тогда посылка (утверждение "Если это верно, то я люблю Бетти") запишется формулой: ((B=>D)=>B). Предполагаемый ответ (следствие) — формулой В. Переберем возможные значения переменных В и D, вычислим значения формул F и G. Полученные данные оформим в виде табл. 20.4. Таблица 20.4. Таблица истинности для формул ((В => D) => В) и В
Нас интересуют только те интерпретации, в которых формула F истинна. В
этих интерпретациях истинна и формула G. Согласно определению формула
G — логическое следствие формулы F. Таким образом, мы выяснили,
что ответ на вопрос "Люблю ли я Бетти?" — положительный. На складе совершено хищение. Подозрение пало на трех человек: А, Б и С. Они были доставлены для допроса. Установлено следующее:
Виновен ли В? Запишем приведенные утверждения с помощью формул исчисления высказываний. На основании определения логического следствия выясним, является ли ответ на вопрос логическим следствием этих трех утверждений. Обозначим через А утверждение "А виновен", через В — "В виновен", через С — "С виновен". Запишем утверждения 1—3 с помощью формул F1 - F3 исчисления высказываний:
Предполагаемый ответ — "В виновен" — обозначим через G. Проверим, является ли формула (7 логическим следствием формул F1, F2, F3. С помощью табл. 20.5 переберем интерпретации и для всех укажем значение каждой из формул F1, F2, F3 в этой интерпретации. Таблица 20.5, Таблица интерпретаций для формул F1, F2, F3
Как и в предыдущем примере, нас интересуют только те интерпретации, в которых
все посылки (формулы F, FI, /3) истинны. Таких интерпретаций только две
— вторая и шестая. В этих интерпретациях и значение формулы G истинно.
Следовательно, формула G— логическое следствие, т. е. обви-. няемый В
виновен. На этот раз на допрос были вызваны четыре подозреваемых: А, В, С, D. Было доказано, что, по крайней мере, один из них виновен и никто кроме А, В, С, D в ограблении не участвовал. Кроме того, удалось установить следующее.
Кто же из подозреваемых граждан виновен? Докажите это, воспользовавшись
понятием логического следствия. Теоремы о логическом следствии Теоремы о логическом следствии позволяют решение вопроса о том, является одно утверждение следствием других, свести к анализу общезначимости или противоречивости некоторой формулы. Теорема 1 Пусть даны формулы F1, F2, ..., Fn и формула G. Тогда формула G является логическим следствием формул F1, F2, ..., Fn тогда и только тогда, когда формула F1 & F2 & ... & Fn => G общезначима. Доказательство. Предположим, что G— логическое следствие. Возьмем произвольную интерпретацию I. Формула F1 & F2 & ... & Fn может быть либо истинной, либо ложной в этой интерпретации. Рассмотрим сначала случай, когда эта формула истинна. Тогда истинны и все формулы Fi. Так как формула G— логическое следствие, то она истинна, если истинны посылки. Таким образом, и вся импликация F1 & F2 & ... & Fn => G истинна. Если же формула F1 & F2 & ... & Fn ложна в выбранной интерпретации, то, независимо от значения формулы G, рассматриваемая нами формула F1 & F2 & ... & Fn => G истинна. Мы выбрали произвольную интерпретацию и доказали, что исследуемая формула в ней истинна. Таким образом, если G — логическое следствие, то формула F1 & F2 & ... & Fn =>G общезначима (или тавтология). Предположим теперь, что формула F1 & F2 & ... & Fn => G общезначима. Докажем, что формула (Алогическое следствие формул F1, F2, ... ,Fn. Нас интересуют интерпретации, в которых истинны посылки. Выберем одну из них. В этой интерпретации истинна формула F1 & F2 & ... & Fn. Так как формула F1 & F2 & ... & Fn => G общезначима, то она истинна и в выбранной нами интерпретации. Тогда формула G также должна быть истинной. Теорема доказана. Теорема 2 Пусть даны формулы F1, F2, ... ,Fn и формула G. Тогда формула G является логическим следствием формул F1, F2, ... , Fn тогда и только тогда, когда формула F1 & F2 & ... & Fn & ~ G противоречива. Доказательство. Согласно теореме 1 формула G является логическим следствием тогда и только тогда, когда формула F1 & F2 & ... & Fn=> G общезначима. Формула F1 & F2 & ... & Fn => G является общезначимой тогда и только тогда, когда ее отрицание противоречиво. Выполним эквивалентные преобразования формулы ~ (F1 & F2 & ... & Fn => G). ~ (F1 & F2 & ... & Fn => G) <-> ~ (~ (F1 & F2 & ... & Fn) v G) <-> F1 & F2 & ... & Fn & ~ G. В результате преобразований получили требуемую формулу, и она противоречива.
Следовательно, теорема доказана. Пример использования теоремы 1 о логическом следствии Предположим, что вас спрашивают: "А верно ли, что если вы любите Еву, то вы также любите и Маргарет?" А вы отвечаете: "Если это правда, то я люблю Еву, и если я люблю Еву, то это правда". Любите ли вы Маргарет? Продемонстрируем решение задачи на основании теоремы 1. Пусть через Е обозначено утверждение "Я люблю Еву", через М — "Я люблю Маргарет". Утверждение "Если вы любите Еву, то вы любите Маргарет" запишется формулой: Е => М. Утверждение: "Если это правда, то вы любите Еву, и если вы любите Еву, то это правда" запишется так: ((E => М) => Е) & (Е=> (E => М)). Предположим, ответ на вопрос будет таким "Я люблю Маргарет". Тогда по теореме 1 формула ((E => М) => Е) & (Е=> (E => М)) => M должна быть общезначимой. Проверим это, выполняя эквивалентные преобразования формул: ((E => М) => Е) & (Е=> (E => М)) => M <-> ~ (((E => М) => Е) & (Е=> (E => М)).) v М<-> ~ ((E => М) => Е) v ~ (Е=> (E => М)). v М <-> (Е => М) & ~ Е v ~ (~E v ~E v М) v M <-> (~ E v M) & ~ E v ( E & ~ M ) v M <-> ~ Е & (M v ~ Е) v (E v М) & (~ M v М) <-> ~E &.(M v ~ E) v (E v M) & <-> ~ Е & (M v ~E) v (Е v М) <-> (~ E v E v M) & (M v ~ E v E v M) <-> & <->. Последняя формула общезначима, поэтому и рассматриваемая формула ((E => М) => Е) & (Е => (E => М)) => М также общезначима, и мы нашли ответ на вопрос задачи. Расследуется простое дело о хищении со склада. Преступник (или преступники) вывезли награбленное имущество на машине. Подозрение пало на трех человек А, В, С, которые были доставлены в Скотланд-Ярд для допроса. Было установлено следующее:
Виновен или не виновен А? 1. Напишите сценарий, который определяет, является ли общезначимой некоторая заданная формула. 2. Напишите сценарий, который определяет, является ли некоторая формула
следствием заданных пользователем формул, опираясь на теорему 1 о логическом
следствии. Пример использования теоремы 2 о логическом следствии Рассмотрим предыдущий пример и ответим на вопрос: "Люблю ли я Еву?" На основании теоремы 2 о логическом следствии нас интересует, является ли противоречивой формула: ((Е => М) => Е) & (Е => (Е => М)) & ~ Е. Убедимся в этом, выполняя эквивалентные преобразования формул: ((E => М) => Е) & (E => (E => М)) & ~ М <-> (~ (Е => М) v E) & (~ Ev (E => M)) & ~ M <-> (E & ~ M v E) & (~ E v M) & ~ E <-> Е & (~ М v Е) & (~ E v M) & ~ E<-> Последняя формула противоречива, следовательно, справедливо утверждение "Я
люблю Еву". На некотором острове, населенном рыцарями и лжецами (напомним, что рыцари говорят только правду, лжецы — ложь), разнесся слух о том, что на нем зарыты сокровища. Вы прибываете на остров и спрашиваете одного из местных жителей (назовем его А), есть ли на острове золото. В ответ на ваш вопрос А заявляет: "Сокровища на этом острове есть в том и только том случае, если я рыцарь". Можно ли определить:
Ответим на второй вопрос. Обозначим через А утверждение "А — рыцарь", через L — "Сокровища на острове есть". Тогда высказывание жителя А "Сокровища на острове есть в том и только том случае, если я рыцарь" запишется формулой: (A <=> L). Если А — рыцарь, то его высказывание истинно; если лжец, то ложно, таким образом, наша посылка — формула вида (А <=> (А <=> L)). Для того чтобы доказать, что утверждение L — следствие нашей посылки, т. е. сокровища на острове есть, нам достаточно на основании теоремы 2 доказать, что формула (А <=> (А <=> L)) & ~ L противоречива. Проверим это, перебрав все интерпретации и вычислив значение формул в каждой из них. В табл. 20.6 приведены значения формул во всех интерпретациях. Таблица 20.6. Таблица истинности для формулы (А <=> (А <=> L)) & ~ L
Формула (А <=> (А <=> L)) & ~ L ложна в любой интерпретации, следовательно, она противоречива, и поэтому
верно утверждение, что сокровища на острове есть; По обвинению в ограблении перед судом предстали А, В и С. Установлено следующее:
Этих данных недостаточно, чтобы доказать виновность каждого из трех подсудимых в отдельности, но эти данные позволяют отобрать двух подсудимых, о которых известно, что один из них заведомо виновен. Определите и докажите, о каких подсудимых идет речь. Мы видим, что если задача такова, что ее посылки (постулаты) и следствие записываются формулами исчисления высказываний, то решить задачу можно одним из следующих способов: 1. На основании определения логического следствия рассмотреть все интерпретации, в которых истинна формула F1 & F2 & .... & Fn, и проверить значение формулы G. 2. На основании теоремы 1 проверить, является ли общезначимой формула F1 & F2 & .... & Fn => G. 3. На основании теоремы 2 проверить, является ли противоречивой формула F1
& F2 & .... & Fn &~ G. Конъюнктивная нормальная форма и ее построение Во многих случаях удобно рассматривать формулы специального вида или, как говорят, формулы в канонической форме. В математической логике и в теории автоматического доказательства теорем рассматриваются формулы в конъюнктивной нормальной форме. Литералом называется атом или отрицание атома. Дизъюнктом называется литерал или дизъюнкция литералов. Формула находится в конъюнктивной нормальной форме (КНФ), если она представляет собой либо дизъюнкт, либо является конъюнкцией дизъюнктов. Элементарной конъюнкцией называется конъюнкция литералов. Дизъюнктивной нормальной формой называется дизъюнкция элементарных
конъюнкций. По любой формуле F может быть построена эквивалентная ей формула G, находящаяся в КНФ. Доказательство. Идею доказательства теоремы и построения КНФ поясним на примере формулы Fот трех переменных. Возьмем следующую формулу F: (X => Y)<=> Z Приведем табл. 20.7, в которой перечислим интерпретации и значение формулы в каждой из интерпретаций. Правый столбец таблицы будем использовать для построения дизъюнктов конъюнктивной нормальной формы, соответствующей формуле. Таблица 20.7. Построение конъюнктивной нормальной формы
Выделим те интерпретации, в которых формула принимает значение "ложь", и для этих интерпретаций построим дизъюнкт по правилу: если значение переменной — "ложь", то включаем в дизъюнкт эту переменную, в противном случае включаем переменную с отрицанием. Тогда по построению в интерпретациях, в которых значение / ложно, значение G также ложно. В нашем случае формула G является конъюнкцией построенных формул: (~ X v ~ Y v Z) & (~ X v Y v ~ Z) & (X v ~ Y v Z) & (X v Y v Z}. Формулы F и G эквивалентны и G имеет КНФ.
Эквивалентность формул можно доказать в качестве упражнения. Преобразуйте следующие формулы в конъюнктивную нормальную форму:
Построение формулы в конъюнктивной нормальной форме Напишем сценарий, который на основании рассмотренной теоремы по произвольной формуле строит эквивалентную формулу, находящуюся в КНФ. В текстовое поле вводится формула, после щелчка по кнопке, формируется эквивалентная формула, находящаяся в КНФ. Один из тестов продемонстрирован на рис 20.7. При построении КНФ перебираются все интерпретации, исследуется значение
формулы в текущей интерпретации, и, если значение ложно, то соответствующая
формула добавляется в строку результата. Вместе с формулой в конъюнктивной
нормальной форме выдается таблица истинности так, как показано на рис.
20.8.
Три функции (построение таблицы истинности, анализ типа формулы и построение КНФ) хранятся во внешнем файле. Приведем содержимое HTML-документа, содержащего требуемые функции (листинг 20.4). Листинг 20.4. Конъюктивеая нормальная форма // Функции построения таблицы истинности и КНФ. Korostelyov Andrey var srcStr = ""; // Исходная строка var let = new Array(); // Массив значений переменных формулы var letName = new Array(); // Массив имен переменных var resStr = ""; // Строка результата var TABLEStr = ""; // Строка формирования элементов таблицы var knfStr = null; // Формула в КНФ var trueVal =0; // Формула общезначима == TRUE var falseVal =0; // Формула противоречива == FALSE // Формирование заголовка документа и таблицы function init() { srcStr=document.data.formula.value; parseLine (srcStr); document.writeln("<u>Исходная формула:</u> "+srcStr+"<br><br>"); TABLEStr += "<u>Таблица истинности</u>n<ТАВЬЕ border=l cellpadding=3>n"+ "<TR bgcolor=#cccccc>n"; for(i=0; i<letName.length; i++) { TABLEStr += "t<TD><b>"+letName[i]+!'</b></TD>n"} TABLEStr += "<TD align=center><b>значение</b></TD>n</TR>n"; prepareTABLE(let, 0); TABLEStr += "</TABLE>"; } // Формирование строки таблицы function parseLine(str) { var cur; var k=0; for(i=0; i<str.length; i++){ cur = str.charAt(i); if(cur=="="||cur=="!"||cur=="("||cur==")") ( resStr+=cur} else if (cur=="&") { resStr+="&&"} else if (cur=="v"||cur=="V") { resStr+="||"} else { var elemlndex = indexOfElement(letName, cur); if(elemlndex==-l) { elemlndex = k let[k] = true; letName [k]=cur; k++; } resStr+="lettr["+elemlndex+"]"; } } } // Возврат индекса найденного элемента или -1, если элемента нет function indexOfElement(arr, element) { for(var l=0; Karr.length; l++) { if (arr[l]==element ) { return l } } return -1; } // Формирование строки таблицы значений function prepareTABLE(lettr, pos) { var resStrVal; var tmpLettr; // pos — номер деременной //j==0 - true //j==l - false for(var j=0; j<2; j++) { if((pos!=0 && j!=0)|I(pos==0)) { TABLEStr += "<TR>n"; for(i=0; Klettr.length; i++) { if (lettr[i]!=false){ tmpLettr="<font color=#555555>"+lettr[i]+"</font>" } else {tmpLettr=lettr[i]} TABLEStr += "t<TD>"+tmpLettr+"</TD>n"; } resStrVal = eval(resStr); if (resStrVal!=false) { resStrVal="<font color=#555555>"+resStrVal+"</font>" } TABLEStr += "t<TD align=center><b>"+resStrVal+"</b></TD>n"; TABLEStr += "</TR>n"; if(resStrVal){ trueVal++; } else { falseVal++; if (knfStr != null){prepareKNF(lettr)} } } if(pos<lettr.length-l) { prepareTABLE(lettr, pos+1)} lettr[pos]=false; } lettr[pos]=true; } // Построение конъюнктивной нормальной формы function prepareKNF(lettr) { if (knfStr != ""){ knfStr += "&"; } knfStr += "("; for(i=0; Klettr.length; i++) { if (lettr[i]) { knfStr += "!"+ letName[i] + "|"; } else { knfStr += letName [i] + "|"; } } knfStr = knfStr.substring(0, knfStr.length-1)+")"; } // Формирование ссылки перехода к основному документу function docFooter() ( document.writeln("<br><A href=index.HTML>Boзвpaт</A>")} // Вывод таблицы function TABLE() { init(); document.writeln(TABLEStr); docFooter(); } // КНФ function knf() { knfStr = ""; init (); if (knfStr==""){knfStr = "Отсутствует"} knfStr = "<u>Конъюнктивно-нормальная форма:</u> <BR>n" + knfStr+"<br>"; document.writeln(knfStr+"<br>"); document.writeln(TABLEStr); docFooter(); } // Определение типа формулы function formulaType() { init(); document.writeln("<u>Формула является:</u><br>n"); if (trueVal==0) { document.writeln("Противоречивой<br><br>") } else if (falseVal==0) { document.writeln("Общезначимой<br><br>")} else ( document.writeln{"Выполнимой<br><br>"); document.writeln(TABLEStr); } docFooter() ; } Один из способов построения формулы в КНФ мы уже продемонстрировали. Заметим, что КНФ G формулы F можно получить, выполняя последовательно эквивалентные преобразования формулы F. Алгоритм преобразования может быть таким: 1. Сначала следует исключить из формулы знаки логической эквивалентности и импликации, применяя последовательно правила эквивалентности: • А <=> В <-> (~ A v B) & (~ В v А) • (А => B)<-> ~ A v В 2. Затем необходимо подтянуть логическое отрицание к атомам, используя правило ~ (~ F) <-> F, и применяя правила де Моргана: • ~ (A v B) <-> ~ A & ~ B • ~ (A & B) <-> ~ A v ~ B 3. Потом применить несколько раз дистрибутивные законы: • A v (В & С) <-> (А & В) v (А & С) • А & (В v С) <-> (А & В) v (А & С) Продемонстрируем в качестве примера те преобразования, которые необходимо выполнить, чтобы построить КНФ для рассмотренной нами ранее формулы (Х=> Y) <=> Z:
Полученная формула G1 (X v Z) & (~ Y v Z) & (~ X v Y v ~ Z) эквивалентна исходной формуле F, находится в конъюнктивной нормальной
форме и не совпадает с G. 1. Преобразуйте следующие формулы в конъюнктивную нормальную форму:
2. Преобразуйте следующие формулы в дизъюнктивную нормальную форму:
Нетрудно доказать, что произвольная пропозициональная формула эквивалентна
дизъюнкции элементарных конъюнкций, соответствующих тем интерпретациям, при
которых данная формула истинна. Автоматизация ввода логических формул Необходимо создать сценарий, который облегчает ввод логических формул. При
нажатии кнопок, сопоставленных переменным, скобкам или логическим операциям,
соответствующая операция появляется в поле ввода. После формирования формулы в
текстовом поле при щелчке по кнопке вычисляется таблица истинности, определяется
тип формулы, строится соответствующая формуле конъюнктивная или дизъюнктивная
нормальные формы так, как показано на рис. 20.8.
Полностью написать сценарий с помощью уже описанных функций предлагается в качестве упражнения. В последних рассмотренных примерах использовались три логические операции.
Это облегчало написание алгоритмов анализа формулы, т. к. позволяло для
вычисления значения формулы воспользоваться функцией evai. Рассмотреть варианты
решения предложенных задач в случае, когда в формуле используются импликация и
эквивалентность, читателю предлагается самостоятельно. Теперь нам надо показать, как из уже имеющихся знаний можно извлекать новые утверждения. Введем правило резолюции, согласно которому из двух рассуждений можно вывести третье. Литерал L1 образует контрарную пару с литералом L2, если L1 = ~ L2. Пусть С1 и C2 — два дизъюнкта. Литерал L1 из дизъюнкта C1, литерал L2 из дизъюнкта C2. Причем литералы L1 и L2 образуют контрарную пару. Резольвентой дизъюнктов C1 и С2 называется дизъюнкт С, составленный из С1 вычеркиванием L1 и из C2 вычеркиванием L2. Таким образом, если у нас есть два дизъюнкта и один из них содержит литерал L, а другой — литерал ~ L, то мы можем рассмотреть дизъюнкт, который содержит литералы первого за исключением литерала L и литералы второго за исключением ~ L. Такой дизъюнкт называется резольвентой первых двух. Например, если первый дизъюнкт ~ A v С, второй ~ С v D, то их резольвентой будет формула ~ A v D. Если первый дизъюнкт состоит из одного литерала А, а второй из литерала ~ А, то их резольвентой будет тождественно ложный дизъюнкт, который принято обозначать символом. Выводом в методе резолюций дизъюнкта С из множества S называется последовательность дизъюнктов С1, C2, ..., Ck такая, что для любого i (i =< k) Сi — либо дизъюнкт из S, либо является резольвентой предыдущих дизъюнктов. Вывод можно рассматривать как формализованный аналог понятия доказательства.
Вывод тождественно ложного дизъюнкта называется опровержением. Пусть даны два дизъюнкта С1 и C2- Резольвента С дизъюнктов С1 и C2 является их логическим следствием. Резольвента позволяет переходить от двух рассуждений к третьему, а теорема о резольвенте гарантирует, что если исходные утверждения были истинными, то истинным будет и построенное утверждение, т. е. резольвента. Доказательство. Пусть C1 = L v Р и С2 = ~ L v Q, тогда резольвента имеет вид Р v Q. Предположим, что дизъюнкты С1 и С2
истинны в произвольно взятой интерпретации I. Нам требуется доказать, что
резольвента С также истинна в этой интерпретации. Если значение литерала
L в выбранной интерпретации истинно, то значение литерала ~ L
ложно, но тогда значение дизъюнкта Q должно быть истинным, т. к.
истинен дизъюнкт C2. А поскольку значение дизъюнкта Q истинно, то
и резольвента истинна. Если же значение литерала L в выбранной
интерпретации ложно, то истинным должно быть значение дизъюнкта Р, т. к.
дизъюнкт С2 истинен. Как и в предыдущем случае, резольвента будет иметь
значение "истина". Таким образом, резольвента является логическим следствием
дизъюнктов, по которым она построена. Пример использования теоремы о резольвенте Предположим, что справедливы следующие утверждения:
Введем следующие обозначения: обозначим через Р утверждение "Электрички приходят не по расписанию", через Q — "Студенты опаздывают на лекцию" и, наконец, через R — "Преподаватель недоволен". Тогда приведенные рассуждения записываются формулами: (P => Q) и (Q => R). После преобразования к КНФ получим дизъюнкты (~ P v Q) и (~ Q v R), содержащие контрарную пару. Резольвентой этих двух дизъюнктов будет формула
(~ Р v R), которая эквивалентна формуле (Р => R).
Последняя формула, очевидно, соответствует рассуждению: "Если электрички не
приходят по расписанию, то преподаватель недоволен". Найдите все возможные резольвенты (если они есть) следующих пар дизъюнктов:
Напишите сценарий, который по двум заданным дизъюнктам строит резольвенту,
если это возможно. Теорема о полноте метода резолюций Множество дизъюнктов S противоречиво тогда и только тогда, когда существует опровержение в S (или из S). Доказательство. Приведем доказательство достаточности. Предположим, что мы построили опровержение во множестве дизъюнктов S, вывод имеет вид: D1, D2, ..., Dn. Докажем, что множество дизъюнктов S противоречиво. Предположим, что это не так, множество S выполнимо и, следовательно, существует интерпретация S, в которой все дизъюнкты из S истинны. Каждое D, в опровержении либо из множества S и является истинным, либо представляет из себя логическое следствие предыдущих дизъюнктов и также истинно по теореме о резольвенте. Но тогда и последний дизъюнкт истинен, чего не может быть, потому что последний дизъюнкт в опровержении тождественно ложная формула. Вернемся к сформулированной ранее задаче. Пусть у нас есть аксиомы или уже доказанные факты F1, F2, ..., Fm. Нам требуется определить, следует ли утверждение G из фактов F1, F2, ..., Fm. По теореме 2 о логическом следствии для решения этого вопроса нам достаточно определить, является ли формула F1 & F2 & ... & Fm & ~ G противоречивой. Эту формулу можно преобразовать к КНФ и рассматривать в дальнейшем множество дизъюнктов S: S= {S1, S2, ..., Sn}. По теореме о полноте метода резолюций, для того чтобы определить
противоречивость (невыполнимость) множества S, достаточно найти
опровержение в S. В совершении преступления подозреваются четверо человек: А, В, С, D. Установлено следующее:
Виновен ли D? Будем считать, как и раньше, что через А обозначено утверждение "А виновен", через В— "В виновен", через С—"С виновен" и, наконец, через D — "D виновен". Запишем четыре известных факта и ответ на вопрос формулами исчисления высказываний:
Следствие G: D (D виновен). По теореме 2 о логическом следствии построим для наших конкретных высказываний формулу вида FI & F2 & F3 & F4 & ~ G: (A v В => C) & (А => В v C) & (С => D) & (~A => D) & ~ D. Приведем ее к КНФ, получим множество дизъюнктов, которые обозначим S1-S6: S = {~ A v С, ~ В v С, ~ A v В v С, ~ С v D, A v D ~ D}. Построим опровержение в S:
Построив опровержение в методе резолюций, мы по теореме о полноте метода
резолюций доказали, что множество дизъюнктов противоречиво, следовательно,
рассматриваемая формула противоречива. По теореме 2 утверждение G —
логическое следствие, т. е. подозреваемый в преступлении D
виновен. Перед нами три девушки: Сью, Марция и Диана. Предположим, что юноша, занимающийся математической логикой, высказывает следующее.
Требуется определить, любит ли автор высказываний Диану? Запишем формулами четыре высказывания и предполагаемое следствие:
Формулу, построенную согласно теореме 2 о логическом следствии: (C v M v D) & (C & ~ D => M) & (D & M v ~ D & ~ M) & (D => Q & ~ D приведем к КНФ и получим интересующее нас множество дизъюнктов: S = {С v М v D ~ С v М v D, M v ~ D, ~ М v D ~ D v С, ~ D]. Считаем, что наши исходные дизъюнкты пронумерованы от S1 до S6. Построим опровержение в S:
На основании теоремы о полноте метода резолюций делаем вывод о том, что автор
высказываний любит Диану. 1. Постройте опровержение для решения следующей задачи. На острове рыцарей и л |
