Все для программиста. Статьи для програмиста скачать бесплатно учебники книги документация форум : Статьи : Глава 20. Формулы исчисления высказываний.

Главное меню
Главная
Опросы
Книжный магазин
Реклама на сайте
Публикации
Партнеры
Рассылки
RSS экспорт
Настройки
О нас пишут
Контакты

Поиск
Google
www сайт

Новостной блок
Новости
Microsoft .NET
Microsoft WinFS
JAVA
Borland JBuilder
MySQL
Microsoft Virtual Server
Oracle
Avalon (WPF)
Книжные новости
Продукты Sybase
Google Code Jam
Cisco
Конференция ISDEF
Лицензия GPL
Mozilla Foundation
Windows Server
Форум Intel (IDF)
Технология AJAX
Обзор вакансий
Безопасность
Стандарты
Новости от Borland
Новости от IBM
Новости SDK
PHP Project
Opensource
Visual Studio 2005
SQL Server 2005
Windows Shell
Веб-сервисы
СУБД PostgreSQL
World Wide Web
Сертификация
Новости от SUN
Телекоммуникации
Новости от SUN
Apache
CRM
Платформа 2006
Microsoft LINQ
Exchange Server
Windows Vista
Google
IronPython
Новости Adobe
Microsoft Dynamics
BizTalk Server
Платформа Live
MS Office 2007
GameDev
WinHEC
Sap
Ubuntu Linux
AMD
1C
Python
Commerce Server
Ruby
Symantec
Live OneCare
CodePlex
Документооборот
Дополненния
Новости Red Hat
Новости софта
InstallShield
Microsoft
Apple
Opera
Autodesk

Основные разделы
C/С++
Delphi
Базы данных
Интернет технологии
Конкурсные статьи
Assembler
.NET Framework
Turbo Pascal
Visual Studio.NET
XAML
C# C Sharp
Visual Basic
TCP/IP
Visual Basic 7 .NET
Графика и игроделание
Windows Server 2003
Visual Studio 2005
Сети
Windows Vista
Microsoft Office
AutoCad
WxWidgets
Системы защиты
Оптимизация кода
Software Testing
Реинжиниринг
Многоядерность
Управление
Microsoft Axapta
Алгоритмы
Обучение
Фракталы
Assembler
Windows Installer
MS-DOS
Visual Basic
Windows API
Драйвера
Создание ОС
Криптография
Протоколы
Linux
Разное
Юмор

Разделы форума
Delphi,Pascal
C/C++, среды
WEB dev [image] Java
VB, VBscript
DirectX, OpenGL
Assembler
.NET Framework
Алгоритмы
ОС (Win, Unix)
Интернет, сети
Дизайн и графика
Разговоры
Сертификация
PowerBuilder
Microsoft Office
Железо
Алгоритмы
Для разработчиков
1C: Вопросы и отв.
Software Development
Windows Vista
Студенту
Безопасность
Конкурсы
Работа

Кто онлайн
Вы не зарегистрированы.
Имя:

Пароль:

Запомнить

Регистрация позволит Вам пользоваться дополнительными сервисами.
Сейчас на сайте:
Гостей: 176
Пользователей: 0

Статьи:: Интернет технологии :: Учебник по JavaScript :: Глава 20. Формулы исчисления высказываний.

Глава 20. Формулы исчисления высказываний.

Глава 20
Формулы исчисления высказываний

  • Общие сведения
  • Упражнения
  • Вычисление значения постоянной логической формулы
  • Вычисление значения формулы в заданной интерпретации
  • Соотношение формул
  • Построение таблицы истинности
  • Упражнение
  • Определение выполнимой, общезначимой и противоречивой формулы
  • Логическое следствие
  • Представление утверждений формулами
  • Задача о хищении
  • Упражнение
  • Теоремы о логическом следствии
  • Пример использования теоремы 1 о логическом следствии
  • Упражнение
  • Задание по программированию
  • Пример использования теоремы 2 о логическом следствии
  • Задача о рыцарях и лжеца
  • Упражнения
  • Конъюнктивная нормальная форма и ее построение
  • Теорема
  • Упражнение
  • Построение формулы в конъюнктивной нормальной форме
  • Алгоритм построения КНФ
  • Упражнения
  • Автоматизация ввода логических формул
  • Метод резолюций
  • Теорема о резольвенте
  • Пример использования теоремы о резольвенте
  • Упражнения
  • Задание по программированию
  • Теорема о полноте метода резолюций
  • Задача о поиске виновного
  • Задача о влюбленном логике
  • Упражнения
  • Задание по программированию
  • Методы сокращения множества дизъюнктов
  • Правило тавтологии
  • Правило однолитерных дизъюнктов
  • Задача о влюбленном логике с применением правила однолитерного дизъюнкта
  • Правило чистых литералов
  • Правило расщепления
  • Пример использования правила чистого литерала
  • Пример использования правила расщепления
  • Задача об искателе приключений
  • Упражнения
  • Задания по программированию
  • Занимательные задачи
  • Прекраснейшая богиня
  • Игроки на скачках
  • Поиск пути выхода из лабиринта
  • Расследование преступления
  • Обвинитель на острове рыцарей и лжецов
  • Суд на острове рыцарей и лжецов
  • Любовь рыцаря или лжеца
  • Интервью на острове рыцарей и лжецов
  • Путешественник на островах
  • Исследование шестого острова
  • Поиск виновных
  • Искатель приключений

Общие сведения

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

Материал этой главы посвящен введению в один из разделов искусственного интеллекта — автоматическое доказательство теорем.

В обычной жизни человек принимает решения в зависимости от конкретной ситуации. Предположим, что нам известны некоторые факты (или ранее уже доказанные утверждения) F1, F2, ..., Fn, и нас интересует, следует ли некоторое утверждение G из утверждений F1, F2, ..., Fn. Утверждение, что G логически следует из утверждений F1, F2, ..., 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 <-> B v A 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 v B) <-> ~ А & ~ В и ~ (А & B) <-> ~ A 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>&nbsp;Moжно использовать "следующие символы: <br>

snbsp;[a..u,w..z,A..U,W..Z] — односимвольные перёменные<br>

&nbsp;! — отрицание<br>

&nbsp;& — логическое И<br>

&nbsp;V — логическое ИЛИ<br> <br>

<input type="button" value="Таблица истинности"

onclick="TABLE()"><br>

</FORM><br>

</BODY>

</HTML>

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

Упражнение

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

  • ~(~(Р => Q))=>(P => Q)
  • ~ (Р & T v R)=> ~ Р
  • (Р => Q & R & T)=>(~ (Q & R & Т)=> Р)
  • P v (R => Q & T )
  • P v (Р & F=> Q & В)
  • ~ Р => (P v T v R & F)

Определение выполнимой, общезначимой и противоречивой формулы

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

При анализе формулы перебираются интерпретации. Вычисляется значение формулы в начальной интерпретации, а затем, если при переходе к следующей интерпретации значение формулы изменилось на противоположное, то она выполнима. Если же при всех интерпретациях значение формулы не изменилось, то она либо общезначима, либо противоречива. Результат выполнения сценария представлен на рис. 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>&nbsp;Можно использовать следующие символы:<br>

&nbsp;[a..u,w..z,A..U,W..Z] — односимвольные переменные<br>

&nbsp;! — отрицание<br>

&nbsp;& — логическое И<br>

&nbsp;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 исчисления высказываний:

  • F1: A v B v С
  • F2: A => В v С
  • 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 имеет КНФ. Эквивалентность формул можно доказать в качестве упражнения.

Упражнение

Преобразуйте следующие формулы в конъюнктивную нормальную форму:

  • (А <=> (А <=> S)) & S
  • ((E => М) =>E) & (E =>(E => М))

Построение формулы в конъюнктивной нормальной форме

Напишем сценарий, который на основании рассмотренной теоремы по произвольной формуле строит эквивалентную формулу, находящуюся в КНФ.

В текстовое поле вводится формула, после щелчка по кнопке, формируется эквивалентная формула, находящаяся в КНФ. Один из тестов продемонстрирован на рис 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:

  • (X => Y) <=> Z
  • ((Х => Y) => Z) & (Z => (X => Y))
  • (~ (X => Y) v Z) & (~ Z v ~ X v Y)
  • (~ (~ X v Y) v Z) & (~ Z v ~ X v Y)
  • (Х & ~Y v Z) & (~ Z v ~ X v Y) & (~ Z v ~ X v Y)
  • (X v Z) & (~Y v Z) & (~ X v Y v ~ Z)

Полученная формула G1

(X v Z) & (~ Y v Z) & (~ X v Y v ~ Z)

эквивалентна исходной формуле F, находится в конъюнктивной нормальной форме и не совпадает с G.

Упражнения

1. Преобразуйте следующие формулы в конъюнктивную нормальную форму:

  • ~ (Р & Q => (R => T
  • ((E => М) => ~ Е) v (E => (Е => ~ M)).
  • (P => (R => Т)) <=> ~ (P & Q)

2. Преобразуйте следующие формулы в дизъюнктивную нормальную форму:

  • ~ (Р & Q) => (R => T) & ~ R Е &
  • ((Е => Mf) => ~ Е) v (E => (E :=> ~ M))
  • ~P => (P =>(R =>T)) <=> ~ (P & Q)

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

Автоматизация ввода логических формул

Необходимо создать сценарий, который облегчает ввод логических формул. При нажатии кнопок, сопоставленных переменным, скобкам или логическим операциям, соответствующая операция появляется в поле ввода. После формирования формулы в текстовом поле при щелчке по кнопке вычисляется таблица истинности, определяется тип формулы, строится соответствующая формуле конъюнктивная или дизъюнктивная нормальные формы так, как показано на рис. 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). Последняя формула, очевидно, соответствует рассуждению: "Если электрички не приходят по расписанию, то преподаватель недоволен".

Упражнения

Найдите все возможные резольвенты (если они есть) следующих пар дизъюнктов:

  • ~ A v C v R v T v В
  • ~ B v C v ~ M
  • ~ A v В v С v ~ N
  • ~ C v D v ~ R
  • A v D v C v ~ Q
  • ~ D

Задание по программированию

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

Теорема о полноте метода резолюций

Множество дизъюнктов 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?

Будем считать, как и раньше, что через А обозначено утверждение "А виновен", через В— "В виновен", через С—"С виновен" и, наконец, через D — "D виновен". Запишем четыре известных факта и ответ на вопрос формулами исчисления высказываний:

  • F1 : A v В => С
  • F2 : A => В v С
  • F3 : С=> D
  • F4 ~ A => 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:

  • S7: ~ M v D резольвента S1 и S2
  • S8: D резольвента S7 и S5
  • S9: резольвента S8 и S6

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

Задача о влюбленном логике

Перед нами три девушки: Сью, Марция и Диана. Предположим, что юноша, занимающийся математической логикой, высказывает следующее.

  • Я люблю, по крайней мере, одну из этих трех девушек.
  • Если я люблю Сью, а не Диану, то я также люблю Марцию.
  • Я либо люблю Диану и Марцию, либо не люблю ни одну из них.
  • Если я люблю Диану, то я также люблю Сью.

Требуется определить, любит ли автор высказываний Диану?

Запишем формулами четыре высказывания и предполагаемое следствие:

  • F1: C v M v D
  • F2: С & ~ D => М
  • F3: D & M v ~ D & ~ М
  • F4: D => С
  • 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:

  • S7: M v D резольвента S1 и S2
  • S8: D резольвента S7 и S5
  • S9: резольвента S8 и 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. Рассмотрим два множества:

  • S1 = {A1, A2,..., Am, R1,.., Rq}
  • S2 = {B1, B2,...,Bk, R1,..., Rq}

Множество 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}, S2 = {D, ~ D, D v ~ C}.

Множество S1 противоречиво, доказать это можно, построив, например, опровержение в S1.

  • S5: С резольвента дизъюнктов В и ~ В v С
  • S6. D резольвента дизъюнктов С и D v ~ С
  • S7: резольвента дизъюнктов D и ~ D

Множество S2 противоречиво, т. к. опровержение строится по дизъюнктам D и ~ D.

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

Задача об искателе приключений

Предположим, что некоторый искатель приключений хочет добраться до острова сокровищ. Путешественнику предложили три карты: X, Y и Z. Только одна из карт правильная и указывает путь к острову сокровищ. В комнате, где лежали карты, находились пятеро колдунов: А, В, С, D и Е. Каждый колдун был либо рыцарем, либо лжецом и каждый дал путешественнику совет:

  • А. X — правильная карта;
  • В: Y— правильная карта;
  • С: неверно, что А и В — оба лжеца;
  • D: либо А — лжец, либо В — рыцарь;
  • Е либо А — лжец, либо С и D — однотипны (либо оба рыцари, либо оба лжецы).

Какая же из карт правильная?

Докажем, что Y — правильная карта. Будем, как ранее, обозначать через А утверждение "А — рыцарь" (аналогично для В, С, D и Е). Обозначим через X утверждение "X— правильная карта" (аналогично для Y и Z). Запишем сначала советы колдунов и предполагаемое следствие формулами исчисления высказываний:

  • F1: A<=> X
  • F2: В <=> Y
  • F3: C <=> ~ (~ А & ~ B)
  • F4: D <=> ~ A v В
  • F5: Е <=> ~ E v (C<=> D)
  • G: Y

Построим КНФ вида

F1 & F2 & F3 & F4 & F5 & ~ G.

Для этого приведем каждое из Fi к КНФ:

  • F1: А <=> X <-> (~ A v X) & (A v ~ X)
  • F2: В <=> Y <-> (~ B v Y) & (B v ~ Y)
  • F3: С <=> ~ (~ A & ~ B) <-> (~ С v A v B) & (С v ~ A & ~ B) (A v В v ~ C & (C v ~ A) & (C v ~ В)
  • F4: D <=> ~ A v B <-> (~ D v ~ A v B) & (A & ~ B v D)<-> (~ D v ~ A v В) & (A v D) & (~ В v D)
  • F5: E <=> ~ E v (C <=> D) <-> (~ Е v ~ Е v (~ С v D) & (С v ~ D)) & (Е & ~ (С <=> D) v E) <-> (~ C v D v ~ E) & (C v ~ D v ~ E) & E & (~ C v ~ D v E) & (C v D v E)

Рассматриваемое нами далее множество дизъюнктов 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) высказали следующие утверждения.

  • a: самая прекрасная;
  • b: фродита не самая прекрасная;
  • c: я самая прекрасная;
  • a: Гера не самая прекрасная;
  • b: я самая прекрасная.

Парис предположил, что высказывания прекраснейшей из богинь истинны, а все утверждения двух остальных ложны. Мог ли Парис вынести свое решение? Кто прекраснейшая из богинь? Какие богини скрываются под именами а, b, c?

Игроки на скачках

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

  • заезд выиграет А или С;
  • если А придет вторым, то выиграет В;
  • если А придет третьим, то С не выиграет;
  • вторым придет А или В.

После заезда выяснилось, что фавориты А, В и С действительно заняли первые три места и что все четыре высказывания знатоков оказались истинными. Как фавориты поделили между собой места?

Поиск пути выхода из лабиринта

Одинокий путник заблудился в лабиринте и попал в комнату, из которой можно выйти в одну из четырех дверей: X, Y, ZK W. По крайней мере одна из дверей ведет к выходу из лабиринта. Того, кто выходит через другую дверь, ожидает дракон, живущий в лабиринте.

К удивлению путника в комнате находятся восемь жрецов, каждый из которых либо рыцарь и говорит всегда только правду, либо лжец и всегда лжет: А, В, С, D, Е, F, G и H. Нашему путнику жрецы сообщили следующее:

  • А. X — дверь, ведущая к выходу из лабиринта;
  • В: по крайней мере одна из дверей Xи Уведет к выходу из лабиринта;
  • С: А и В — рыцари;
  • D: обе двери Х и Y ведут к выходу из лабиринта;
  • Е: обе двери Х и Zведут к выходу из лабиринта;
  • F: либо D, либо Е — рыцарь;
  • G: если С — рыцарь, то F — рыцарь;
  • Н: если Сия сам — рыцари, то А — рыцарь.

Какую же дверь выбрать одинокому путнику?

Расследование преступления

Какие выводы вы бы сделали из следующих фактов?

  • Если А виновен и В невиновен, то С виновен.
  • С никогда не действует в одиночку.
  • А никогда не ходит на дело вместе с С.
  • Никто, кроме А, B и С, в преступлении не замешан и, по крайней мере, один из этой тройки виновен.

Чья виновность не вызывает сомнений?

Обвинитель на острове рыцарей и лжецов

На одном из островов, населенных рыцарями и лжецами, за совершение преступления судили двух местных жителей X и Y. Об обвинителе было известно, что он либо рыцарь, либо лжец. На суде обвинитель сделал два заявления:

  • X виновен;
  • Х и Y не могут быть виновны оба.

Кто обвинитель: рыцарь или лжец?

Суд на острове рыцарей и лжецов

Предположим, что обвинитель сделал следующих два заявления:

  • либо Х не виновен, либо F виновен;
  • X виновен.

К какому заявлению вы бы пришли на основании этих заявлений?

Любовь рыцаря или лжеца

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

  • я люблю Линду;
  • если я люблю Линду, то я люблю Диану. Кто же он: рыцарь или лжец?

Интервью на острове рыцарей и лжецов

У трех обитателей А, В и С острова рыцарей и лжецов взяли интервью, в ходе которого они высказали следующие утверждения:

  • А: В — рыцарь;
  • В: если А — рыцарь, то С — рыцарь.

Можно ли определить, кто из А, В и С рыцарь и кто лжец?

Путешественник на островах

Путешественник ищет остров с названием Майя. Исследуя третий остров, путешественник встретил двух жителей А и В, которые заявили следующее:

  • А: по крайней мере, один из нас лжец, и этот остров называется Майя;
  • В: совершенно верно!

Можно ли утверждать, что третий остров действительно называется Майя?

Исследование шестого острова

Путешественник ищет остров с названием Майя. Исследуя шестой остров, путешественник встретил двух жителей А и В, которые заявили следующее:

  • А: либо В — рыцарь, либо этот остров называется Майя;
  • В: либо А — лжец, либо этот остров называется Майя.

Можно ли утверждать, что шестой остров действительно называется Майя?

Поиск виновных

В этом случае подсудимых четверо:

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

Кто из подсудимых виновен вне всякого сомнения, и чья вина остается под сомнением?

Искатель приключений

Предположим, что некоторый искатель приключений хочет добраться до острова сокровищ. Путешественнику предложили три карты: X, Y и Z. Только одна из карт правильная и указывает путь к острову сокровищ. В комнате, где лежали карты, находились пятеро колдунов: А, В, С, D и Е. Каждый колдун был либо рыцарем, либо лжецом и каждый дал путешественнику совет:

  • А. X— правильная карта;
  • В: У — правильная карта;
  • С: неверно, что Aw. В — оба лжеца;
  • D: либо А — лжец, либо В — рыцарь;
  • Е: либо А — лжец, либо С и D— однотипны (либо оба рыцари, либо оба лжеца).

Какая же из карт правильная?

Рубрика: Учебник по JavaScript Добавлено: admin 13.08.2004 21:27
Рeйтинг: (Голосов:3)
Просмотров:2110
Последние статьи | Последние файлы
Тестирование производительности InnoDB д... Справочное руководство по MySQL версии 5... Сверхдинамичные веб-интерфейсы О грамотном использовании БД MySQL Использование фонового изображения для з... Оценка XHTML Предохраняйся с помощью сессий Использование XML/XSL для публикации в W... 10 простых советов для начинающего PHP к... ISAPI DLL: их разработка и использование... ISAPI DLL: их разработка и использование... Обработка SimpleXML с помощью PHP Подключение к ASP.NET web сервису по про... Xml сериализация в .Net Framework 2.0 ti... Программист Delphi. Обзоры зарплат | Visual DataFlex Studio 12 Personal Report Sharp-Shooter Express 2.1 MSN Search SDK Beta 0.60 Getting Started with the XNA Creators Cl... phpMyAdmin 2.9.2 RC1 InstallAware Express 6.13 SP3 RzDBLookupComboBox (Raize Components) Un... Bluetooth Framework VCL 5.0 SharePoint Server 2007 Code Sample: Item... 2007 Office System Document: User Interf... Office Business Application for Store Op... Visual Studio 2005 Team Edition for Data... Web Service Software Factory Dec-2006 Word 2007: Rich Text Format (RTF) Specif... Windows Vista Developer Pack

Copyright © Realcoding.NET 2003-2007. При перепечатке материалов ссылка на автора материала обязательна.
Сообщить об ошибке или написать письмо администрации через форму контактов.

[AD-SIZE] [AD-SIZE] Этот сайт работает на движке CMS Shmel [AD-SIZE]