Презентация - Исчисление высказываний

Смотреть слайды в полном размере
Презентация Исчисление высказываний


Вашему вниманию предлагается презентация на тему «Исчисление высказываний», с которой можно предварительно ознакомиться, просмотреть текст и слайды к ней, а так же, в случае, если она вам подходит - скачать файл для редактирования или печати.

Презентация содержит 35 слайдов и доступна для скачивания в формате ppt. Размер скачиваемого файла: 1.17 MB

Просмотреть и скачать

Pic.1
Исчисление высказываний
Исчисление высказываний
Pic.2
Исчисление высказываний – формальная теория Т, в которой заданы: 1. Алфавит А: переменные - x, y, z,
Исчисление высказываний – формальная теория Т, в которой заданы: 1. Алфавит А: переменные - x, y, z, xi ; логические связки - , (дополнительно можно ввести связки , т. к. ( ) – технические символы (, не является символом алфавита).
Pic.3
2. Язык состоит из слов. Словом (формулой исчисления) называют любую конечную последовательность алф
2. Язык состоит из слов. Словом (формулой исчисления) называют любую конечную последовательность алфавита. 3. Правильно построенные формулы (ППФ). других ППФ нет.
Pic.4
4. Аксиомы.
4. Аксиомы.
Pic.5
5. Правило вывода. МР принимается без доказательства!
5. Правило вывода. МР принимается без доказательства!
Pic.6
6. Вывод формулы - конечная последовательность формул А1, А2, …, Аn, такая, что: последняя формула с
6. Вывод формулы - конечная последовательность формул А1, А2, …, Аn, такая, что: последняя формула совпадает с выводимой; каждая формула вывода является либо аксиомой, либо получена из предыдущих по МР.
Pic.7
Исчисление высказываний представляет собой множество выводимых формул в данном алфавите при данном н
Исчисление высказываний представляет собой множество выводимых формул в данном алфавите при данном наборе аксиом и правил вывода.
Pic.8
Первые теоремы ИВ Д-во первых теорем выглядит громоздко и непредсказуемо. В дальнейшем выводятся нек
Первые теоремы ИВ Д-во первых теорем выглядит громоздко и непредсказуемо. В дальнейшем выводятся некоторые правила, которые будут предсказывать д-во теорем. Ⱶ А – формула А выводима. Перед всеми аксиомами можно поставить знак Ⱶ, т. к. они постулировались.
Pic.9
Исчисление высказываний, слайд 9
Pic.10
Исчисление высказываний, слайд 10
Pic.11
Исчисление высказываний, слайд 11
Pic.12
Исчисление высказываний, слайд 12
Pic.13
Исчисление высказываний, слайд 13
Pic.14
Исчисление высказываний, слайд 14
Pic.15
Выводимость из гипотез Пусть даны формулы – гипотезы А1, А2, …, Аn Нужно доказать А1, А2, …, Аn Ⱶ F
Выводимость из гипотез Пусть даны формулы – гипотезы А1, А2, …, Аn Нужно доказать А1, А2, …, Аn Ⱶ F Совокупность этих гипотез обозначим Г Выводом (доказательством) формулы F из гипотез Г называется последовательность формул F1, F2, …, Fn, в которых последняя формула совпадает с F и каждая Fi – аксиома или получена из предыдущих по МР.
Pic.16
Свойства выводимости из гипотез Если Г, А⊢А (самовыводимость). Если Г⊢А, то Г, В⊢А (расширение списк
Свойства выводимости из гипотез Если Г, А⊢А (самовыводимость). Если Г⊢А, то Г, В⊢А (расширение списка гипотез). Если Г, А⊢В, Г⊢А, то Г⊢В (удаление). Если Г⊢А, А⊢В, то Г⊢В (транзитивность). Если Г, А,В⊢С, то Г, В,А⊢С (коммутативность). Если Г, А, А⊢В, то Г, А⊢В (сокращение).
Pic.17
Теорема дедукции (ТД) выявляет некоторую общую закономерность при таких построениях и тем самым обле
Теорема дедукции (ТД) выявляет некоторую общую закономерность при таких построениях и тем самым облегчает процесс построения доказательства. Если Г, В ├ А, то Г ├ В → А, где Г - это набор некоторых формул Г={F1, F2, . . . , Fn}.
Pic.18
Связь ⊢ и  Наличие МР и ТД позволяет взаимно заменять знаки. Г, А⊢В  Г⊢АВ МР: А, А  В А, А  В ⊢
Связь ⊢ и  Наличие МР и ТД позволяет взаимно заменять знаки. Г, А⊢В  Г⊢АВ МР: А, А  В А, А  В ⊢ В В
Pic.19
Если ТД применять в качестве аксиомы, то А1, А2 можно доказать как теоремы. Докажем А1: ⊢А (В А) А
Если ТД применять в качестве аксиомы, то А1, А2 можно доказать как теоремы. Докажем А1: ⊢А (В А) Анализ: ТД А ⊢ В А ТД А , В ⊢А
Pic.20
Д-во: А , В ⊢А 10 А ⊢ В А 1), ТД А1: ⊢А (В А) 2), ТД
Д-во: А , В ⊢А 10 А ⊢ В А 1), ТД А1: ⊢А (В А) 2), ТД
Pic.21
Докажем А2: ⊢(А (В С))  (А В) (АС) Докажем А2: ⊢(А (В С))  (А В) (АС) Анализ: ТД (А (В
Докажем А2: ⊢(А (В С))  (А В) (АС) Докажем А2: ⊢(А (В С))  (А В) (АС) Анализ: ТД (А (В С)) ⊢ (А В) (АС) ТД А (В С), А В ⊢ АС ТД А (В С), А В, А⊢С
Pic.22
Д-во: А (В С), А В, А⊢В МР А (В С), А В, А⊢В С МР А (В С), (А В), А⊢С 1),2), МР А (В С),
Д-во: А (В С), А В, А⊢В МР А (В С), А В, А⊢В С МР А (В С), (А В), А⊢С 1),2), МР А (В С), А В ⊢ АС 3), ТД (А (В С)) ⊢ (А В) (АС) 4), ТД ⊢(А (В С))  (А В) (АС) 5), ТД
Pic.23
Докажем А В, В С ⊢ АС Анализ: ТД А В, В С, А⊢С Д-во: А В, В С, А⊢В МР А В, В С, А, В⊢С 1),
Докажем А В, В С ⊢ АС Анализ: ТД А В, В С, А⊢С Д-во: А В, В С, А⊢В МР А В, В С, А, В⊢С 1), МР А В, В С, А⊢С 1), 2), 30 А В, В С ⊢ АС 4), ТД
Pic.24
Докажем А В⊢ ВА Д-во: А А, А В⊢ А  В Т3 А В, В В⊢ А  В Т3 А В⊢ А  В 1, 2, 40
Докажем А В⊢ ВА Д-во: А А, А В⊢ А  В Т3 А В, В В⊢ А  В Т3 А В⊢ А  В 1, 2, 40
Pic.25
4) А В⊢ В  А А3 5) А В⊢ В  А 3, 4, 40
4) А В⊢ В  А А3 5) А В⊢ В  А 3, 4, 40
Pic.26
Исчисление высказываний, слайд 26
Pic.27
Производные правила вывода Лемма – доказанное утверждение, полезное для доказательства других утверж
Производные правила вывода Лемма – доказанное утверждение, полезное для доказательства других утверждений.
Pic.28
Lemma 1 (удаление &) Из & двух высказываний выводится каждый член АВ ⊢А Анализ: А В ⊢ А Д-в
Lemma 1 (удаление &) Из & двух высказываний выводится каждый член АВ ⊢А Анализ: А В ⊢ А Д-во: закон контрапозиции 1) А, В А 10 А ⊢ АВ 2) А , АВ 1),конт. ТД 3) А ⊢ АВ 2),ТД А , АВ 4) А В ⊢ А 3), конт. закон контрапозиции 5) АВ ⊢А А, В А
Pic.29
Lemma 2 (удаление &) АВ ⊢В Анализ: А В ⊢ В Д-во: закон контрапозиции 1) В, А ⊢ В 10 В ⊢ АВ 2)
Lemma 2 (удаление &) АВ ⊢В Анализ: А В ⊢ В Д-во: закон контрапозиции 1) В, А ⊢ В 10 В ⊢ АВ 2) В ⊢ АВ 1), ТД ТД 3) А В ⊢ В 2), конт. В , АВ 4) АВ ⊢В
Pic.30
Lemma 3 (введение &) А,В ⊢АВ Анализ: А, В⊢ А В Д-во: закон контрапозиции 1) А, АВ⊢В (МР) А, А
Lemma 3 (введение &) А,В ⊢АВ Анализ: А, В⊢ А В Д-во: закон контрапозиции 1) А, АВ⊢В (МР) А, АВ⊢В 2) А, В⊢ А В 1), контр. 3) А,В ⊢АВ
Pic.31
Lemma 4 (введение V) А ⊢АvB Анализ: А ⊢ А В Д-во: ТД 1) А, В А 10 А, А ⊢ В 2) А , АВ 1),конт. кон
Lemma 4 (введение V) А ⊢АvB Анализ: А ⊢ А В Д-во: ТД 1) А, В А 10 А, А ⊢ В 2) А , АВ 1),конт. контр. 3) А ⊢ АВ 2), ТД А, В ⊢ А 4) А ⊢АvB Lemma 5 (введение V) В ⊢АvB (ВvA)
Pic.32
Lemma 6 (удаление v) Если А ⊢С, В ⊢С, то АvB⊢С Д-во: А ⊢С – дано С⊢А 1), контр. В ⊢С – дано С⊢В 3),
Lemma 6 (удаление v) Если А ⊢С, В ⊢С, то АvB⊢С Д-во: А ⊢С – дано С⊢А 1), контр. В ⊢С – дано С⊢В 3), контр. А,В ⊢А∙В (А В) введ. & С⊢ А В 2),4),5),40 А В ⊢С 6), контр. АvB⊢С
Pic.33
Исчисление высказываний, слайд 33
Pic.34
Доказать: АvBC(AvB) ∙(AvC) Анализ: вв. & АvBCAvB, АvBCAvC уд. V уд. V АAvB, BCAvB АAvC, BCAvC уд
Доказать: АvBC(AvB) ∙(AvC) Анализ: вв. & АvBCAvB, АvBCAvC уд. V уд. V АAvB, BCAvB АAvC, BCAvC уд. & уд. & B,CAvB B,CAvC Д-во: АAvB (вв. v) B,CAvB (вв. v) BCB (уд. &) BCC (уд. &) BCAvB (2), 3),40) АvBCAvB (5), уд. &) АAvC (вв. v) 10) АvBCAvC (7), 9), уд. v) B,CAvС (вв. v) 11) АvB, AvC(AvB) ∙(AvC) (10), вв. &) BCAvC (8), уд. &) 12) АvBC(AvB) ∙(AvC) (6), 10),11),40)
Pic.35
Теорема о полноте Если формула F является тавтологией, то тогда F — выводима.
Теорема о полноте Если формула F является тавтологией, то тогда F — выводима.


Скачать презентацию

Если вам понравился сайт и размещенные на нем материалы, пожалуйста, не забывайте поделиться этой страничкой в социальных сетях и с друзьями! Спасибо!