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

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

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

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

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

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

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

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

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

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

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

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

В предыдущем параграфе мы видели, что для получения ответа на вопрос о выполнимости множества дизъюнктов можно рассматривать не все интерпертации, а только H-интерпретации. В данном параграфе мы в этом направлении продвинемся еще дальше. Мы фактически покажем, что для решения упомянутого вопроса можно ограничиться конечными подмножествами эрбрановского универсума. Основным понятием этого параграфа будет понятие семантического дерева.

На дерево будем смотреть, как на корневое ориентированное дерево. Изображать дерево будем растущим вниз, ориентацию дуг указывать не будем. Напомним, что листом дерева называется вершина, из которой не выходит не одна дуга. Путь в дереве – это последовательность дуг e1,e2,…,ek,… такая, что если дуга ei заходит в вершину v, то дуга ei+1 выходит из этой вершины. Путь в дереве называется максимальным, если к нему нельзя добавить ни одной дуги. Для каждой вершины существует единственный путь от корня к этой вершине. Если вершина является листом, то этот путь максимален. Если p – путь в дереве, то через I(p) будем обозначать объединение всех литералов, принадлежащим дугам пути. В случае, когда p – путь от корня до вершины v, то вместо I(p) будем писать I(v). Мы будем использовать понятие поддерева несколько в ином смысле, нежели в теории графов. А именно, поддеревом дерева Т будем называть подграф T′, удовлетворяющий следующим условиям:

1) T′ – дерево;

2) T′ содержит корень дерева Т,

3) если из v в v′ идет дуга в дереве T, v и v′Î T′, то T′ содержит все вершины, в которые из v идет дуга.


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

1. Из любой вершины выходит конечное число дуг e1,…,ek; если ci – конъюнкция литералов, приписанных дуге ei, то c1Úc2ÚÚck – тождественно истинная формула.

2. Для любой вершины v множество I(v) не содержит противоположных литералов.


Рассмотрим примеры. Пусть S – множество дизъюнктов из примера 2 предыдущего параграфа, B – его эрбрановский базис. Напомним, что B{P(a), Q(a), R(a)}. Для простоты в примерах вместо P(a), Q(a) и R(a) будем писать просто P,Q,R. На рисунках 4.4 и 4.5 приведены примеры семантических деревьев для S. Семантическое дерево может быть бесконечным. На рисунке 4.6 приведен пример семантического дерева для множества дизъюнктов S из примера 1 §4. Напомним, что эрбрановский базис в этом случае есть B{P(a), Q(a), P(f(a)), Q(f(a)),…}.


Рис. 4.4


Рис. 4.5


Рис. 4.6


Определение. Пусть B – эрбрановский базис множества дизъюнктов S. Семантическое дерево Т называется полным, если для любого элемента А базиса B множество I(p) содержит либо А, либо ØА.

Семантические деревья, изображенные на рис.4.4 и 4.6 являютя полными, а семантическое дерево изображенное на рис.4.5 – неполным.


Определение. Вершина v семантического дерева называется опровергающей, если I(v) опровергает основной пример некоторого дизъюнкта S. Вершина v называется максимальной опровергающей, если вершина v′, предшествующая v, опровергающей не является.


Рассмотрим в качестве примера дерево, изображенное на рис.4.5. Напомним, что оно является семантическим деревом множества дизъюнктов S={P(x), Q(x)ÚØR(y)}. Вершины v1 и v3 будут опровергающими вершинами, так как множество I(v1), равное {ØQ(a)&R(a), P(a)}, опровергает основной пример Q(a)ÚØR(a) дизъюнкта Q(x)ÚØR(y), а множество I(v3), равное {R(a),ØP(a)&ØQ(a)} опровергает основной пример P(a) дизъюнкта P(x). Вершина v1 будет максимальной опровергающей, а вершина v3 не будет максимальной, потому что опровергающей является предшествующая ей вершина v4. Вершина v2 опровергающей не является.

Определение. Вершина v семантического дерева называется выводящей, если все непосредственно следующие за ней вершины являются максимальными опровергающими.

Пусть S={P(x), ØP(x)ÚQ(f(y)), ØQ(f(a))} множество дизъюнктов примера 1 предыдущего параграфа. Дерево, изображенное на рис.4.7, является семантическим деревом для S. Вершина v этого дерева является выводящей вершиной, а никакие другие вершины выводящими не являются.


Рис. 4.7


Определение. Семантическое дерево называется замкнутым, если каждый его лист является максимальной опровергающей вершиной.

Дерево, изображенное на рис.4.4, замкнуто, а деревья на рис.4.5 и 4.6 незамкнуты.


Следующее утверждение – знаменитая теорема математической логики, которая является основой многих алгоритмов доказательства теорем. Она называется теоремой Эрбрана.


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


Доказательство теоремы 4.6 использует известное математике утверждение, которое называется леммой Кенига. Сформулируем ее.


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

Доказательство леммы Кенига приводить не будем. С ним можно познакомиться по книге С.Клини, указанной в списке литературы.


Приведем доказательство теоремы 4.6. Докажем вначале необходимость. Пусть множество дизъюнктов S невыполнимо и Т – полное семантическое дерево для S. Рассмотрим максимальный путь p в дереве Т. По определению полного семантического дерева для каждой атомарной формулы А эрбрановского базиса B, либо А, либо ØА принадлежит I(p). Это означает, что I(p) есть H-интерпретация множества S. Поскольку S невыполнимо, то I(p) опровергает основной пример D′ некоторого дизъюнкта D из S. Дизъюнкт D′ конечен, поэтому путь p должен проходить через максимальную опровергающую вершину дерева Т. В каждом максимальном пути отметим такую вершину. Пусть Т – корневое поддерево дерева Т, листьями которого являются отмеченные вершины. В силу леммы Кенига. Т′ – конечное поддерево дерева Т. Дерево T′ по построению является замкнутым. Необходимость доказана.

Докажем достаточность. Пусть полное семантическое дерево Т содержит конечное замкнутое поддерево T′. По определению поддерева (см.начало данного параграфа) отсюда следует, что каждый максимальный путь дерева Т содержит опровергающую вершину. Множество всех максимальных путей полного семантического дерева исчерпывает все H-интерпретации множества S. Следовательно S ложно при всех H-интерпретациях. По теореме 4.5 S невыполнимо.

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

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

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

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

Задачи

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

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

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

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


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

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