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

Сентябрь 16, 2022

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

Содержание

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

Слайд 2

Определение
Формальная система представляет собой совокупность чисто абстрактных объектов, не связанных с

внешним миром, в которой представлены правила оперирования множеством символов только в синтаксической трактовке без учета смыслового содержания.

Слайд 3

Всякая формальная система строится на основе формализованного языка (как средства формирования

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

Слайд 4

В формальной теории все формулы доказываются.
Под теоремой в формальной системе понимают

высказывание, истинное в данной системе, − это некоторое обоснованное и строгое утверждение, которое строится на основе определенных логических правил и доказательства.

Слайд 5

Доказательство – это способ получения одних выражений из других с помощью

операций над символами и построения обоснованной аргументации, следствием которой и является теорема.
При построении любой формальной теории (системы) в качестве исходных посылок всегда используются некоторые неопределяемые термины и аксиомы.

Слайд 6

Неопределяемые термины – это те термины и понятия, смысл и содержание

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

Слайд 7

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

как очевидные истины.
Такие выражения называют аксиомами, а системы, в основе построения которых лежит использование аксиом, называются аксиоматическими системами.

Слайд 8

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

которые образуют алфавит формальной системы.
2. Устанавливаются процедуры построения формул формальной системы.

Слайд 9

3. Устанавливается множество аксиом, т.е. формул, истинность которых не требует доказательства.

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

Слайд 10

В общем случае эти правила могут быть представлены в следующем виде

что означает: из множества истинных формул указанных в левой части выражения, следует истинность формул правой части выражения.
Говорят, что формула М, полученная в результате применения правила вывода, выводима в данной теории.

Слайд 11

Определение
Формальным доказательством, или просто доказательством, называется последовательность формул
такая, что каждая формула

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

Слайд 12

Задаваемые при описании формальной системы правила вывода называют также правилами вывода

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

Слайд 13

Различают два типа правил вывода.
1. Правила, применяемые к формулам, рассматриваемым как

единое целое, в этом случае их называют продукционными правилами.
Пример. x < y и y < z, следовательно x < z − это продукция с двумя посылками.

Слайд 14

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. Математик изучает реальность, конструируя некоторое абстрактное представление о ней, т.е.

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

Слайд 24

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.
То есть переменная a должна принимать взаимно исключающие значения, что невозможно. Следовательно, предположение о существовании интерпретации, при которой формула
принимает значение «ложь» неверно и это означает ее общезначимость.

Слайд 69

Метод резолюций. Для порождения логических следствий будет использована очень простая схема

рассуждений. Пусть A, B и X – формулы. Предположим, что две формулы истинны. Тогда, если X истина, то отсюда следует, что B тоже истина. Наоборот, если X – ложь, то следует, что A – истина. Получаем правило
,
которое можно записать в виде
.

Слайд 70

В том частном случае, когда 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 необходимо строить логические следствия из него до тех пор, пока не будет получен пустой дизъюнкт или дальнейшее построение логических следствий окажется невозможным.

Слайд 75

Метод резолюций выгодно отличается от других методов тем, что он дает

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

Слайд 76

Определение. Литера − это элементарное высказывание или его отрицание. Например,
.
Определение.

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

Слайд 77

Так как для того, чтобы выражение в форме КНФ было тождественно

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

Слайд 78

Итак, невыполнимость формул, из которых формируется конечное множество дизъюнктов S, доказывается

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

Слайд 79

Шаг 2. Построение резольвенты. Выбираем l, S1, S2, такие, что и

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

Слайд 80

Шаг 3. Обновление множества дизъюнктов. Заменяем множество дизъюнктов
, т.е. добавляем

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

Слайд 81

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

дизъюнкты. Это делается для того, чтобы при построении резольвенты можно было сослаться на дизъюнкты, которые для этого использовались.

Слайд 82

Порождаем логические следствия, при порождении следствия будем указывать, номера участвовавших в

построении дизъюнктов:

Слайд 83

Замечание. Алгоритм проверки невыполнимости недетерминирован. Вообще говоря, возможен не один вариант

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

Слайд 84

Свойство 1. Если множество S не содержит ни одной пары дизъюнктов,

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

Слайд 85

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

гипотез H, где
, а
. Сначала преобразуем множество гипотез в множество дизъюнктов:

Слайд 86

Для доказательства того, что H |= S необходимо и достаточно доказать

невыполнимость следующего множества дизъюнктов

Слайд 87

Пример. Пусть дано множество утверждений, сформулированных на естественном языке, и некоторое

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

Слайд 88

Введем следующие обозначения для высказываний:
g – встать рано;
d – играть в

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

Слайд 89

Следствие примет вид . При построении доказательства по дедукции в качестве

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

Слайд 90

Теперь построим доказательство, используя метод резолюций. Для этого приведем имеющиеся гипотезы

к форме дизъюнктов:
Отрицание следствия будет иметь вид ,
а цепочка доказательства: