дзержинский и воронцов 2

Такие высказывания будем называть сложными. Каждое сложное высказывание, как и элементарное, принимает значение «истина» или «ложь», („И“, „/\“), („T’’. „F’’), („t”, „f’’).

Определение формулы:

1.Всякое элементарное высказывание является формулой

2.Если А и В формулы, то Ā, (A \/ B),(A /\ B ),(A→B)(A↔B)

тоже формулы

3.Формулы получаются с помощью правил 1. И 2.

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

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

Так как множество высказываний с операциями (/\, \/, -) является булевой алгеброй, то то, что было изложено в курсе «Основы дискретной математики» для булевой алгебры булевых векторов будет справедливо и для булевой алгебры высказываний (это изоморфизм булевых алгебр).

Определение: Пусть S – множество высказываний S= H1, H2, …Hn , высказывание А есть логическое следствие высказываний H1,…,Hn (или называется логическим следствием из S). Если всякий раз, когда все Hi равны «…Истина» («Т») («И»), значение А также равно «Т».

Семантические таблицы

Для проверки того является ли высказывание тавтологией или противоречием метод таблиц истинности удобен при небольшом количестве атомов (переменных) , однако при числе атомов u=10 таблица истинности будет содержать 210=1024 строк, поэтому существует более совершенные и

23

экономичные методы.

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

Пусть «а» высказывание. Обозначим через fa – утверждение „a- ложно“, через ta – утверждение „a-истинно“. fa и ta называются помеченными формулами.

Вершинами семантической таблицы называются все помеченные формулы, встречающиеся в этой таблице.

Элементарные семантические таблицы.

Атомарные семантические таблицы.

Таблица 6

Обозначение:

Для любого высказывания а:

fa (высказывание а ложно) и

24

ta (высказывание а истинно)

называются помеченными вершинами.

Определение:

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

Определение:

Вершина семантической таблицы называется особой, если она встречается как корень в некоторой атомарной семантической таблице.

Иначе – вершина называется обычной.

Определение:

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

Определение:

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

Семантическую таблицу называют противоречивой, если все ее ветви противоречивы.

Индуктивное определение семантической таблицы

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

Шаг 1 Поместить помеченную формулу tk ( fk ) в корень таблицы

Далее по индукции.

Шаг n. Пусть построена семантическая таблица Tn

Шаг n+1. Расширить таблицу Tn до Тn+1 ,при этом использовать некоторую вершину таблицы Tn ,которая в дальнейшем использоваться не будет. Из всех обычных вершин Tn , ближайших к корню ,выбрать самую левую, и обозначить ее за х . К концу каждой непротиворечивой ветви присоединить атомарную таблицу, имеющую корнем х.

25

При этом х становится особой вершиной . В результате получается таблица Tn+1 .

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

Пример: Закон Пирса

(((А→ B)→ A)→ A) ƒ(((А→ B)→ A)→ A)

|

ƒ((А→ B)→ A)

ƒ(B)

|

Вывод: закон Пирса - тавтология. t(((А→ B)→ A)→ A)

|

ƒ((А→ B)→ A) or tA

|

t(А→ B)

|

t( ̶А)

|

ƒА

|

ƒА or tB

Противоречивых ветвей нет. Значит закон Пирса-тавтология.

Определение:

Доказательством или выводом по Бету высказывания k называется противоречивая семантическая таблица ,в корне которой помещена ƒk.

26

Определение:

Замкнутая противоречивая семантическая таблица, имеющая в качестве корня tk. Называется опровержением по Бету высказывания k .

Определение:

Говорят ,что высказывание доказуемо по Бету ,если существует доказательство по Бету.

Обозначение:

|̶ b K K доказуемо по Бету

|̶b (((А→ B)→ A)→ A)

Пример 1:

K=(А ʌ ̶А)ᴠ(B v (C ʌ D))

Определим условие истинности K.

Высказывание k истинно при истинном означивании V. V1 (B)=t, V2(C)=t, V2(D)=t.

V1(А)=tǁƒ

V1(C)=tǁƒ

V1(B)=tǁƒ

27

Аксиоматическая система вывода

Логика высказываний ,подобно другим математическим системам может быть представлена как аксиоматическая система с логическими аксиомами и правилами вывода. Аксиомы – это некоторые тавтологии ,правило вывода R выводит высказывание σ из последовательности высказываний σ1, σ2,… σn

Определение: каждое высказывание следующего вида является аксиомой

1.ϕ→(τ→ϕ)

2.(ϕ→(τ→σ))→((ϕ→τ)→(ϕ→σ))

3.(ɿϕ→ɿτ)→(τ→ϕ)

Высказывания ϕ, τ, σ могут быть произвольными. Все эти аксиомы являются тавтологиями.

Определение: Правило вывода Modus Ponens(Правило заключения) утверждает, что высказывания τ выводится из высказываний ϕ и ϕ→τ

ϕ

A→A

Сначала возьмем первую аксиому и вместо ϕ ставим А; вместо τ = B→A получим А→((В→А)→А)

Вторую аксиому запишем ,заменив в ней ϕ на А , τ на (В→А) ; σ на А (А→((В→А)→А))→((А→(В→А))→(А→А))

из этих двух высказываний по правилу вывода получаем

(А→(В→А))→(А→А)

Используя вновь первую аксиому в виде А→(В→А) по правилу вывода выводим высказывание А→А.

28

Следовательно высказывание А→А выводимо в нашей аксиоматической системе.

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

Теорема (о подстановке эквивалентных формул)

Пусть высказывание σ↔ σ1 выводимо в логике высказываний , σ – подформул высказывания ϕ, и высказывание ϕ1 получено в результате подстановки в высказывание ϕ вместо некоторых вхождений формулы σ эквивалентной ей формулы σ1. Тогда высказывание ϕ↔ϕ1 , также выводимо в логике высказываний. Формально это записывается так : |̶ σ↔ σ1 <=> |̶ϕ↔ ϕ1

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

Пусть S – множество высказываний.

Доказательством или выводом из S называется такая конечная последовательность высказываний σ1,σ2,….., σn , что для каждого I 1 ≤ I ≤ n верно:

а) σi принадлежит S или б) σi – аксиома или

в) σi получено из σj и σk где 1 ≤ j, k≤ j

по правилу заключения

Высказывание σ называется: доказуемым или выводимым из множества высказываний S, если существует такое доказательство σ1, σ2,… σn из S,что σn совпадает с σ. Для обозначения выводимости высказывания σ из множества высказывания S будем использовать запись S |̶ σ .

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

Отметим ,что если S пустое множество ,то понятия выводимого из множества S высказывания совпадает с понятием выводимого высказывания

.Заметим что если σ выводимо из бесконечного множества S ,то σ выводимо из некоторого конечного подмножества ,так как доказательство всегда конечно . Следующая Теорема является основной в теории доказательств

Теорема дедукции .

Пусть S - множество высказываний .

29

K, L – высказывания .Тогда S ᴜ { k } |̶ L <=> S |̶ (K→L)

На эту теорему мы в дальнейшем будем часто ссылаться . Отметим , что :Если высказывания σ и (σ→τ) доказуемы по Бету то σ и (σ→τ) логически истинны ,следовательно , τ также логически истинно и доказуемо по Бету . Каждая тавтология может быть доказана из аксиом последовательным применением правила заключения. Наши аксиомы будучи логическими истинными высказываниями , доказуемомы по Бету. Используя правило вывода мы из логически истинных высказываний получаем также логически истинные высказывания.

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

Метод резолюции

Метод резолюции – наиболее эффективный способ алгоритмического доказательства как в логике высказываний так и в логике предикатов именно этот метод построения доказательств составляет основу языка программирования ПРОЛОГ

Мы знаем что любую формулу не являющуюся тавтологией можно представить в виде КНФ.

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

литерала и является всегда неподтверждённым.

Удобнее формулировать сложное высказывание, представленное в виде КНФ как множество дизъюнктов . А каждый дизъюнкт представлять как множество литералов. ТО есть КНФ это конъюнкция конечного множества дизъюнктов , а дизъюнкт – это дизъюнкция конечного множества литералов.

Пример (Av¬Bv¬C) ^(BvD)^( ¬Av¬D) S={{{A, ┐B, ┐C},{B,D},{┐A, ┐D}}

Напомним свойства операций v и ^: Склеивание дизъюнкций

(XvD)*( ¬XvD)=(X*¬X)vD=0vD=D

Поглощение

D1*(D1vD2)=(D1v0)*( D1vD2)= D1v(0*D2)=D1v0=D1

Обобщённое склеивание

(XvD1)*( ¬XvD2)=(XvD1)*( ¬XvD2)*(D1vD2)

Доказательство этого

30

(XvD1)*( ¬XvD2)=(XvD1)*(XvD1vD2)*( ¬XvD2)*( ¬XvD2vD1)=(XvD1)*( ¬XvD2)*(XvD1vD2)( ¬XvD2vD1)=

=(XvD1)*( ¬XvD2)*(D1vD2)

XvD1

D1vD2

¬XvD2

Пусть С1 и С2 – дизъюнкты, такие что C1 ={L}υA a C2={¬L}υB

Мы можем считать, что дизъюнкты С1 и С2 вступают в противоречие, так как С1 содержит литерал L a C2 – литерал - ¬L.Устранение причины противоречия приводит к дизъюнкту D=AυB, который разрешает конфликт. Своим названием метод резолюции обязан этому разрешению (от англ. Resolve

– разрешать)

Дадим формальное определение резолюции

Опр Пусть С1 и С2 дизъюнкты, L- такой литерал, что L ϵ C1 и ¬L ϵ C2, тогда резольвентой дизъюнктов С1 и С2 называется дизъюнкт

D={C1\{L}}υ{C2\{¬L}

D={AυB}

Опр Пусть мн. S={C1,….Cn} – множество дизъюнктов. Резольвентой мн S наз множество R(S)=Sυ{D:D-резольвента дизъюнктов Ci,Cj 1≤i,j≤n}

Пример S={{A, ¬B, ¬C},{B,D},{¬A, ¬D}}

В итоге R(S)= {B,D},{¬A, ¬D},{A,D, ¬C},{B¬A},{¬B, ¬C, ¬D}

Мы можем продолжить применять этот метод последовательно получим множества

R0 (S)=S,R1(S)=R0(S) υR(S), R2(S)=R1(S) υR(R1S …Rn(S)= Rn-1(S) υR(Rn-

1(S))

А затем объединив все множества

R*(S)=

Заметим, что R*(S) конечно тогда и только тогда, когда S конечно

Содержательная подоплёка метода резолюции такова: если истинное означивание подтверждает дизъюнкты С1 и С2 , то оно также подтверждает их резольвенту D. Аналогично, если истинностное означивание подтверждает мн.

31

S, то оно также подтверждает R(S).

Заметим, что резольвента D дизъюнктов C1 и С2 содержит меньше информации, чем сами дизъюнкты С1 и С2

назовём такую конечную последовательность дизъюнктов С1,....Сn , что для каждого Ci i=1,…n

Либо Ci ϵ S, либо Ci ϵ R({Cj,Cк}) 1≤j, k≤I

Дизъюнкт C считается резолютивно выводимым из мн. дизъюнктов S, если существует резолютивный вывод из S, последний дизъюнкт которого – С=Cn. Очевидно что C ϵ R*(S). Этот факт обозначается так

S R С

Мн дизъюнктов S не подтверждаемо (или невыполнимо) тогда и только тогда,

Когда R*(S)= содержит пустой дизъюнкт

То есть если мы при применении метода резолюции к множеству S получим пустой дизъюнкт, то множество S будет неподтверждаемым .

Так как правило резолюции – это выводимое правило логики высказываний, то можно использовать теорему дедукции, по которой

{SυK} ⱶ ¬ L ↔ S ⱶ (К→L)

{Sυ¬B} ⱶ □ ↔ S ⱶ (¬B →□)

{Sυ¬B } ⱶ □ ↔ S ⱶ ¬¬B v □

S ⱶ B ↔ (Sυ ¬B) ⱶ □

Пример. Доказать, что высказывание ┐B резолютивно выводимо из мн

S={{A, ┐B},{¬A, ¬B, ¬C},{¬A, ¬B,C}}

32