ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ И ИСЧИСЛЕНИЕ ПРЕДИКАТОВ

Вывод в исчислении высказываний

Формальная система, порождающая высказывания, которые являются тавтологиями и только их, называются исчислением высказываний (ИВ).

Все логические законы должны быть тавтологиями (тождественно истинными). Иногда законы называются правилами вывода, которые определяют правильный вывод из посылок:

1) Modus ponens (правило отделения) ;

2) Формальная запись высказывания (умозаключения, рассуждения) в виде формулы

;

3) правило подстановки .

Фиксируем логико-математический язык первого порядка L. Аксиомами исчисления высказываний(ИВ) в языке L называются формулы этого языка, имеющие один из следующих видов:

, (1)

, (2)

.(3)

Здесь A, B, C – произвольные формулы языка L, так что каждая строка приведенного списка задает схему аксиом ИВ.

Формулы в ИВ считаются выводимыми из аксиом. В каждом выводе из тавтологий выводятся тавтологии.

Выражение ⊦ содержит вывод теоремы В из аксиом или гипотез .

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

Выводом назовем любую конечную последовательность формул , такую, что каждая формула этой последовательности есть либо аксиома, либо совпадает с какой-либо предыдущей формулой этой последовательности, либо получается из каких-то предыдущих формул этой последовательности с помощью одного из правил вывода. При этом получается вывод последней формулы, и формула - выводима, или, что то же самое, теорема теории. Будем записывать это в виде Г⊦ A (выводимость или секвенция).

Список Г может быть пуст, тогда имеет место вывод A без гипотез, формула A выводима в ИВ, записывается это в виде ⊦ A.

Пример.

Вывести в теории L теорему (A A).

Решение.

Возьмем в качестве примера первой формулы вывода аксиому (2). Применим к ней правило подстановки в виде:

( A, ( A A ), A ).

Получим

(( A (( A A ) A )) (( A ( A A )) ( A A ))). (а)

Из аксиомы (1) подстановкой ( A, ( A A )) получим:

( A (( A A ) A )). (б)

Применим правило (MP) к (а) и (б):

(( A ( A A )) ( A A )). (в)

Из аксиомы (1) подстановкой ( A, A ) получим:

(( A ( A A ))). (г)

Применяя (МР) к (в) и (г), окончательно получим:

( A A ). (д)

Запишем правила вывода в исчислении высказываний.

Правило сложного заключения

Если формулы и доказуемы, то и формула L доказуема:

├ А₁, ├ А₂, …, ├ А_n, ├ A₁→ (A₂→ (A₃→ (...(A_n→ L) …)))

├ L

Правило силлогизма

Если доказуемы формулы А→ В и В→ С, то доказуема формула А→ С, т. е.

├ А→ В, ├ В→ С

├ А→ С

Правило контр позиции

Если доказуема формула А→ В, то доказуема формула , т. е.

├ А → В

├

Правило снятия двойного отрицания

Если доказуема формула , то доказуема формула .

Если доказуема формула , то доказуема формула :

├ А →

├ ,

├ → В

├ .

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

Если

j₁, j₂, …, j_n, j ├ ψ,

то

j₁, j₂, …, j_n├ (j → ψ ).

Если нужно в некоторой ситуации установить, что , то допустим (введем гипотезу), что A верно, и докажем B, исходя из этой гипотезы.

Применяя к утверждению теоремы снова несколько раз теорему дедукции, можно, очевидно, получить новые следствия:

j₁, j₂, …, j_n_{− 1}├ (j_n → (j → ψ ));

…

├ (j₁ → … → (j_n_{− 1} → (j_n → (j → ψ )))…).

Теорема, обратная к теореме о дедукции

Если

j₁, j₂, …, j_n├ (j → ψ ),

то

j₁, j₂, …, j_n, j ├ ψ.,

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

Теорема о полноте

Для того чтобы проверить выводимость формулы в ИВ (исчислении высказываний) достаточно проверить, будет ли формула являться тавтологией ЛВ (логики высказываний).

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

Упражнения

Построить вывод или обосновать выводимость формулы логики высказываний. Сделать проверку с помощью теоремы о полноте.

1. ;

2. ;

3. .

Индивидуальное задание

1 Доказать утверждение, предъявив формальный вывод из гипотез или аксиом, предварительно проверив выводимость заключения с помощью теоремы о полноте. Можно пользоваться теоремой дедукции и её обращением.

1.1 (A → (C → B)), (D → A), C ├ (D → B);

1.2 (A → B), (A → C) ├ (A → (B & C));

1.3 (A → B) ├ ((A → B)Ú B);

1.4 (B → A) ├ ((A Ú B)→ A);

1.5 (A → B), (B → C) ├ (A → C);

1.6 (A → (B → C))├ (B → (A → C));

1.7 (A → (Ø B)) ├ (B → (Ø A));

1.8 ├ ((A → (Ø B)) → (B → (Ø A)));

1.9 ├ ((A Ú A) → A);

1.10 A, B ├ (B & A).

1.11 А├ (А → (B → A));

1.12 А → B ├ А→ А;

1.13 B├ А→ А;

1.14 ├ А→ А;

1.15 А, B ├ А→ B.

Метод резолютивного вывода

Алгоритмы доказательства выводимости А⊦ B, построенные на основе этого метода, применяются во многих системах искусственного интеллекта, а также являются фундаментом, на котором построен язык логического программирования «Пролог».

Идея метода резолюций заключается в том, что доказательство истинности или ложности выдвинутого предположения, например:

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

Если в процессе доказательства возникает противоречие между отрицанием гипотезы и аксиомами, выражающееся в нахождении пустого списка (дизъюнкта), то выдвинутая гипотеза правильна. В методе резолюций множество предложений обычно рассматривается как составной предикат, содержащий несколько предикатов, соединенных логическими функциями и кванторами существования и общности. Так как одинаковые по смыслу предикаты могут иметь разный вид, то предложения преобразуются в клаузальную форму – разновидность конъюнктивной нормальной формы, в которой удалены кванторы существования, всеобщности, символы импликации, равнозначности и др. Клаузальную форму называют сколемовской конъюнктивной формой.

В клаузальной форме вся исходная логическая формула представляется в виде множества предложений (клауз) С, называемых клаузальным множеством:

Любое предложение, из которого образуется клаузальное множество, является совокупностью атомарных предикатов или их отрицаний, соединенных символом дизъюнкции:

Предикат или его отрицание называется дизъюнктом, литералом, атомом, атомарной формулой.

Сущность метода резолюций состоит в проверке того факта, содержит ли клазуальное множество пустое предложение, если не содержащее литер. Если клазуальное множество содержит пустое предложение, то множество противоречиво (невыполнимо).

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

Предложение, вновь сформированное из клауз называется резольвентой.

Например, из клауз:

получится резольвента .

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

Алгоритм метода резолюций в исчислении высказываний

1. Каждый дизъюнкт из КНФ представим в виде , где С - переменные, входящие в дизъюнкт, x_i - выделенная переменная с отрицанием , либо без отрицания .

2. Выбираем контрарную пару дизъюнктов, редуцируем новый дизъюнкт:

Пара дизъюнктов редуцировалась в дизъюнкт ⊦ .

3. Образуем новый список дизъюнктов из дизъюнктов вида: (оставшийся список дизъюнктов). Такой список называется редуцированным.

4. Применяем правило R применяют к редуцированному списку дизъюнктов.

Остановка наступает, когда в списке остаются только два дизъюнкта вида и , либо применение R невозможно.

Список дизъюнктов редуцировался в КНФ .

Алгоритм метода резолюций в исчислении предикатов отличается тем, что формулу логики предикатов необходимо привести к сколемовской форме, затем матрицу формы (предикаты без кванторов) привести к КНФ с помощью законов упрощения формул. После чего также выделяется список дизъюнктов, к которому применяется правило резолюций.

Пример. Методом резолюций проверить выводимость формулы

├ .