Тема: Методы доказательства в исчислении высказываний

Лекция №4

Тема: Методы доказательства в исчислении высказываний

План:

1.  Метод натурального исчисления.

2.  Алгоритм Хао Вонга.

3.  Метод резолюций.

1.  Метод натурального исчисления

Исчисление, не содержащее аксиом, называют натуральным (ИВН). Правила вывода ИВН являются формализацией стандартных правильных умозаключений. Их можно разделить на две группы: правила включения и правила исключения. Все правила задаются выражениями вида , где S1,…,Sk, S– произвольные секвенции (выражения со знаком «⊢»), а S называется непосредственным следствием из S1,…,Sk по данному правилу вывода. В записи правил буквы A, B и C обозначают любые формулы, при этом С используется для обозначения последней посылки, а буквы Г1, Г2, Г3 и Г – обозначают конечные последовательности формул, возможно, пустые.

(включение конъюнкции);

(включение дизъюнкции);

(включение импликации);

(включение отрицания);

(исключение конъюнкции);

(исключение импликации);

(исключение отрицания);

Выводом в ИВН называется непустая конечная последовательность формул С1,С2,…,Сn, удовлетворяющая следующим двум условиям:

1)  каждая из формул Сi (i=1,2,…,n), либо является посылкой (гипотезой, допущением), либо получена из предыдущих формул по одному из правил вывода; и

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

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

Если имеется последовательность формул С1,С2,…,Сn, являющаяся выводом, в котором формулы А1,А2,…,Аk – являются неисключенными посылками, а формула Сn совпадает с формулой В, то эту последовательность называют выводом формулы В из посылок А1,А2,…,Аk. Этот факт обозначают: A1,…, Ak ⊢ B («из посылок A1,…, Ak выводимо В», запятая между посылками означает их конъюнкцию). Если формулы А1,А2,…,Аk содержатся в множестве формул Г, то последовательность С1,С2,…,Сn, является также выводом В из Г: Г ⊢ В.

Доказательством называется вывод из пустого множества неисключенных посылок. Последняя формула в доказательстве называется доказанной формулой или теоремой. («⊢ B» – B доказуема или B – теорема).

Выбор посылок.

Построение выводов и доказательств – задача творческая. Она состоит в нахождении нужной последовательности формул, в которую при необходимости включают также формулы посылок. Однако в дальнейших шагах вывода все принятые допущения должны быть исключены. Вообще говоря, в качестве посылок можно брать любые формулы, но не любой такой выбор одинаково быстро приводит к результату. Поэтому, чтобы этот процесс не был случайным перебором всех возможностей, определим приёмы, позволяющие в большинстве случаев уменьшить число переборов. Эти приёмы будем называть эвристиками для выбора посылок.

Пусть требуется построить вывод для обоснования секвенции вида:

Первая эвристика: в выводимой формуле следует выделить антецедент и консеквент, добавить антецедент к посылкам, а консеквент оставить справа от знака ⊢, т. о. будет получена новая секвенция: , вывод которой следует построить. Если это возможно, то к полученной секвенции снова применяют тот же приём и действуют так до тех пор, пока справа от знака ⊢, не останется формула без импликаций. Если это формула B, то секвенция принимает вид: . Формула B здесь является целью вывода, и если удастся достигнуть этой цели, то затем, применяя последовательно правило Éв, можно исключить дополнительные посылки и тем самым обосновать вывод (1). Этот приём основан на теореме о дедукции: , где Г – набор некоторых формул, C и B – произвольные формулы.

Вторая эвристика: эта эвристика применяется после первой, если после её применения не удается построить вывод для (2), где B – не импликативная формула. Тогда в качестве дополнительной посылки берут ù B , и общий список посылок теперь ù B. А целью вывода становится получение в его составе противоречия, т. е. получения в выводе двух формул вида D и ù D. Если это удалось, то далее можно применить правило ùв и получить формулу ù ù B, а затем, применяя правило ùи, получить формулу B и тем самым обосновать вывод (2). Далее, применив нужное число раз правило Éв, получить вывод (1). Этот прием основан на эквивалентности секвенций и .

Третья эвристика: (применяется после второй). Если в выводе имеется дизъюнктивная формула AÚB, то в качестве дополнительных посылок можно выбрать части этой формулы в следующих комбинациях: или A, или B, или ù A, или ù B, или A и B, или ù A и ù B. При этом, поскольку выбор неоднозначен, то требуется творческая переработка каждого из вариантов. И т. к. 3-я эвристика применятся после второй, то целью вывода остается получение в его составе противоречия.

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

A É B ºù A Ú B; A É B ºù ( A &ù B );

A & B ºù (ù A Ú ù B ); A & B ºù ( A Éù B );

A Ú B ºù (ù A &ù B ); A Ú B ºù A É B; A Ú B º(( A É B ) É B );

(A º B) = (( A É B ) & ( B É A ))

Примеры выводов и доказательств, построенных методом ИВН

1) Построить вывод формулы C из посылок (A É B), (B É C) и A или доказать секвенцию: (A É B), (B É C), A ⊢ C

1.	A É B	пос.
2.	B É C	пос.
3.	A	пос.
4.	B	Éи, 1, 3
5.	C	Éи, 2, 4

Запись вывода оформляется в виде последовательности пронумерованных формул (по одной в строке). Для каждой формулы помечается, является ли она посылкой или получена из предыдущих формул по какому-нибудь правилу вывода. Исключенные из вывода формулы помечаются слева вертикальной чертой.

2) Доказать секвенцию: E É D, E º C, C º A, D º B ⊢ A É B

1.	E É D	пос.
2.	(E É C) & (C É E)	пос.(эквив. преобраз.)
3.	(C É A) & (A É C)	пос.(эквив. преобраз.)
4.	(D É B) & (B É D)	пос.(эквив. преобраз.)
5.	A	пос.(1-я эврист.)
6.	A É C	&и, 3
7.	C	Éи, 5, 6
8.	C É E	&и, 2
9.	E	Éи, 7, 8
10.	D	Éи, 1, 9
11.	D É B	&и, 4
12.	B	Éи, 10, 11
13.	A É B	Éв, пос.5, 12

2. Алгоритм Хао Вонга

Этот алгоритм предоставляет почти механическую процедуру для обоснования или опровержения секвенций . Его основанием является истинная секвенция A, B ⊢ A, которая выражает отношение порядка в ИВ и равносильна правилу &и. Перед применением этого метода посылки A1,…,An и заключение B в исходном выражении следует представить в виде формул без знака «É». Это легко сделать, используя законы взаимовыразимости логических связок. Затем выполняют действия по следующей схеме.

1. Если какая-нибудь формула имеет вид ùD, то перенести эту формулу на другую сторону относительно знака «⊢», опустив отрицание, например, строка: AÚB, ù(CÚD), ùE ⊢ S, ùP, переходит в строку: AÚB, P ⊢ S, (CÚD), E

2. Если слева от знака «⊢» в какой-нибудь формуле главной связкой является «&», а справа – «Ú», то заменить эти связки запятыми. Например: A&B, C&(ùAÚD) ⊢ ùBÚùC, переходит в A, B, C,(ùAÚD) ⊢ ùB,ùC

3. Если главной связкой в формуле слева от «⊢» является «Ú», а справа – «&», то образовать два новых выражения, каждое из которых содержит одну из двух подформул, заменяющих исходную формулу. Например, из A, ùAÚB ⊢ B, получаются строки: 1) A, ùA ⊢ B и 2) A, B ⊢ B. Чтобы обосновать выводимость исходной формулы, требуется доказать все полученные таким образом строки.

4. Если одна и та же формула находится с обеих сторон от знака «⊢», то строка доказана.

5. Если в строке не остается ни одной связки и если ни одна переменная не присутствует с обеих сторон от знака «⊢», то строка недоказуема. Если же все переменные в левой части от «⊢» истинны, а в правой части ложны, то исходное утверждение опровергается.

Примеры выводов и доказательств, построенных методом Вонга

1) Доказать секвенцию: (A É B), (B É C), A ⊢ C

ùAÚB, ùBÚC, A ⊢ C
ùA, ùBÚC, A ⊢ C	B, ùBÚC, A ⊢ C
ùBÚC, A ⊢ C, A	B, ùB, A ⊢ C	B, C, A ⊢ C
	B, A ⊢ C, B

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

2) Доказать теорему: ⊢ ( A Ú B ) É ( B Ú A )

⊢ ù( A Ú B ) Ú ( B Ú A )
A Ú B ⊢B, A
A ⊢B, A	B ⊢B, A

3) Доказать: A º B ⊢ (( C É A) º ( C É B))

I. ùAÚB, ùBÚA ⊢ (ù (ùCÚA)ÚùCÚB)&(ù (ùCÚB)ÚùCÚA)

1) ùAÚB, ùBÚA ⊢ (ù (ùCÚA)ÚùCÚB)

ùAÚB, ùBÚA, ùCÚA ⊢ ùC, B

a) ùAÚB, ùBÚA, ùC ⊢ ùC, B– строка доказана.

b) ùAÚB, ùBÚA, A, C⊢ B

i) B, ùBÚA, A, C⊢ B– строка доказана.

ii) ùA, ùBÚA, A, C⊢ B

ùBÚA, A, C⊢ B, A– строка доказана.

2) ùAÚB, ùBÚA ⊢ (ù (ùCÚB)ÚùCÚA)

ùAÚB, ùBÚA, ùCÚB ⊢ ùC, A

a) ùAÚB, ùBÚA, ùC ⊢ ùC, A– строка доказана.

b) ùAÚB, ùBÚA, B, C ⊢ A

i) ùAÚB, A, B, C ⊢ A– строка доказана.

ii) ùAÚB, ùB, B, C ⊢ A

ùAÚB, B, C ⊢ A, B– строка доказана.

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

Метод резолюции основан на выводимой секвенции A Ú C, B Ú ù C ⊢ A Ú B, называемой законом склеивания. Здесь два посылочных дизъюнкта «склеиваются» по формуле C и ù C, образуя дизъюнкт–резольвенту без формулы C. Процедура доказательства секвенций начинается с замены всех посылок и отрицания заключения на эквивалентные им формулы в конъюнктивной нормальной форме (КНФ). Затем все элементарные дизъюнкции полученных КНФ помещаются в единую группу и из этой группы отбираются две формулы так, что если в одну из них входит некоторая переменная C, то в другой имеется ù C. Эти формулы «склеиваются», и полученный таким образом новый дизъюнкт помещается в общую группу. Процесс продолжается до тех пор, пока: 1) либо встречается противоречие, и тогда утверждение доказано; 2) либо невозможно построить ни одной новой формулы, и тогда утверждение опровергается.

Примеры выводов и доказательств, построенных методом резолюций

1) Доказать секвенцию: (A É B), (B É C), A ⊢ C

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

2) Доказать секвенцию: E É D, E º C, C º A, D º B ⊢ A É B.

Пусть Z = A É B. Тогда КНФ(ùZ)=A&ùB

3) Доказать секвенцию: E É D, C Ú E, A Ú D, D Éù B ⊢ C & D, (E & B) É (E É A)

Пусть Z= (C & D) Ú ((E & B) É (E É A)).

1.	ùE Ú D	7.	B
2.	C Ú E	8.	ùA
3.	A Ú D	9.	res(4, 7) =ùD
4.	ùD Ú ùB	10.	res(3, 9) =A
5.	ùC Ú ùD	11.	res(8, 10) =^
6.	E

Тогда КНФ(ùZ) =ù (C & D)&ù ((E & B) É 

(E É A)) = (ùC Ú ùD)& E & B&ù(E É A) = (ùC Ú ùD)&E & B &ùA. Построим вывод в виде списка. Будем обозначать формулу, получаемую при «склеивании», – «res» (резольвента).

4) Доказать или опровергнуть: ⊢ (ùB ÉùA) É ((ùB ÉA) É ùA).

Пусть Z =(ùB ÉùA) É ((ùB ÉA) É ùA). Тогда КНФ(ùZ) =ù((ùB ÉùA) É ((ùB ÉA) É ùA))

=(B Ú ùA)&ù ((ùB ÉA) É ùA) =(B Ú ùA)& (B Ú A)& A.

1.	B Ú ùA	3.	A
2.	B Ú A	4.	res(1, 3) =B

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