lec10

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

ϕ

ϕ→τ

τ

ϕ, ϕ→τ ⱶ τ

ϕ и ϕ→τ называются гипотезами, а τ – заключением.

Новые высказывания получаются при помощи этих трех аксиом и Modus Ponens

21

	Пример. 10.4. Применение аксиом и MP			A1: ϕ→(τ→ϕ)
	для вывода формулы логики высказывания			A2: (ϕ→(τ→σ))→((ϕ→τ)→(ϕ→σ))
				A3: (ϕ→ τ)→(τ→ϕ)
		A A
					MP: ϕ, ϕ τ ⱶ τ
	1) В А1 вместо ϕ ставим А; вместо τ = B A получим
	А ((В А) А)				ϕ
	2) В А2 меняем ϕ на А, τ на (В А); σ на А получим					τ

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

ϕ
3) Применяем MP для 1) и 2). Получим
(А (В А)) (А А)	τ
4) Интерпретируем А1 в виде (А (В А)) и по MP (для 3) получаем		A A

Итог: высказывание А А выводимо в нашей аксиоматической системе

22

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

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

Тогда высказывание ϕ↔ϕ1, также выводимо в логике высказываний. Формально это записывается в виде:

ⱶσ↔σ1 ⱶ ϕ↔ϕ1

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

23

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

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

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

σi S

или

σi – аксиома

или

σi получено из σj и σk

по правилу заключения (1≤j,k<i).

24

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

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

S ⱶ σ.

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

!!! 1. Если S = Ø, то понятие выводимого из множества S высказывания совпадает с понятием выводимого высказывания.

2. Если σ выводимо из бесконечного множества S, то σ выводимо из некоторого конечного подмножества S, т.к. доказательство всегда конечно.

25

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

Пусть S – множество высказываний. K, L – высказывания. Тогда

S { K } ⱶ L S ⱶ (K L)

!!! является основной в теории доказательств. Запомнить!

Если высказывания σ и (σ→τ) доказуемы по Бету, то σ и (σ→τ) логически истинны τ также логически истинно и доказуемо по Бету. Каждая тавтология может быть доказана из аксиом последовательным применением MP. A1÷A3 будучи логическими истинными высказываниями, доказуемы по Бету. Используя MP из логически истинных высказываний получаем также логически истинные высказывания.

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

26

Часть 4.

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

Метод резолюции – наиболее эффективный способ алгоритмического доказательства как в логике высказываний так и в логике предикатов.

!!! основа языка программирования ПРОЛОГ.

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

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

Пустой дизъюнкт – это дизъюнкт, который не содержит ни одного литерала.

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

Пример 10.5. (A B C) (B D) ( A D). S={{A, B, C},{B,D},{ A, D}}

28

Свойства операций и :

1)Склеивание дизъюнкций: (X D) ( X D) = (X X) D = 0 D = D.

2)Поглощение: D1 (D1 D2) = (D1 0) (D1 D2) = D1 (0 D2) = D1 0 = D1.

3)Поглощение: (X D1) ( X D2) = (X D1) ( X D2) (D1 D2).

Доказательство:

(X D1) ( X D2) = (X D1) (X D1 D2) ( X D2) ( X D2 D1) =

=(X D1) ( X D2) (X D1 D2) ( X D2 D1) =

=(X D1) ( X D2) (D1 D2)

29

Пусть С1 и С2 – дизъюнкты, такие что

C1 = {L} 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}}.

30