Презентация Общие сведения о формальных и аксиоматических системах

Категория: Математика


500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500500

Вы можете ознакомиться и скачать презентацию на тему Общие сведения о формальных и аксиоматических системах. Доклад-сообщение содержит 91 слайдов. Презентации для любого класса можно скачать бесплатно. Если материал и наш сайт презентаций Mypresentation Вам понравились – поделитесь им с друзьями с помощью социальных кнопок и добавьте в закладки в своем браузере.


Слайды и текст этой презентации

Слайд 1
Описание слайда:
§3. ОБЩИЕ СВЕДЕНИЯ О ФОРМАЛЬНЫХ И АКСИОМАТИЧЕСКИХ СИСТЕМАХ

Слайд 2
Описание слайда:
Определение Формальная система представляет собой совокупность чисто абстрактных объектов, не связанных с внешним миром, в которой представлены правила оперирования множеством символов только в синтаксической трактовке без учета смыслового содержания.

Слайд 3
Описание слайда:
Всякая формальная система строится на основе формализованного языка (как средства формирования и изложения выражений, имеющих смысл в данной теории) и совокупности теорем. Так же, как в естественном языке, средством выражения мысли является предложение, построенное по определенным правилам, в математике средством выражения является формула, построенная из заданного набора символов.

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

Слайд 5
Описание слайда:
Доказательство – это способ получения одних выражений из других с помощью операций над символами и построения обоснованной аргументации, следствием которой и является теорема. При построении любой формальной теории (системы) в качестве исходных посылок всегда используются некоторые неопределяемые термины и аксиомы.

Слайд 6
Описание слайда:
Неопределяемые термины – это те термины и понятия, смысл и содержание которых считается уже известным, и через них вводятся все новые понятия и термины. Совершенно аналогично вводится некоторая часть постулатов (формул), которые, как считается в данной теории, не требуют доказательства.

Слайд 7
Описание слайда:
Обычно это утверждения, правильность которых не вызывает сомнения, и они принимаются как очевидные истины. Такие выражения называют аксиомами, а системы, в основе построения которых лежит использование аксиом, называются аксиоматическими системами.

Слайд 8
Описание слайда:
Определение формальной системы осуществляется в следующем порядке: Определение формальной системы осуществляется в следующем порядке: 1. Задается конечное множество символов, которые образуют алфавит формальной системы. 2. Устанавливаются процедуры построения формул формальной системы.

Слайд 9
Описание слайда:
3. Устанавливается множество аксиом, т.е. формул, истинность которых не требует доказательства. Обычно к ним относят те утверждения, которые полагаются очевидными по самой природе рассматриваемых понятий. 3. Устанавливается множество аксиом, т.е. формул, истинность которых не требует доказательства. Обычно к ним относят те утверждения, которые полагаются очевидными по самой природе рассматриваемых понятий. 4. Устанавливается конечное множество правил вывода, которые позволяют получать новые формулы из некоторого множества известных формул.

Слайд 10
Описание слайда:
В общем случае эти правила могут быть представлены в следующем виде В общем случае эти правила могут быть представлены в следующем виде что означает: из множества истинных формул указанных в левой части выражения, следует истинность формул правой части выражения. Говорят, что формула М, полученная в результате применения правила вывода, выводима в данной теории.

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

Слайд 12
Описание слайда:
Задаваемые при описании формальной системы правила вывода называют также правилами вывода заключений, т.е. они позволяют определить, является ли данная формула теоремой данной формальной системы или нет.

Слайд 13
Описание слайда:
Различают два типа правил вывода. 1. Правила, применяемые к формулам, рассматриваемым как единое целое, в этом случае их называют продукционными правилами. Пример. x < y и y < z, следовательно x < z  это продукция с двумя посылками.

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

Слайд 15
Описание слайда:
Определение Правило подстановки заключается в замещении всех вхождений какой-либо переменной на формулу из формальной системы, которая не содержит этой переменной.

Слайд 16
Описание слайда:
Пример Рассмотрим формальную систему следующего вида: Алфавит = {a, b, w}. Формулы  символ или последовательность символов a, b или w. Аксиома awa. Правило вывода (продукция). с1 w с2 -> b с1 w с2 b

Слайд 17
Описание слайда:
Символы с1 и с2 не принадлежат алфавиту формальной системы (ФС), они служат посредниками для формализации правил вывода. То есть с1 и с2 обозначают какие-либо последовательности символов a или b формальной системы и могут быть замещены любыми последовательностями символов a или b. Учитывая способ образования формул, можно сказать, что незамещаемые символы a и b называются константами, а символ w - оператором.

Слайд 18
Описание слайда:
Из определения ФС вытекает и способ получения допустимых формул, т.е. формул, выводимых согласно правилу вывода путем его последовательного применения к аксиоме: Из определения ФС вытекает и способ получения допустимых формул, т.е. формул, выводимых согласно правилу вывода путем его последовательного применения к аксиоме: awa bawab bbawabb bbbawabbb и т.д.

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

Слайд 20
Описание слайда:
Определение Интерпретация представляет собой распространение исходных положений какой-либо формальной системы на реальный мир. Интерпретация придает смысл каждому символу формальной системы и устанавливает взаимно однозначное соответствие между символами формальной системы и реальными объектами.

Слайд 21
Описание слайда:
Теоремы формальной системы, будучи интерпретированы, становятся после этого утверждениями в обычном смысле слова, и в этом случае уже можно делать выводы об их истинности или ложности.

Слайд 22
Описание слайда:
Следует отметить, что при интерпретации речь идет о замыкании или логическом завершении математического подхода, который в общем случае можно описать в виде следующей последовательности действий:

Слайд 23
Описание слайда:
1. Математик изучает реальность, конструируя некоторое абстрактное представление о ней, т.е. некоторую формальную систему. 1. Математик изучает реальность, конструируя некоторое абстрактное представление о ней, т.е. некоторую формальную систему. 2. Строится доказательство теорем формальной системы. Вся польза и удобства формальных систем заключаются в их абстрагировании от конкретной реальности. Благодаря этому одна и та же формальная система может служить моделью многочисленных различных конкретных ситуаций.

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

Слайд 25
Описание слайда:
Замечание Изучение аксиом и теорем как абстрактных выражений, представленных в некоторой форме, называется синтаксическим изучением аксиоматических систем (АС); изучение и рассмотрение смысла этих выражений называется семантическим изучением АС. С синтаксическим аспектом АС и связано понятие формальной системы.

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

Слайд 27
Описание слайда:
1. Проблема противоречивости. Логическое исчисление называется непротиворечивым, если в нем недоказуемы никакие две формулы, из которых одна является отрицанием другой. 2. Проблема полноты. Система исчисления считается полной, если любая теорема теории может быть доказана или опровергнута.

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

Слайд 29
Описание слайда:
§4. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ

Слайд 30
Описание слайда:
Определение Исчисление высказываний (ИВ), т.е. логика высказываний – это формальная система, интерпретацией которой является алгебра высказываний. Под высказыванием понимается повествовательное предложение, о котором можно сказать, что оно истинно или ложно.

Слайд 31
Описание слайда:
Как и любая формальная система, исчисление высказываний строится на основе четырех основных процедур: 1. Задания алфавита. 2. Установления правил построения формул. 3. Определение аксиом. 4. Определение правил вывода.

Слайд 32
Описание слайда:
Алфавит, который состоит из символов трех категорий: Алфавит, который состоит из символов трех категорий: а) бесконечное счетное множество высказываний (или переменных высказываний), которые обычно обозначаются буквами: x, y, z, a, b, c, x10, y1, , и т.д.; б) логические операторы (или логические связки), которые обозначают символы логических операций (v, &, и т.д.); в) открывающиеся и закрывающиеся скобки: ( , ) . Других символов в ИВ нет!!!

Слайд 33
Описание слайда:
Формулы в исчислении высказываний однозначно получаются с помощью правил, которые описываются базисом и индуктивным шагом: Формулы в исчислении высказываний однозначно получаются с помощью правил, которые описываются базисом и индуктивным шагом: базис: всякое высказывание есть формула; индуктивный шаг: если X и Y  формулы, то , , , также формулы. Никакая другая последовательность символов не является формулой!!!

Слайд 34
Описание слайда:
Пример. Если x, y, z  формулы в соответствии с правилом базиса, то (x->y), (x&z) и т.д.  формулы в соответствии с правилом индуктивного шага. Очевидно, что не будут формулами: &x, (x&z, т.к. они не удовлетворяют вышеуказанным правилам. В первом случае в бинарной операции используется один операнд, а во втором  отсутствует закрывающая скобка!!!

Слайд 35
Описание слайда:
С введением понятия формулы вводится и понятие подформулы или части формулы, делается это следующим образом. С введением понятия формулы вводится и понятие подформулы или части формулы, делается это следующим образом. Подформулой элементарной формулы является только она сама. Если X - формула, то ее подформулами будут: она сама, X и все подформулы X. Обозначим w  любую из логических операций (v, &, -> и т.д.), кроме отрицания. Тогда, если (XwY)  формула, то ее подформулы: она сама, формулы X и Y и все подформулы X и Y.

Слайд 36
Описание слайда:
Пример. Пусть задана формула , определим ее подформулы и глубину их вложенности.

Слайд 37
Описание слайда:
Кроме табличной формы каждая правильная формула может быть представлена в виде дерева, ветви которого – исходные и промежуточные формулы

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

Слайд 39
Описание слайда:
Существует несколько вариантов подбора аксиом как исходных тождественно истинных формул. Эти наборы эквивалентны в том смысле, что они определяют один и тот же класс выводимых формул.

Слайд 40
Описание слайда:

Слайд 41
Описание слайда:
Тождественную истинность аксиом можно проверить либо прямым вычислением значения формулы на каждом наборе, либо приведением их к константе 1 путем эквивалентных преобразований, применяемых в булевой алгебре.

Слайд 42
Описание слайда:
Пример

Слайд 43
Описание слайда:
Правила вывода устанавливают отношения на множестве формул исчисления высказываний. Правила вывода обычно представляются как отношения на множестве формул исчисления высказываний. Над чертой записываются формулы, которые играют роль посылки (уже известные истинные выражения), а под чертой – выводимая формула, истинность которой утверждается данным правилом. Она называется следствием или заключением.

Слайд 44
Описание слайда:
В исчислении высказываний используется два правила вывода: В исчислении высказываний используется два правила вывода: правило заключения (modus ponens). Если A и  это выводимые формулы, то B также является выводимой формулой. Записывается это правило так:

Слайд 45
Описание слайда:
2) правило подстановки. где - это формулы,  попарно различные переменные высказывания; через запись обозначен результат одновременной замены всех вхождений переменных в A на формулы

Слайд 46
Описание слайда:
Справедливость правил вывода исчисления высказываний подтверждается применением методов булевой алгебры. Справедливость правил вывода исчисления высказываний подтверждается применением методов булевой алгебры. В частности, тождественную истинность выводимой формулы В можно установить следующим образом: если А и А → В  тождественно истинные формулы, то есть А = 1 и А → В = 1, следовательно Так как в последнем выражении = 0, а значение логической суммы равно 1, то В должно быть равно 1 (то есть быть истинным).

Слайд 47
Описание слайда:
Кроме двух приведенных выше правил вывода, можно получить и другие правила, позволяющие строить новые доказуемые формулы. Но так как они реализуются с помощью правила подстановки и заключения, то они получили название производных правил вывода.

Слайд 48
Описание слайда:
Правило сложного заключения. Если  формулы и  теорема, то формула B  также теорема. Правило двойного отрицания Если и  теоремы, то будет теоремой и формула иначе и

Слайд 49
Описание слайда:
Правило силлогизма (замыкания). Правило силлогизма (замыкания). Если и  теоремы, то также теорема, иначе Правило композиции. Если теорема, то так же теорема, иначе

Слайд 50
Описание слайда:
Правила вывода можно рассматривать и как результат логического анализа некоторых человеческих рассуждений. Рассмотрим примеры для приведенных выше правил.

Слайд 51
Описание слайда:
Правило заключения ИСХОДНЫЕ ПОСЫЛКИ. Если данный многоугольник правильный (А=1), то в него можно вписать окружность (А → В). Возьмем правильный многоугольник (А=1). ВЫВОД. В данный многоугольник можно вписать окружность (В = 1).

Слайд 52
Описание слайда:
Правило силлогизма ИСХОДНЫЕ ПОСЫЛКИ. Если треугольник равнобедренный (А = 1), то две его стороны равны (В = 1), т.е. А → В. Если две стороны треугольника равны (В = 1), то два его угла равны (С = 1), т.е. В → С. ВЫВОД. Если треугольник равнобедренный, то два его угла равны (А→С).

Слайд 53
Описание слайда:
Как отмечалось выше, формулы исчисления высказываний можно интерпретировать как формулы алгебры высказываний (АВ). Для этого следует переменные ИВ трактовать как переменные АВ, т.е. переменные, которые могут принимать только значение 0 и 1 (ложь и истина). Все логические операции (, ,  и т.д.), которые используются в ИВ, интерпретируются так же, как и в АВ, т.е. на основе тех же самых таблиц истинности. Очевидно, что между формулами ИВ и АВ существует взаимнооднозначное соответствие.

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

Слайд 55
Описание слайда:
Определение. Формула выполнима, если она может принимать значение «истина» (например, Определение. Формула выполнима, если она может принимать значение «истина» (например, ) Определение. Формула невыполнима, если ни при каких значениях составляющих ее высказываний она не может быть истинной (например, ). Определение. Формула общезначима, если она принимает значение «истина» независимо от истинности ее составляющих (например, ). Определение. Формула нейтральна, если она не общезначима и не является невыполнимой.

Слайд 56
Описание слайда:
Определение. Тавтологиями называются общезначимые формулы. Если формула А≡1, т.е. А – тавтология, то это можно записать так

Слайд 57
Описание слайда:
Определение (Логический вывод на основе множества гипотез). Пусть E – это множество формул, тогда запись означает, что если все формулы из Е истинны, то будет истинной формула А. В этом случае А – называется логическим следствием из Е. Если и E|=A , то можно записать Формулы называются гипотезами, а формула А – заключением.

Слайд 58
Описание слайда:
Определение. Принцип дедукции состоит в следующем. Формула A является логическим следствием конечного множества Е тогда и только тогда, когда содержит невыполнимые формулы.

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

Слайд 60
Описание слайда:
Действительно, если А есть логическое следствие гипотез ,то, учитывая сформулированный выше принцип дедукции, можно считать справедливой следующую запись: Это правило называется правилом прямой дедукции. Возьмем отрицание от этого выражения, тогда по правилу де Моргана получим Это правило называется правилом обратной дедукции.

Слайд 61
Описание слайда:
МЕТОДЫ, ИСПОЛЬЗУЕМЫЕ ДЛЯ ОПРЕДЕЛЕНИЯ ОБЩЕЗНАЧИМОСТИ ФОРМУЛ ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ

Слайд 62
Описание слайда:
Алгоритм редукции. Этот алгоритм позволяет доказывать общезначимость формул исчисления высказываний путем приведения к абсурду. Рассмотрим на примере. Пусть требуется доказать общезначимость следующей формулы: Алгоритм редукции. Этот алгоритм позволяет доказывать общезначимость формул исчисления высказываний путем приведения к абсурду. Рассмотрим на примере. Пусть требуется доказать общезначимость следующей формулы:

Слайд 63
Описание слайда:
Предположим, что при некоторой интерпретации эта формула принимает значение «ложь». Из определения функции импликации известно, что значение «ложь» она принимает только в том случае, когда посылка истинна, а заключение ложно. Учитывая указанное свойство, представляем исходную формулу в виде двух интерпретаций следующего вида: Предположим, что при некоторой интерпретации эта формула принимает значение «ложь». Из определения функции импликации известно, что значение «ложь» она принимает только в том случае, когда посылка истинна, а заключение ложно. Учитывая указанное свойство, представляем исходную формулу в виде двух интерпретаций следующего вида:

Слайд 64
Описание слайда:
Применив ранее использованные рассуждения к первой строке, получим следующие значения переменных: Применив ранее использованные рассуждения к первой строке, получим следующие значения переменных: Если подставить полученные значения во вторую строку, то получится противоречие. Значит, предположение о том, что существует некоторая интерпретация, при которой исходная формула принимает значение «ложь», неверно, и это означает общезначимость исходной формулы.

Слайд 65
Описание слайда:
Пример. Используя алгоритм редукции, доказать общезначимость следующей формулы: Пример. Используя алгоритм редукции, доказать общезначимость следующей формулы: Пусть при некоторой интерпретации Это возможно только, если

Слайд 66
Описание слайда:
Тогда из первой формулы следует, что возможна одна из следующих комбинаций значений переменных a и b:

Слайд 67
Описание слайда:
Из второй формулы следует Из второй формулы следует это означает, что возможны следующие значения c и a:

Слайд 68
Описание слайда:
Из имеем c=1, b=0. Это единственно допустимые для c и b значения, при которых формула принимает значение «ложь». Сопоставляем полученные результаты с ранее рассмотренными возможными значениями переменных. Оказывается, что при с=1 единственное допустимое значение для a  это a=1, а при b=0 единственное допустимое значение a=0. Из имеем c=1, b=0. Это единственно допустимые для c и b значения, при которых формула принимает значение «ложь». Сопоставляем полученные результаты с ранее рассмотренными возможными значениями переменных. Оказывается, что при с=1 единственное допустимое значение для a  это a=1, а при b=0 единственное допустимое значение a=0. То есть переменная a должна принимать взаимно исключающие значения, что невозможно. Следовательно, предположение о существовании интерпретации, при которой формула принимает значение «ложь» неверно и это означает ее общезначимость.

Слайд 69
Описание слайда:
Метод резолюций. Для порождения логических следствий будет использована очень простая схема рассуждений. Пусть A, B и X – формулы. Предположим, что две формулы истинны. Тогда, если X истина, то отсюда следует, что B тоже истина. Наоборот, если X – ложь, то следует, что A – истина. Получаем правило Метод резолюций. Для порождения логических следствий будет использована очень простая схема рассуждений. Пусть A, B и X – формулы. Предположим, что две формулы истинны. Тогда, если X истина, то отсюда следует, что B тоже истина. Наоборот, если X – ложь, то следует, что A – истина. Получаем правило , которое можно записать в виде .

Слайд 70
Описание слайда:
В том частном случае, когда X – высказывание, а A и B – дизъюнкты, это правило называется правилом резолюций. В том частном случае, когда X – высказывание, а A и B – дизъюнкты, это правило называется правилом резолюций. Рассмотрим, каким образом это правило может быть использовано для построения доказательства. В методе резолюций применяется также приведенное выше правило прямой дедукции: для того чтобы доказать, что формула С является логическим следствием из гипотез H1,H2,…,Hn, следует доказать, что H1&H2&…&Hn& =0.

Слайд 71
Описание слайда:
Так как левая часть последнего равенства представляет собой конъюнкцию, для его выполнения достаточно доказать равенство нулю любой входящей в уравнение формулы. Так как левая часть последнего равенства представляет собой конъюнкцию, для его выполнения достаточно доказать равенство нулю любой входящей в уравнение формулы. Таким образом, для доказательства выводимости исходной формулы С необходимо доказать, что в множестве {H1,H2,…,Hn, } имеется хотя бы одна невыполнимая формула. Для этого каждый элемент указанного множества рассматривается как элементарная дизъюнкция (дизъюнкт).

Слайд 72
Описание слайда:
Применение метода резолюций предусматривает порождение новых дизъюнктов на основе следующей леммы, в основе которой лежит правило резолюций. Применение метода резолюций предусматривает порождение новых дизъюнктов на основе следующей леммы, в основе которой лежит правило резолюций. Лемма. Пусть S1 и S2 – дизъюнкты нормальной формы S, а l – литера. Если и , то дизъюнкт является логическим следствием нормальной формы S. Следствие. Нормальные формы S и эквивалентны. Замечание. Дизъюнкт r называется резольвентой дизъюнктов S1 и S2 .

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

Слайд 74
Описание слайда:
Таким образом, принцип резолюций заключается в использовании того факта, что множество дизъюнктов S не выполнимо, если пустой дизъюнкт является логическим следствием из него. То есть, для доказательства невыполнимости множества S необходимо строить логические следствия из него до тех пор, пока не будет получен пустой дизъюнкт или дальнейшее построение логических следствий окажется невозможным. Таким образом, принцип резолюций заключается в использовании того факта, что множество дизъюнктов S не выполнимо, если пустой дизъюнкт является логическим следствием из него. То есть, для доказательства невыполнимости множества S необходимо строить логические следствия из него до тех пор, пока не будет получен пустой дизъюнкт или дальнейшее построение логических следствий окажется невозможным.

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

Слайд 76
Описание слайда:
Определение. Литера  это элементарное высказывание или его отрицание. Например, Определение. Литера  это элементарное высказывание или его отрицание. Например, . Определение. Дизъюнкт или элементарная дизъюнкция  это совокупность различных литер, связанных дизъюнктивной связью. Например, . Определение. Конъюнктивной нормальной формой (КНФ) некоторой формулы называется равносильная ей формула, представляющая конъюнкций элементарных дизъюнкций. Например, .

Слайд 77
Описание слайда:
Так как для того, чтобы выражение в форме КНФ было тождественно истинным, необходимо и достаточно, чтобы был истиной каждый дизъюнкт в него входящий, то при построении логического вывода можно перейти от КНФ к множеству дизъюнктов, в котором каждый элемент множества имеет значение «истинно». Так как для того, чтобы выражение в форме КНФ было тождественно истинным, необходимо и достаточно, чтобы был истиной каждый дизъюнкт в него входящий, то при построении логического вывода можно перейти от КНФ к множеству дизъюнктов, в котором каждый элемент множества имеет значение «истинно». Определение. Пустой дизъюнкт  это такой дизъюнкт, значение которого тождественно ложно.

Слайд 78
Описание слайда:
Итак, невыполнимость формул, из которых формируется конечное множество дизъюнктов S, доказывается с помощью следующего алгоритма. Итак, невыполнимость формул, из которых формируется конечное множество дизъюнктов S, доказывается с помощью следующего алгоритма. Шаг 1. Проверка множества S на невыполнимость. Если пустой дизъюнкт принадлежит множеству S (он может либо присутствовать изначально или получается из-за того, что в множестве одновременно присутствует некоторая литера и ее отрицание), это означает, что множество S невыполнимо и алгоритм свою работу закончил. Иначе переходим на шаг 2.

Слайд 79
Описание слайда:
Шаг 2. Построение резольвенты. Выбираем l, S1, S2, такие, что и и вычисляем резольвенту r. Если невозможно выбрать l, S1, S2, соответствующие указанным условиям, то алгоритм свою работу закончил и можно сказать, что исходное множество выполнимо. Иначе переходим на шаг 3. Шаг 2. Построение резольвенты. Выбираем l, S1, S2, такие, что и и вычисляем резольвенту r. Если невозможно выбрать l, S1, S2, соответствующие указанным условиям, то алгоритм свою работу закончил и можно сказать, что исходное множество выполнимо. Иначе переходим на шаг 3.

Слайд 80
Описание слайда:
Шаг 3. Обновление множества дизъюнктов. Заменяем множество дизъюнктов , т.е. добавляем к существующим дизъюнктам новый дизъюнкт  резольвенту, полученную на предыдущем шаге. После чего переходим на шаг 1.

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

Слайд 82
Описание слайда:
Порождаем логические следствия, при порождении следствия будем указывать, номера участвовавших в построении дизъюнктов: Порождаем логические следствия, при порождении следствия будем указывать, номера участвовавших в построении дизъюнктов:

Слайд 83
Описание слайда:
Замечание. Алгоритм проверки невыполнимости недетерминирован. Вообще говоря, возможен не один вариант выбора значений для l, S1 и S2. В приведенном примере дизъюнкты выбирались в лексико-графическом порядке номеров. Такая стратегия не оптимальна, так как некоторые резольвенты оказались не нужны, а также вычислялись более одного раза. Этот же пример с минимумом резолюций будет выглядеть так: Замечание. Алгоритм проверки невыполнимости недетерминирован. Вообще говоря, возможен не один вариант выбора значений для l, S1 и S2. В приведенном примере дизъюнкты выбирались в лексико-графическом порядке номеров. Такая стратегия не оптимальна, так как некоторые резольвенты оказались не нужны, а также вычислялись более одного раза. Этот же пример с минимумом резолюций будет выглядеть так: Ясно, что принятая стратегия может существенно влиять на процесс выполнения алгоритма. Тем не менее существуют два свойства, не зависящие от используемой стратегии.

Слайд 84
Описание слайда:
Свойство 1. Если множество S не содержит ни одной пары дизъюнктов, допускающих резольвенту, то оно выполнимо (за исключением случая, когда оно содержит пустой дизъюнкт). Свойство 2. Если выполнение этого алгоритма закончилось нормально после порождения пустого дизъюнкта, то установлена невыполнимость исходного множества S. В заключение рассмотрим несколько примеров применения метода резолюций в логике высказываний.

Слайд 85
Описание слайда:
Пример. Доказать, используя метод резолюций, что S является логическим следствием множества гипотез H, где Пример. Доказать, используя метод резолюций, что S является логическим следствием множества гипотез H, где , а . Сначала преобразуем множество гипотез в множество дизъюнктов:

Слайд 86
Описание слайда:
Для доказательства того, что H |= S необходимо и достаточно доказать невыполнимость следующего множества дизъюнктов Для доказательства того, что H |= S необходимо и достаточно доказать невыполнимость следующего множества дизъюнктов

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

Слайд 88
Описание слайда:
Введем следующие обозначения для высказываний: Введем следующие обозначения для высказываний: g – встать рано; d – играть в преферанс; с – идти на первую пару; s – лечь поздно спать; e – мало спать. Используя введенные обозначения, перейдем от утверждений к следующему набору гипотез: , , .

Слайд 89
Описание слайда:
Следствие примет вид . При построении доказательства по дедукции в качестве механизма воспользуемся методом эквивалентных преобразований и методом резолюций. Требуется доказать невыполнимость следующего множества: Следствие примет вид . При построении доказательства по дедукции в качестве механизма воспользуемся методом эквивалентных преобразований и методом резолюций. Требуется доказать невыполнимость следующего множества: , где . Используя метод эквивалентных преобразований, требуется доказать, что имеет место равенство . Докажем, что

Слайд 90
Описание слайда:
Теперь построим доказательство, используя метод резолюций. Для этого приведем имеющиеся гипотезы к форме дизъюнктов: Теперь построим доказательство, используя метод резолюций. Для этого приведем имеющиеся гипотезы к форме дизъюнктов: Отрицание следствия будет иметь вид , а цепочка доказательства:

Слайд 91
Описание слайда:



Похожие презентации

Mypresentation.ru

Загрузить презентацию