- •Построение доказательств в логике высказываний
- •Аксиоматический метод
- •Принцип резолюций
- •Метод Вонга
- •Метод натурального исчисления
- •Задания на практическую работу по логике высказываний
- •Решения
- •Примеры решения задач
- •С помощью средств предыдущего примера доказать клаузу:
- •Составить легенды для приведенных ниже четырех клауз.
- •Операции над предикатами и кванторами
- •Построение доказательств в логике предикатов
- •Задания на практическую работу по логике предикатов
- •Разбор решений задач по логике предикатов
Метод Вонга
Близким к методу резолюций является метод Вонга, в котором тоже используется сконструированная конъюнктивно-дизъюнктивная нормальная форма представления исходной клаузы, а аксиому порядка заменяет клауза Вонга.
X,L=>X;R,
здесь Xпробегает некоторые буквы, входящие в клаузу,aLиR— определенные комбинации дизъюнктов и конъюнктов.
Конструктивная процедура доказательства сводится к последовательному разбиению дизъюнктов или конъюнктов таким образом, чтобы слева и справа от метаимпликации появилась одна и та же буква X. Если в результате такого разбиения все конечные клаузы приобретают вид клаузы Вонга, то и исходная клауза была составлена верно. Разберем метод Вонга на примере доказательства справедливостиправила отделения:
А, А -> В => В или A, -AvВ => В .
Здесь имеется только один дизъюнкт, который можно подвергнуть разбиению. После его разбиения получим две новых клаузы:
А, -А=>В и А, В =>В .
Вторая клауза удовлетворяет и аксиоме порядка и клаузе Вонга. В качестве Xв ней выступаетB,aL=AиR=0. Первая же клауза тоже будет удовлетворять необходимым требованиям, но только после того, как терм -А из левой части клаузы с противоположным знаком перенести в правую часть. Тогда будем иметь:
А => А; В
где X=A,L= 1 иR= В .
При большом числе букв в исходной клаузе прибегают к специальной нумерации производных клауз чтобы не запутаться. Пусть требуется установить справедливость следующей клаузы:
X v Y, (X -> Y) v U, Z -> (Y -> W) => (W -> X) -> (Z -> X).
Приведем ее в соответствующую конъюнктивно-дизъюнктивную нормальную форму:
X v Y, -X v Y v U, -Z v -Y v W => W & -X; -Z; X .
Далее произведем разбиение первого дизъюнкта, в результате получим две производные клаузы:
X, -X v Y v U, -Z v –Y v W => W & -X; -Z; X
Y, -X v Y v U, -Z v –Y v W => W & -X; -Z; X
Клауза (1) отбрасывается, так как она удовлетворяет клаузе Вонга. Разбивая следующий дизъюнкт клаузы (2), получаем еще три новых клаузы:
2.1. Y, -X, -Z v -Y v W => W & -X; -Z; X
2.2. Y, Y, -Z v -Y v W => W & -X; -Z; X
2.3. Y, U, -Z v -Y v W => W & -X; -Z; X
Клаузы (2. 1) и (2. 2) сводятся к одной клаузе —
Y, -Z v -Y v W => W & -X; -Z; X
Произведем ее разбиение:
2.1.1. Y, -Z=>W & -X; -Z; X
2.1.2. Y, Y => W & -X; -Z; X
2.1.3. Y, W => W & -X; -Z; X
Первые две клаузы удовлетворяют клаузе Вонга. У клаузы (2.1.3) нужно разбивать конъюнкт:
2.1.3.1. Y, W => W; -Z; X
2.1.3.2. Y, W => -X; -Z; X
Теперь обе клаузы имеют вид клаузы Вонга.
Но у нас осталась еще ветвь (2.3). Она отличается от рассмотренной ветви (наличием непарного терма U, который, однако, не может повлиять на конечный результат, т.е. разбиение клаузы (2.3) практически полностью совпадает с разбиением клаузы (2.1). Следовательно, исходная клауза была записана верно.
Метод натурального исчисления
Недостатком метода Вонга, как и метода резолюций, является то, что исходная клауза обязательно должна иметь нормальную дизъюнктивную или конъктивную форму. Этот недостаток преодолен в методе натурального исчисления, к которому мы переходим.
Доказательный вывод в натуральном исчислении строится как упорядоченная цепь преобразований, связанных с удалением или введением логических связок на основе следующих десяти правил:
№ пп |
Формула правила |
Название правила |
|
(=> А) & (=> В) // => А & В |
введение конъюнкции (ВК) |
|
=> А & В // => А |
удаление конъюнкции (УК) |
|
В // => А -> В А => В // => А -> В |
введение импликации (ВИ) |
|
(=>А) & (=> А -> В) // => В, => А -> В // А=> В |
удаление импликации (УИ) |
|
=> А // =>AvВ |
введение дизъюнкции (ВД) |
|
(=> AvВ) & (А => С) & (В => С) //=> С |
удаление дизъюнкции (УД) |
|
А, В => 0 // А =>-В |
введение отрицания (ВО) |
|
(А => -В) & (А => В) // А => 0 |
удаление отрицания (УО) |
|
(А => В) & (В => А) // => А ~В |
введение эквивалентности (ВЭ) |
|
=> А~В // (А => В) & (В => А) |
удаление эквивалентности (УЭ) |
Замечание. Эти правила надо понимать так: если слева от символа « // » стоят истинные клаузы, то справа от символа « // » тоже будут стоять истинные клаузы. Например, первое правиловведения конъюнкцииможно прочитать следующим образом: если высказывания А и В (связка «и» передается знаком « & ») порознь истинные (о чем говорят рядом стоящие с этими буквами символы метаимшшкации «=>»), то будет истинной и их конъюнкция А & В. При этом надо помнить, что во всех десяти правилах перед символом метаимпликации « => » может стоять любой перечень посылок Р. Так, десятое правило может выглядеть следующим образом:
Р => А ~В // (Р, А => В) & (Р, В => А).
Кроме перечисленных десяти правил, имеется еще одно — базовое правило (БП), которое сначала сформулируем словами:
во-первых, любая посылка может выступать в роли следствия,
т.е.
А, В, С => А , А, В, С => В и А, В, С => С
будут всегда истинными и не требуют доказательства, т.к. удовлетворяют аксиоме порядка,
во-вторых, в перечень посылок истинной клаузы всегда можно добавить новые посылки, т.е. если клауза
А, В, С => X
верна, то будут истинными и все клаузы, построенные на ее основе —
А, В, С, D=>X, А, В, С, ... =>X.
В обобщенной форме базовое правило можно записать так:
Р => X// Р,Y=>X,
где X— любая посылка из Р,aY— произвольная посылка.
Действенность метода натурального исчисления продемонстрируем на примере следующей тавтологии:
1 => (А -> В) -> ((А -> -В) -> -А).
Доказательство:
№ пп |
Выводы |
Почему |
|
А, А -> В => В |
УИ |
|
А, А -> -В =>-В |
УИ |
|
А, А -> В, А -> -В => В |
1, БП |
|
А, А -> -В, А -> В =>-В |
2, БП |
|
А, А -> В, А ->-В => 0 |
3, 4, УО |
|
А -> В, А -> -В =>-А |
5, ВО |
|
А -> В => (А -> -В) ->-А |
6, ВИ |
|
1 => (А -> В) ->((А ->-В) ->-А) |
7, ВИ |
Справа в круглых скобках указан номер строки, из которой получена данная клауза, а также начальные буквы используемого правила. Приведем доказательство еще одной клаузы:
1 => (А -> В) -> ((С -> D) -> ((А v С) -> (В v D))) .
Доказательство:
№ пп |
Выводы |
Почему |
|
А -> В => (С -> D) -> ((AvС) -> (ВvD)) |
УИ |
|
A -> B, C -> D => (A v C) -> (B v D) |
1, УИ |
|
А -> В, С -> D,AvС => ВvD |
2, УИ |
|
Р1,Р2,Р3 => ВvD |
3 |
|
Р => А -> В |
P1, БП |
|
Р, А => В |
5, УИ |
|
P, A => B v D |
6, ВД |
|
Р => С -> D |
Р2, БП |
|
Р, С => D |
8, УИ |
|
Р, С => DvВ |
9, ВД |
|
P => A v C |
Р3, БП |
|
P => B v D |
7, 10, 11, УД |