Дискретная математика

Раздел 1. Математическая логика

Тема 1. Логика высказываний

Тема 2. Булевы функции

Тема 3. Логика предикатов

Тема 4. Метод резолюций

Тема посвящена рассмотрению метода доказательства того, что формула G является логическим следствием формул F1,F2,...,Fk, который называется методом резолюций. Отметим, что задача о логическом следствии сводится к задаче о выполнимости. Действительно, формула G есть логическое следствие формул F1,F2,...,Fk тогда и только тогда, когда множество формул {F1,F2,...,Fk,ØG} невыполнимо. Метод резолюций, если говорить более точно, устанавливает невыполнимость. Это первая особенность метода. Вторая особенность метода состоит в том, что он оперирует не с произвольными формулами, а с дизъюнктами (или элементарными дизъюнкциями).

§1. Метод резолюций в логике высказываний

§2. Подстановка и унификация

§3. Метод резолюций для логики первого порядка

§4. Эрбрановский универсум множества дизъюнктов

§5. Семантические деревья, теорема Эрбрана

§6. Полнота метода резолюций в логике предикатов

Параграф посвящен доказательству теоремы 4.3. Напомним ее формулировку.


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


Доказательство. Пусть множество дизъюнктов S невыполнимо и B={A1,A2,…,An,…} – эрбрановский базис для S. Рассмотрим полное семантическое дерево Т, изображенное на рис.4.8.


Рис. 4.8


По теореме Эрбрана Т содержит конечное замкнутое семантическое поддерево Т/. Если Т/ состоит только из корня, то □ÎS и поэтому □ выводим из S. Предположим, что Т/ состоит не только из корня. Тогда Т/ имеет вершину v, потомки v1 и v2 которой являются максимальными опровергающими для множества S вершинами. Пусть


I(v)={L1, L2,…, Lk},

I(v1)={L1, L2,…,Lk, Ak+1},

I(v2)={L1, L2,…, Lk, ØAk+1}.


Существует дизъюнкт D1ÎS такой, что его основной пример D1/ опровергается в I(v1), и существует дизъюнкт D2ÎS такой, что его основной пример D2/ опровергается в I(v2). Так как дизъюнкты D1/ и D2/ не опровергаются в I(v), то D1/ содержит ØAk+1, а D2/ – Ak+1. Применим к D1/ и D2/ правило резюлюций, отрезая литералы ØAk+1 и Ak+1, получим дизъюнкт D/:


D/=(D1/ ØAk+1)È(D2/ – Ak+1).


Отметим, что дизъюнкт D1/ – Ak+1 ложен в I(v), поскольку в противном случае, D1/ был бы истинен в I(v1). Аналогично заключаем, что D2/ – Ak+1 ложен в той же интерпретации I(v).

Отсюда следует, что D/ ложен при I(v).

По лемме о подъеме (теорема 4.4) существует дизъюнкт D, который является резольвентой дизъюнктов D1 и D2. Ясно, что D опровергается в I(v). Рассмотрим множество дизъюнктов SÈ{D}. Замкнутое семантическое дерево T// для этого множества дизъюнктов можно получить вычеркиванием некоторых вершин (и идущих в них дуг) дерева T/. А именно, в дереве T/ вычеркиваем все дуги и вершины, которые лежат ниже первой вершины, где дизъюнкт D/ ложен. Полученное таким образом дерево T// содержит меньше вершин, нежели дерево T/, так как v1,v2ÏT//.

Применим описанный выше процесс к T//, мы получим резольвенту дизъюнктов из SÈ{D}. Расширим множество SÈ{D} за счет этой резольвенты, придем к конечному замкнутому дереву с меньшим числом вершин, нежели T//. В конце концов, получим замкнутое семантическое дерево, состоящее только из корня. Это возможно, лишь в случае, когда множество S, расширенное резольвентами, содержит пустой дизъюнкт, Следовательно, □ выводим из S. Необходимость условия теоремы доказана.

Докажем достаточность. Пусть пустой дизъюнкт выводим из S, и D1,D2,…,Dn=□ – вывод из S. Предположим, что S выполнимо в некоторой интерпретации. Тогда, поскольку правила резолюций и правило склейки сохраняют истинность, то все дизъюнкты вывода, в том числе и пустой, являются истинными в этой интерпретации. Полученное противоречие доказывает, что S невыполнимо.

Теорема доказана.

§7. Стратегии метода резолюций

§8. Применение метода резолюций.

§9. Метод резолюций и логическое программирование

Задачи

Ответы, указания и решения

Раздел 2. Теория графов

Тема 5. Раскраски

Тема 6. Ориентированные графы и сети


Fair.ru Ярмарка сайтов
Rambler's Top100 Submitter.ru - Free promoting

Дизайн: Alex © 2002
Все вопросы и предложения можно направлять по адресу cad@mail.ustu.ru