Презентация «Общие сведения о формальных и аксиоматических системах»
Смотреть слайды в полном размере 
Вы можете ознакомиться с презентацией онлайн, просмотреть текст и слайды к ней, а также, в случае, если она вам подходит - скачать файл для редактирования или печати. Документ содержит 91 слайд и доступен в формате ppt. Размер файла: 1.91 MB
Pic.1
§3. ОБЩИЕ СВЕДЕНИЯ О ФОРМАЛЬНЫХ И АКСИОМАТИЧЕСКИХ СИСТЕМАХ
Pic.2
Определение Формальная система представляет собой совокупность чисто абстрактных объектов, не связанных с внешним миром, в которой представлены правила оперирования множеством символов только в …
Pic.3
Всякая формальная система строится на основе формализованного языка (как средства формирования и изложения выражений, имеющих смысл в данной теории) и совокупности теорем. Так же, как в естественном …
Pic.4
В формальной теории все формулы доказываются. Под теоремой в формальной системе понимают высказывание, истинное в данной системе, это некоторое обоснованное и строгое утверждение, которое строится …
Pic.5
Доказательство – это способ получения одних выражений из других с помощью операций над символами и построения обоснованной аргументации, следствием которой и является теорема. При построении любой …
Pic.6
Неопределяемые термины – это те термины и понятия, смысл и содержание которых считается уже известным, и через них вводятся все новые понятия и термины. Совершенно аналогично вводится некоторая часть …
Pic.7
Обычно это утверждения, правильность которых не вызывает сомнения, и они принимаются как очевидные истины. Такие выражения называют аксиомами, а системы, в основе построения которых лежит …
Pic.8
Определение формальной системы осуществляется в следующем порядке: Определение формальной системы осуществляется в следующем порядке: 1. Задается конечное множество символов, которые образуют алфавит …
Pic.9
3. Устанавливается множество аксиом, т. е. формул, истинность которых не требует доказательства. Обычно к ним относят те утверждения, которые полагаются очевидными по самой природе рассматриваемых …
Pic.10
В общем случае эти правила могут быть представлены в следующем виде В общем случае эти правила могут быть представлены в следующем виде что означает: из множества истинных формул указанных в левой …
Pic.11
Определение Формальным доказательством, или просто доказательством, называется последовательность формул такая, что каждая формула является либо аксиомой, либо выводима из предшествующих ей формул . …
Pic.12
Задаваемые при описании формальной системы правила вывода называют также правилами вывода заключений, т. е. они позволяют определить, является ли данная формула теоремой данной формальной системы или …
Pic.13
Различают два типа правил вывода. 1. Правила, применяемые к формулам, рассматриваемым как единое целое, в этом случае их называют продукционными правилами. Пример. x < y и y < z, следовательно …
Pic.14
2. Правила, которые могут применяться к любой отдельной части формулы, причем сами эти части являются формулами, входящими в состав формальной системы. В этом случае их называют правилами …
Pic.15
Определение Правило подстановки заключается в замещении всех вхождений какой-либо переменной на формулу из формальной системы, которая не содержит этой переменной.
Pic.16
Пример Рассмотрим формальную систему следующего вида: Алфавит = {a, b, w}. Формулы символ или последовательность символов a, b или w. Аксиома awa. Правило вывода (продукция). с1 w с2 -> b с1 w …
Pic.17
Символы с1 и с2 не принадлежат алфавиту формальной системы (ФС), они служат посредниками для формализации правил вывода. То есть с1 и с2 обозначают какие-либо последовательности символов a или b …
Pic.18
Из определения ФС вытекает и способ получения допустимых формул, т. е. формул, выводимых согласно правилу вывода путем его последовательного применения к аксиоме: Из определения ФС вытекает и способ …
Pic.19
Определение Формальная система называется разрешимой, если существует хорошо определенный способ действия, который за конечное число шагов для любой формулы формальной системы позволяет определить …
Pic.20
Определение Интерпретация представляет собой распространение исходных положений какой-либо формальной системы на реальный мир. Интерпретация придает смысл каждому символу формальной системы и …
Pic.21
Теоремы формальной системы, будучи интерпретированы, становятся после этого утверждениями в обычном смысле слова, и в этом случае уже можно делать выводы об их истинности или ложности.
Pic.22
Следует отметить, что при интерпретации речь идет о замыкании или логическом завершении математического подхода, который в общем случае можно описать в виде следующей последовательности действий:
Pic.23
1. Математик изучает реальность, конструируя некоторое абстрактное представление о ней, т. е. некоторую формальную систему. 1. Математик изучает реальность, конструируя некоторое абстрактное …
Pic.24
3. Происходит возвращение к начальной точке всего построения и осуществляется интерпретация теорем, полученных при формализации. 3. Происходит возвращение к начальной точке всего построения и …
Pic.25
Замечание Изучение аксиом и теорем как абстрактных выражений, представленных в некоторой форме, называется синтаксическим изучением аксиоматических систем (АС); изучение и рассмотрение смысла этих …
Pic.26
Формальную теорию часто называют исчислением. Под исчислением понимают формальное представление теории, которое позволяет оперировать с объектами без учета формального смысла выражений. В рамках …
Pic.27
1. Проблема противоречивости. Логическое исчисление называется непротиворечивым, если в нем недоказуемы никакие две формулы, из которых одна является отрицанием другой. 2. Проблема полноты. Система …
Pic.28
3. Проблема независимости аксиом. Для начала введем понятие независимой аксиомы. Аксиома называется независимой, если она не может быть выведена из других аксиом. Система аксиом исчисления называется …
Pic.29
§4. ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ
Pic.30
Определение Исчисление высказываний (ИВ), т. е. логика высказываний – это формальная система, интерпретацией которой является алгебра высказываний. Под высказыванием понимается повествовательное …
Pic.31
Как и любая формальная система, исчисление высказываний строится на основе четырех основных процедур: 1. Задания алфавита. 2. Установления правил построения формул. 3. Определение аксиом. 4. …
Pic.32
Алфавит, который состоит из символов трех категорий: Алфавит, который состоит из символов трех категорий: а) бесконечное счетное множество высказываний (или переменных высказываний), которые обычно …
Pic.33
Формулы в исчислении высказываний однозначно получаются с помощью правил, которые описываются базисом и индуктивным шагом: Формулы в исчислении высказываний однозначно получаются с помощью правил, …
Pic.34
Пример. Если x, y, z формулы в соответствии с правилом базиса, то (x->y), (x&z) и т. д. формулы в соответствии с правилом индуктивного шага. Очевидно, что не будут формулами: &x, …
Pic.35
С введением понятия формулы вводится и понятие подформулы или части формулы, делается это следующим образом. С введением понятия формулы вводится и понятие подформулы или части формулы, делается это …
Pic.36
Пример. Пусть задана формула , определим ее подформулы и глубину их вложенности.
Pic.37
Кроме табличной формы каждая правильная формула может быть представлена в виде дерева, ветви которого – исходные и промежуточные формулы
Pic.38
Для упрощения записи формул ИВ используются те же соглашения, что и в алгебре логики, которые позволяют учитывать приоритеты операций и избавиться от излишних скобок. Пример.
Pic.39
Существует несколько вариантов подбора аксиом как исходных тождественно истинных формул. Эти наборы эквивалентны в том смысле, что они определяют один и тот же класс выводимых формул.
Pic.40
Pic.41
Тождественную истинность аксиом можно проверить либо прямым вычислением значения формулы на каждом наборе, либо приведением их к константе 1 путем эквивалентных преобразований, применяемых в булевой …
Pic.42
Пример
Pic.43
Правила вывода устанавливают отношения на множестве формул исчисления высказываний. Правила вывода обычно представляются как отношения на множестве формул исчисления высказываний. Над чертой …
Pic.44
В исчислении высказываний используется два правила вывода: В исчислении высказываний используется два правила вывода: правило заключения (modus ponens). Если A и это выводимые формулы, то B также …
Pic.45
2) правило подстановки. где - это формулы, попарно различные переменные высказывания; через запись обозначен результат одновременной замены всех вхождений переменных в A на формулы
Pic.46
Справедливость правил вывода исчисления высказываний подтверждается применением методов булевой алгебры. Справедливость правил вывода исчисления высказываний подтверждается применением методов …
Pic.47
Кроме двух приведенных выше правил вывода, можно получить и другие правила, позволяющие строить новые доказуемые формулы. Но так как они реализуются с помощью правила подстановки и заключения, то они …
Pic.48
Правило сложного заключения. Если формулы и теорема, то формула B также теорема. Правило двойного отрицания Если и теоремы, то будет теоремой и формула иначе и
Pic.49
Правило силлогизма (замыкания). Правило силлогизма (замыкания). Если и теоремы, то также теорема, иначе Правило композиции. Если теорема, то так же теорема, иначе
Pic.50
Правила вывода можно рассматривать и как результат логического анализа некоторых человеческих рассуждений. Рассмотрим примеры для приведенных выше правил.
Pic.51
Правило заключения ИСХОДНЫЕ ПОСЫЛКИ. Если данный многоугольник правильный (А=1), то в него можно вписать окружность (А → В). Возьмем правильный многоугольник (А=1). ВЫВОД. В данный многоугольник …
Pic.52
Правило силлогизма ИСХОДНЫЕ ПОСЫЛКИ. Если треугольник равнобедренный (А = 1), то две его стороны равны (В = 1), т. е. А → В. Если две стороны треугольника равны (В = 1), то два его угла равны (С = …
Pic.53
Как отмечалось выше, формулы исчисления высказываний можно интерпретировать как формулы алгебры высказываний (АВ). Для этого следует переменные ИВ трактовать как переменные АВ, т. е. переменные, …
Pic.54
Однако формализма, реализованного в АВ, не всегда достаточно для реализации построения доказательств в ИВ, поэтому существует и множество других методов. Перед рассмотрением методов установления …
Pic.55
Определение. Формула выполнима, если она может принимать значение «истина» (например, Определение. Формула выполнима, если она может принимать значение «истина» (например, ) Определение. Формула …
Pic.56
Определение. Тавтологиями называются общезначимые формулы. Если формула А≡1, т. е. А – тавтология, то это можно записать так
Pic.57
Определение (Логический вывод на основе множества гипотез). Пусть E – это множество формул, тогда запись означает, что если все формулы из Е истинны, то будет истинной формула А. В этом случае А – …
Pic.58
Определение. Принцип дедукции состоит в следующем. Формула A является логическим следствием конечного множества Е тогда и только тогда, когда содержит невыполнимые формулы.
Pic.59
В силу того, что для высказываний справедливы все свойства логических операций, которые были определены в алгебре логики, то, используя законы де Моргана, можно ввести понятие прямой и обратной …
Pic.60
Действительно, если А есть логическое следствие гипотез ,то, учитывая сформулированный выше принцип дедукции, можно считать справедливой следующую запись: Это правило называется правилом прямой …
Pic.61
МЕТОДЫ, ИСПОЛЬЗУЕМЫЕ ДЛЯ ОПРЕДЕЛЕНИЯ ОБЩЕЗНАЧИМОСТИ ФОРМУЛ ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ
Pic.62
Алгоритм редукции. Этот алгоритм позволяет доказывать общезначимость формул исчисления высказываний путем приведения к абсурду. Рассмотрим на примере. Пусть требуется доказать общезначимость …
Pic.63
Предположим, что при некоторой интерпретации эта формула принимает значение «ложь». Из определения функции импликации известно, что значение «ложь» она принимает только в том случае, когда посылка …
Pic.64
Применив ранее использованные рассуждения к первой строке, получим следующие значения переменных: Применив ранее использованные рассуждения к первой строке, получим следующие значения переменных: …
Pic.65
Пример. Используя алгоритм редукции, доказать общезначимость следующей формулы: Пример. Используя алгоритм редукции, доказать общезначимость следующей формулы: Пусть при некоторой интерпретации Это …
Pic.66
Тогда из первой формулы следует, что возможна одна из следующих комбинаций значений переменных a и b:
Pic.67
Из второй формулы следует Из второй формулы следует это означает, что возможны следующие значения c и a:
Pic.68
Из имеем c=1, b=0. Это единственно допустимые для c и b значения, при которых формула принимает значение «ложь». Сопоставляем полученные результаты с ранее рассмотренными возможными значениями …
Pic.69
Метод резолюций. Для порождения логических следствий будет использована очень простая схема рассуждений. Пусть A, B и X – формулы. Предположим, что две формулы истинны. Тогда, если X истина, то …
Pic.70
В том частном случае, когда X – высказывание, а A и B – дизъюнкты, это правило называется правилом резолюций. В том частном случае, когда X – высказывание, а A и B – дизъюнкты, это правило называется …
Pic.71
Так как левая часть последнего равенства представляет собой конъюнкцию, для его выполнения достаточно доказать равенство нулю любой входящей в уравнение формулы. Так как левая часть последнего …
Pic.72
Применение метода резолюций предусматривает порождение новых дизъюнктов на основе следующей леммы, в основе которой лежит правило резолюций. Применение метода резолюций предусматривает порождение …
Pic.73
Для доказательства приведенных выше утверждений о выполнимости формулы С необходимо, как отмечалось выше, доказать, что хотя бы один дизъюнкт из рассматриваемого множества исходных и порожденных …
Pic.74
Таким образом, принцип резолюций заключается в использовании того факта, что множество дизъюнктов S не выполнимо, если пустой дизъюнкт является логическим следствием из него. То есть, для …
Pic.75
Метод резолюций выгодно отличается от других методов тем, что он дает возможность использовать средства автоматического доказательства, применяемые в логическом программировании. Метод резолюций …
Pic.76
Определение. Литера это элементарное высказывание или его отрицание. Например, Определение. Литера это элементарное высказывание или его отрицание. Например, . Определение. Дизъюнкт или …
Pic.77
Так как для того, чтобы выражение в форме КНФ было тождественно истинным, необходимо и достаточно, чтобы был истиной каждый дизъюнкт в него входящий, то при построении логического вывода можно …
Pic.78
Итак, невыполнимость формул, из которых формируется конечное множество дизъюнктов S, доказывается с помощью следующего алгоритма. Итак, невыполнимость формул, из которых формируется конечное …
Pic.79
Шаг 2. Построение резольвенты. Выбираем l, S1, S2, такие, что и и вычисляем резольвенту r. Если невозможно выбрать l, S1, S2, соответствующие указанным условиям, то алгоритм свою работу закончил и …
Pic.80
Шаг 3. Обновление множества дизъюнктов. Заменяем множество дизъюнктов , т. е. добавляем к существующим дизъюнктам новый дизъюнкт резольвенту, полученную на предыдущем шаге. После чего переходим на …
Pic.81
Пример. Доказать, используя метод резолюций, невыполнимость следующего множества дизъюнктов . Пронумеруем дизъюнкты. Это делается для того, чтобы при построении резольвенты можно было сослаться на …
Pic.82
Порождаем логические следствия, при порождении следствия будем указывать, номера участвовавших в построении дизъюнктов: Порождаем логические следствия, при порождении следствия будем указывать, …
Pic.83
Замечание. Алгоритм проверки невыполнимости недетерминирован. Вообще говоря, возможен не один вариант выбора значений для l, S1 и S2. В приведенном примере дизъюнкты выбирались в лексико-графическом …
Pic.84
Свойство 1. Если множество S не содержит ни одной пары дизъюнктов, допускающих резольвенту, то оно выполнимо (за исключением случая, когда оно содержит пустой дизъюнкт). Свойство 2. Если выполнение …
Pic.85
Пример. Доказать, используя метод резолюций, что S является логическим следствием множества гипотез H, где Пример. Доказать, используя метод резолюций, что S является логическим следствием множества …
Pic.86
Для доказательства того, что H |= S необходимо и достаточно доказать невыполнимость следующего множества дизъюнктов Для доказательства того, что H |= S необходимо и достаточно доказать невыполнимость …
Pic.87
Пример. Пусть дано множество утверждений, сформулированных на естественном языке, и некоторое заключение, которое из них следует. Требуется превратить их в множество высказываний и доказать …
Pic.88
Введем следующие обозначения для высказываний: Введем следующие обозначения для высказываний: g – встать рано; d – играть в преферанс; с – идти на первую пару; s – лечь поздно спать; e – мало спать. …
Pic.89
Следствие примет вид . При построении доказательства по дедукции в качестве механизма воспользуемся методом эквивалентных преобразований и методом резолюций. Требуется доказать невыполнимость …
Pic.90
Теперь построим доказательство, используя метод резолюций. Для этого приведем имеющиеся гипотезы к форме дизъюнктов: Теперь построим доказательство, используя метод резолюций. Для этого приведем …
Pic.91
Если вам понравился сайт и размещенные на нем материалы, пожалуйста, не забывайте поделиться этой страничкой в социальных сетях и с друзьями! Спасибо!
