| Назад | Содержание | Вперед |
В предыдущих главах для самострятельной работы предлагались упражнения, которые располагались в конце каждой главы. При выполнении упражнения следовало написать сценарий решения некоторой задачи. В настоящей главе изложение материала будет изменено. Упражнение может быть предложено сразу после рассмотрения теоретического материала или примера, иллюстрирующего теорию. Кроме того, упражнения не обязательно предполагают создание сценария. Отдельно формулируется задание на создание сценария.
Материал этой главы посвящен введению в один из разделов искусственного интеллекта — автоматическое доказательство теорем.
В обычной жизни человек принимает решения в зависимости от конкретной ситуации. Предположим, что нам известны некоторые факты (или ранее уже доказанные утверждения) F1, F 2, ..., Fn, и нас интересует, следует ли некоторое утверждение G из утверждений F1, F 2, ..., Fn. Утверждение, что G логически следует из утверждений F1, F 2, ..., Fn называют теоремой. Доказательство теоремы — рассуждения, позволяющие установить, что теорема верна.
Математическая логика — наука о правильных математических рассуждениях, о математическом мышлении. Впервые правила рассуждений систематизировал Аристотель. Однако как наука математическая логика сложилась лишь в середине XIX века, когда Джордж Буль ввел логические связки и исчисление высказываний. Математическая логика изучает:
и многое другое. Одной из задач математической логики является формализация понятия доказательства.
Для описания утверждений можно использовать формулы исчисления высказываний. Каждое высказывание либо истинно, либо ложно. Можно строить составные высказывания, используя логические связки', отрицание (~), конъюнкцию (&), дизъюнкцию (у), импликацию (=>) и эквивалентность (<=>). Логические константы "истина" и "ложь" будем обозначать буквами И и Л соответственно. Логические переменные (в математической логике их называют пропозициональные переменные) будем обозначать большими буквами латинского алфавита.
Унарная связка ~ меняет значение высказывания на противоположное. В табл. 20.1 представлены результаты логических связок таблицы истинности.
Таблица 20.1. Таблица истинности бинарных связок
|
А
|
B
|
А&В
|
AvB
|
А=>В
|
А<=>В
|
|
и
|
и
|
и
|
и
|
и
|
и
|
|
и
|
л
|
л
|
и
|
л
|
л
|
|
л
|
и
|
л
|
и
|
и
|
л
|
|
л
|
л
|
л
|
л
|
и
|
и
|
В исчислении высказываний логические константы и логические переменные называются атомами и считаются простейшими логическими формулами. Кроме атомов логической формулой считается отрицание логической формулы, а также (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. Равнозначные формулы
|
Формула |
Формула |
|
А <-> B <-> (~ A v B) & (~ В v А) (А => В) <-> ~ A v B A v (S v С) <-> (A v B) v С A v (B & C) <-> (A v B) & ( A v C ) ~ (~A) <-> A A v ~ A <->A A v <->A ~ (A v B) <-> ~ A & ~ B |
А & (В & С) <-> (А & В) & С А & В <-> В & А А & (В v С) <-> (А & B) v (А & С)
A & ~ A <-> А & <-> A & <-> A ~ (A & В) <-> ~ A v ~ B |
Нетрудно доказать, что любую формулу исчисления высказываний можно преобразовать к равнозначной формуле, которая содержит только три логические связки: отрицание, конъюнкцию и дизъюнкцию. Действительно доказав равнозначность формул А => В и ~А v В, а также формул A<=>B и (A & B) v (~А & ~B), получим то, что требуется. Некоторые часто используемые правила получили специальные названия, например:
Пусть заданы две формулы (A => B) => С и A => (В => С). Требуется определить, эквивалентны ли они. Для того чтобы решить задачу, мы переберем все интерпретации и в каждой из интерпретаций вычислим значение формулы. Результаты приведены в табл. 20.3.
Таблица 20.3.
Таблица истинности для формул (А => В) => С и А
=*
(В => С)
|
№
|
А
|
B
|
C
|
(А=>В)=>С
|
А => (В => С)
|
|
1
|
и
|
и
|
и
|
и
|
и
|
|
2
|
и
|
и
|
л
|
л
|
л
|
|
3
|
и
|
л
|
и
|
и
|
и
|
|
4
|
и
|
л
|
л
|
и
|
и
|
|
5
|
л
|
и
|
и
|
и
|
и
|
|
6
|
л
|
и
|
л
|
л
|
и
|
|
7
|
л
|
л
|
и
|
и
|
и
|
|
8
|
л
|
л
|
л
|
л
|
и
|
После вычислений видно, что значения формул не совпадают в некоторых интерпретациях, поэтому заданные формулы неравнозначны.
Напишем сценарий, который для логической формулы строит таблицу истинности. В формуле разрешено использовать операции отрицания, дизъюнкции и конъюнкции; переменные представляются буквами латинского алфавита. Вид документа представлен на рис. 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) => В) и В
|
В
|
D
|
F: ( (В => D) => В)
|
G:B
|
|
и
|
и
|
и
|
и
|
|
и
|
л
|
и
|
и
|
|
л
|
и
|
л
|
—
|
|
л
|
л
|
л
|
—
|
Нас интересуют только те интерпретации, в которых формула
F
истинна. В этих интерпретациях истинна и формула
G.
Согласно определению формула
G —
логическое следствие формулы
F.
Таким образом, мы выяснили, что ответ на вопрос "Люблю ли я Бетти?" — положительный.
На складе совершено хищение. Подозрение пало на трех человек: А, Б и С. Они были доставлены для допроса. Установлено следующее:
Виновен ли В?
Запишем приведенные утверждения с помощью формул исчисления высказываний. На основании определения логического следствия выясним, является ли ответ на вопрос логическим следствием этих трех утверждений. Обозначим через А утверждение "А виновен", через В — "В виновен", через С — "С виновен". Запишем утверждения 1—3 с помощью формул F1 - F3 исчисления высказываний:
Предполагаемый ответ — "В виновен" — обозначим через G. Проверим, является ли формула (7 логическим следствием формул F1, F2, F3 . С помощью табл. 20.5 переберем интерпретации и для всех укажем значение каждой из формул F1, F2, F3 в этой интерпретации.
Таблица 20.5, Таблица интерпретаций для формул F1, F2, F3
|
№
|
А
|
B
|
C
|
F1: A v В v C
|
F2: А => В v С
|
F3: ~ C
|
G:B
|
|
1
|
и
|
и
|
и
|
и
|
и
|
л
|
|
|
2
|
и
|
и
|
л
|
и
|
и
|
и
|
и
|
|
3
|
и
|
л
|
и
|
и
|
и
|
л
|
|
|
4
|
и
|
л
|
л
|
и
|
л
|
и
|
|
|
5
|
л
|
и
|
и
|
и
|
и
|
л
|
|
|
6
|
л
|
и
|
л
|
и
|
и
|
и
|
и
|
|
7
|
л
|
л
|
и
|
и
|
и
|
л
|
|
|
8
|
л
|
л
|
л
|
л
|
и
|
и
|
|
Как и в предыдущем примере, нас интересуют только те интерпретации, в которых все посылки (формулы
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
|
(A <=> L)
|
(А <=> (А <=> L))
|
(А <=> (А <=> 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. Построение конъюнктивной нормальной формы
|
№
|
X
|
Y
|
Z
|
(X => Y) <=> Z
|
Дизъюнкты формулы
|
|
1
|
и
|
и
|
и
|
и
|
|
|
2
|
и
|
и
|
л
|
л
|
~X v ~ Y v Z
|
|
3
|
и
|
л
|
и
|
л
|
~ X v Y v ~ Z
|
|
4
|
и
|
л
|
л
|
и
|
|
|
5
|
л
|
и
|
и
|
и
|
|
|
6
|
л
|
и
|
л
|
л
|
X v ~ V v Z
|
|
7
|
л
|
л
|
и
|
и
|
|
|
8
|
л
|
л
|
л
|
л
|
X v Y v Z
|
Выделим те интерпретации, в которых формула принимает значение "ложь", и для этих интерпретаций построим дизъюнкт по правилу: если значение переменной — "ложь", то включаем в дизъюнкт эту переменную, в противном случае включаем переменную с отрицанием. Тогда по построению в интерпретациях, в которых значение / ложно, значение 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.
|
| Рис 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.
|
| Рис 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. Постройте опровержение для решения следующей задачи. На острове рыцарей и лжецов за преступление судили двух жителей. Обвинитель, однако, оказался также жителем острова. Он заявил следующее.
• Х и Yне могут быть виновны оба;
• X виновен.
Кто обвинитель: рыцарь или лжец?
2. Постройте опровержение для решения следующей задачи. Три человека, А, В и С, проживают на острове рыцарей и лжецов. Условимся называть двух людей однотипными, если они оба рыцаря или оба лжеца. Пусть А и В высказывают следующие утверждения:
• А: В — лжец;
• В: А и С однотипны.
Кто такой С: рыцарь или лжец?
1. Напишите сценарий, который по заданной последовательности дизъюнктов определяет, может ли она быть выводом в данном множестве дизъюнктов.
2. Напишите сценарий построения опровержения для заданного множества дизъюнктов.
Методы сокращения множества дизъюнктов
Мы исследуем вопрос, является ли противоречивым множество дизъюнктов
S.
Однако это множество может быть достаточно велико, поэтому искать вывод
из большого множества дизъюнктов иногда затруднительно. Возникает вопрос, можно
ли как-нибудь это множество сократить? Математики Девис и Патнем предложили
несколько правил, которые позволяют сократить исходное множество дизъюнктов.
Из множества дизъюнктов
S
можно вычеркнуть все дизъюнкты, которые являются тавтологиями. Оставшееся множество дизъюнктов противоречиво тогда и только тогда, когда противоречиво множество
S.
Правило однолитерных дизъюнктов
Если во множестве
S
существует однолитерный дизъюнкт
L,
то множество
Si
получается из
S
вычеркиванием всех дизъюнктов, содержащих
L.
Если построенное
Si
пусто, то исходное
S
выполнимо. Для доказательства выполнимости
S
достаточно рассмотреть интерпретацию, в которой значение
L
истинно. В противном случае по
S\
строим множество дизъюнктов
S^,
вычеркивая из
S\
все вхождения ~
L.
Множество дизъюнктов 52 противоречиво тогда и только тогда, когда противоречиво множество
S.
Задача о влюбленном логике с применением правила однолитерного дизъюнкта
Мы рассмотрели ранее задачу о влюбленном логике и трех девушках: Сью, Марции и Диане. Для решения вопроса о том, любит ли человек, высказывающий четыре утверждения, Диану, мы строили опровержение в методе резолюций. Однако решить эту задачу можно, применяя к построенному множеству дизъюнктов правило однолитерного дизъюнкта. Рассмотрим множество дизъюнктов S:
S={C v M v D, ~ C v D v M, D v ~ M, ~ D v M, ~ D v С, ~ D}.
Дизъюнкт ~ D — однолитерный; применив к множеству S правило однолитерного дизъюнкта, получим множество S2
S1 = {C v M v D, ~ C v D v M, D v ~ M}.
Теперь вычеркиванием из S1 всех вхождений D получим множество S2:
S2={C v М, ~ C v М, ~ М}.
В построенном множестве также есть единичный дизъюнкт ~
М
.
После применения правила единичного дизъюнкта к этому множеству получаем
{С, ~ С}
.
В последнем множестве опять есть единичный дизъюнкт, после применения правила получаем противоречивое множество, следовательно, и исходное множество
S
противоречиво, т. е.
D —
логическое следствие.
Литерал L называется чистым литералом, если в S не входит литерал ~ L.
Если
L —
чистый литерал, то вычеркиваем из
S
все дизъюнкты, содержащие
L.
Оставшееся множество дизъюнктов обозначим через
Si.
Множество дизъюнктов
Si
противоречиво тогда и только тогда, когда противоречиво множество
S.
Пусть множество S можно представить в виде:
S= {A1 v L, ..., Am v L, B1 v ~ L, ..., Bk v ~ L, R1, ..., Rq], причем дизъюнкты
Ai, Bi, Ri не содержат ни L, ни ~ L. Рассмотрим два множества:
Множество S противоречиво тогда и только тогда, когда оба множества
S1 и S2 противоречивы.
Пример использования правила чистого литерала
Рассмотрим множество дизъюнктов S:
S = {A v В v С, A v В v ~ С, ~ В, ~ С}.
В этом множестве есть чистый литерал А. Применим к множеству дизъюнктов правило чистого литерала. Множество после применения правила чистого литерала будет следующим:
S1 = {~B,~ C}.
Пример использования правила расщепления
Рассмотрим множество дизъюнктов S и применим к нему правило расщепления по литералу А:
S = {~ A v В, ~ A v ~ В v С, A v D, D v ~ С, A v ~ D, ~ D}.
Полученные после применения правила расщепления множества:
S1 = (В, ~ В v С, D v ~ С, ~ D}, S 2 = {D, ~ D, D v ~ C}.
Множество S1 противоречиво, доказать это можно, построив, например, опровержение в S1.
Множество S2 противоречиво, т. к. опровержение строится по дизъюнктам D и ~ D.
В некоторых случаях удается решить задачу, используя лишь правила сокращения дизъюнктов. Продемонстрируем такую возможность при решении следующей задачи.
Задача об искателе приключений
Предположим, что некоторый искатель приключений хочет добраться до острова сокровищ. Путешественнику предложили три карты: X, Y и Z. Только одна из карт правильная и указывает путь к острову сокровищ. В комнате, где лежали карты, находились пятеро колдунов: А, В, С, D и Е. Каждый колдун был либо рыцарем, либо лжецом и каждый дал путешественнику совет:
Какая же из карт правильная?
Докажем, что Y — правильная карта. Будем, как ранее, обозначать через А утверждение "А — рыцарь" (аналогично для В, С, D и Е). Обозначим через X утверждение "X— правильная карта" (аналогично для Y и Z ). Запишем сначала советы колдунов и предполагаемое следствие формулами исчисления высказываний:
Построим КНФ вида
F1 & F2 & F3 & F4 & F5 & ~ G.
Для этого приведем каждое из Fi к КНФ:
Рассматриваемое нами далее множество дизъюнктов S имеет вид
S={~ A v X, A v ~ X, ~ B v Y, B v ~ Y, A v B v ~ С, C v ~ A, C v ~ B,~ D v
~A v B, A v D, ~ B v D, ~ C v D v ~ E, C v ~ D v ~ E, E, ~ C v ~ D v E,
C v D v E, ~ Y}.
Применим к множеству S правило единичного дизъюнкта (дизъюнкт Е), получим множество S1:
S1 = {A v X, A v ~ X, ~ B v Y, B v ~ Y, A v B v ~ C, C v ~ A, C v ~ B, ~ D v ~ A v B, A v D,~ B v D, ~ C v D, C v ~ D, ~ Y}.
В полученном множестве есть единичный дизъюнкт ~ Y, применим к множеству S2 правило единичного дизъюнкта, получим множество S2.
S2 = {~ A v X, A v ~ X, ~ B, A v B v ~ C, C v ~ A, C v ~ B, ~ D v ~ A v B, A v
D, ~ B v D, ~ C v D, C v ~ D}.
Во множестве S2 есть единичный дизъюнкт ~ В, после применения правила по этому дизъюнкту получим множество S3 :
S3 = {~ A v X, A v ~ X, A v ~ C, C v ~ A,~D v ~ A, A v D, ~ C v D, C v ~ D}.
К построенному множеству S2 применим правило расщепления по дизъюнкту А, получим два множества S4 и S5 :
S4 = {X, С, ~D, -C v D, C v ~ D};
S5 = {~ X, ~ С, D, ~ С v D, C v ~ D}.
Во множестве S4 есть чистый литерал X. По правилу чистого литерала все дизъюнкты, содержащие этот литерал, можно исключить из рассматриваемого множества. Получим множество
S6 = {C, ~ D, ~ C v AC v ~ D}.
К множеству S5 можно применить правило единичного дизъюнкта по литералу
С,
получим множество S7 = {~ D, D}
.
Множество
S7
противоречиво.
Во множестве S5 есть чистый литерал ~
X.
Применяя к
S5
правило
чистого литерала, а затем правило единичного дизъюнкта, получаем противоречивое
множество. Следовательно, утверждение
Y—
логическое следствие утверждений
FI—FS,
таким образом, карта
Y —
правильная карта и поиск сокровищ
можно продолжать.
1. Перед нами три островитянина, А, В, С, каждый из которых либо рыцарь, либо лжец. Двое из них высказывают утверждения.
• А: все мы лжецы;
• В: ровно один из нас лжец. Кто такой островитянин С?
Постройте множество дизъюнктов и примените для сокращения к нему правила Девиса и Патнема.
2. Путешественник проснулся на острове рыцарей и лжецов, название которого он не помнит. Он разговорился с двумя местными жителями А и В, которые сообщили ему следующее.
• А: В — рыцарь и остров называется Майя;
• В: А — лжец и остров называется Майя.
Можно ли утверждать, что остров действительно называется Майя.
Постройте множество дизъюнктов и примените для сокращения к нему правила Девиса и Патнема.
3. Внимание трех девушек Екатерины, Елены и Евгении привлек проезжающий мимо автомобиль.
• Екатерина сказала: "Эта машина изготовлена в США, марка ее — Форд";
• Елена возразила: "По-моему, эта машина из Германии, ее марка — Мерседес";
• Евгения добавила: "Марка машины — Ауди, изготовлена не в США".
Оказалось, что каждая из трех девушек права только в одном из своих высказываний. Какой марки автомобиль, и в какой стране изготовлен?
Постройте множество дизъюнктов и примените для сокращения к нему правила Девиса и Патнема.
1. Напишите сценарий, который сокращает заданное множество дизъюнктов по правилам Девиса и Патнема.
2. Напишите сценарий, который проверяет правильность построения формулы исчисления высказываний методом рекурсивного спуска.
3. Напишите сценарий, который для заданной пропозициональной формулы находит все подформулы, значения которых совпадают с заданным.
4. Напишите сценарий, который по формуле исчисления высказываний, представленной в инфиксной нотации, строит формулу в префиксной нотации.
5. Напишите сценарий, который вычисляет значение пропозициональной формулы, находящейся в постфиксной нотаций.
6. Напишите сценарий, при выполнении которого пропозициональная формула преобразуется таким образом, что знак отрицания встречается лишь перед переменной.
7. Заданы две пропозициональные формулы. Напишите сценарий, который проверяет, являются ли формулы эквивалентными.
8. Переменная х в формуле А называется фиктивной, если существует формула В, эквивалентная формуле А, и не содержащая вхождений переменной х. Напишите сценарий, который находит в заданной формуле все фиктивные переменные.
9. Напишите сценарий, который по заданной пропозициональной формуле определяет, верно ли, что на наборах противоположных значений переменных формула принимает противоположное значение.
10. Пара скобок в пропозициональной формуле называется избыточной, если после ее удаления формула остается эквивалентной исходной формуле. Напишите сценарий, который удаляет все избыточные пары скобок.
Если задача описывается с помощью формул исчисления высказываний, то многие этапы решения задачи (определение общезначимости, противоречивости или выполнимости формул, приведение к КНФ, сокращение множества дизъюнктов и др.) можно автоматизировать, в чем мы могли убедиться, выполняя различные задания по написанию сценариев.
Полученные знания рекомендуется применить при создании сайта, позволяющего пользователю решать логические задачи и проверять правильность решения. Для выбранной из предложенного списка задачи пользователю требуется ввести формулы, соответствующие условию задачи, и указать предполагаемое следствие. Созданный сценарий должен проверять правильность решения задачи любым из описанных способов. Предлагается следующий список задач, который может быть дополнен или изменен разработчиком.
В одном старинном задачнике описан суд Париса следующим образом. Богини Гера, Афродита и Афина пришли к Парису, чтобы он решил, кто из них прекраснее. Богини (обозначим их a, b, c) высказали следующие утверждения.
Парис предположил, что высказывания прекраснейшей из богинь истинны, а все утверждения двух остальных ложны. Мог ли Парис вынести свое решение? Кто прекраснейшая из богинь? Какие богини скрываются под именами а,
b, c?
Перед началом бегов на ипподроме четверо знатоков из числа зрителей обсуждали шансы трех фаворитов: А, В и С. Во время обсуждения были высказаны следующие утверждения.
После заезда выяснилось, что фавориты А, В и С
действительно заняли первые три места и что все четыре высказывания знатоков оказались истинными. Как фавориты поделили между собой места?
Поиск пути выхода из лабиринта
Одинокий путник заблудился в лабиринте и попал в комнату, из которой можно выйти в одну из четырех дверей: X, Y, ZK W. По крайней мере одна из дверей ведет к выходу из лабиринта. Того, кто выходит через другую дверь, ожидает дракон, живущий в лабиринте.
К удивлению путника в комнате находятся восемь жрецов, каждый из которых либо рыцарь и говорит всегда только правду, либо лжец и всегда лжет: А, В, С, D, Е, F, G и H . Нашему путнику жрецы сообщили следующее:
Какую же дверь выбрать одинокому путнику?
Какие выводы вы бы сделали из следующих фактов?
Чья виновность не вызывает сомнений?
Обвинитель на острове рыцарей и лжецов
На одном из островов, населенных рыцарями и лжецами, за совершение преступления судили двух местных жителей X и Y. Об обвинителе было известно, что он либо рыцарь, либо лжец. На суде обвинитель сделал два заявления:
Кто обвинитель: рыцарь или лжец?
Суд на острове рыцарей и лжецов
Предположим, что обвинитель сделал следующих два заявления:
К какому заявлению вы бы пришли на основании этих заявлений?
Предположим, что некоторый человек, который может быть либо рыцарем, либо лжецом, делает следующие заявления:
Интервью на острове рыцарей и лжецов
У трех обитателей А, В и С острова рыцарей и лжецов взяли интервью, в ходе которого они высказали следующие утверждения:
Можно ли определить, кто из
А, В
и
С
рыцарь и кто лжец?
Путешественник ищет остров с названием Майя. Исследуя третий остров, путешественник встретил двух жителей А и В, которые заявили следующее:
Можно ли утверждать, что третий остров действительно называется Майя?
Путешественник ищет остров с названием Майя. Исследуя шестой остров, путешественник встретил двух жителей А и В, которые заявили следующее:
Можно ли утверждать, что шестой остров действительно называется Майя?
В этом случае подсудимых четверо:
Кто из подсудимых виновен вне всякого сомнения, и чья вина остается под сомнением?
Предположим, что некоторый искатель приключений хочет добраться до острова сокровищ. Путешественнику предложили три карты: X, Y и Z. Только одна из карт правильная и указывает путь к острову сокровищ. В комнате, где лежали карты, находились пятеро колдунов: А, В, С, D и Е. Каждый колдун был либо рыцарем, либо лжецом и каждый дал путешественнику совет:
Какая же из карт правильная?
| Назад | Содержание | Вперед |