Семантические деревья
Исчисление семантических деревьев
похоже на исчисление по Бету.
Следовательно,
вопрос о том, как построить процедуру,
которая, имея на входе предложение
и соответствующее множество дизъюнктов,
Т.е. с помощью этой процедуры мы хотим
получить доказательство невыполнимости
предложения или контрпример. При
построении такой процедуры используются
семантические деревья.
Деревом
называется связный граф без циклов,
одна из вершин которого (единственная)
называется корнем. Из корня может быть
достигнута любая вершина дерева. Две
вершины дерева, связанные ребром (ветвью)
находятся в отношении предшествования
. T=(x,
r)
— дерево, xry
означает: x
является непосредственным предшественником
y,
а y
– последователем x.
Здесь x,y
-элементы из множества основных примеров
с отрицанием или без.
Семантическим
деревом для Sназывается
дерево Т, удовлетворяющее следующим
условиям:
1
2 3
Семантическое
дерево Т для S
изображено на рисунке 5.
имвол
означает противоречие. Справа от
него указан номер дизъюнкта, ответственного
за это противоречие. Посмотрим, почему
вторая ветвь противоречива. Эта ветвь
представляет конъюнкцию
Отсюда
мы имеем также Q(f(a))&P(a) =(Q(f(a))P(a)).
Следовательно, рассматриваемая ветвь
дает противоречие со вторым дизъюнктом
множестваS.
Порядок
выбора очередного элемента из Н для
подстановки в атомы из множества Sпроизволен.
Если
множество дизъюнктов S
невыполнимо, то S
опровергается семантическим деревом.
Фактически
теорема Эрбрана предоставляет возможность
при проверке выполнимости предложения
или множества дизъюнктов Sиспользовать методы логики высказываний,
например, метод семантических таблиц
или метод резолюций. ЕслиSневыполнимо, то существует множество
основных примеров дизъюнктов множестваS, которое также будет
невыполнимым. Это конечное множество
состоит из высказыванийPL,
и его невыполнимость может быть обнаружена
известными методами. Таким образом,
для каждого множества дизъюнктовSмы перечис-
Рисунок
6 Семантическое дерево
P(a)
P(a)
ляем
все основные примеры дизъюнктов из S. При этом систематически проверяем
выполнимость каждого конечного множества
основных примеров, пользуясь методами
логики высказываний. ЕслиSневыполнимо, такая проверка покажет,
что одно из конечных подмножеств
невыполнимо. ЕслиSвыполнимо, эта процедура будет продолжаться
бесконечно.
Приведем
пример выполнимого множества дизъюнктов.
Пусть дано предложение
СНФ
предложения имеет вид:
Соответствующее
множество дизъюнктов имеет вид:
Это
бесконечное семантическое дерево
содержит одну противоречивую ветвь.
Остальные ветви по своей конструкции
не являются противоречивыми, так как
конъюнкция их атомов не противоречит
единственному дизъюнкту множества S.
В предыдущем параграфе мы видели, что для
получения ответа на вопрос о выполнимости множества дизъюнктов можно
рассматривать не все интерпертации, а только H-интерпретации. В данном параграфе мы в этом
направлении продвинемся еще дальше. Мы фактически покажем, что для решения
упомянутого вопроса можно ограничиться конечными подмножествами эрбрановского
универсума. Основным понятием этого параграфа будет понятие семантического
дерева.
1) T′ – дерево;
2) T′ содержит корень дерева Т,
3) если из v в v′ идет дуга в дереве T, v и v′ T′,
то T′ содержит все вершины, в которые из v идет дуга.
Определение.
Пусть S – множество дизъюнктов, B – эрбрановский базис для S. Семантическим
деревом для S называется
корневое дерево, каждой дуге которого приписано непустое множество формул из B или их отрицаний так, что выполнены следующие
условия.
2. Для любой вершины v множество I(v) не содержит
противоположных литералов.
Определение. Пусть
B – эрбрановский
базис множества дизъюнктов S. Семантическое дерево Т называется полным, если для любого элемента А базиса B множество I() содержит либо А, либо А.
Семантические
деревья, изображенные на рис.4.4 и 4.6 являютя полными, а семантическое дерево
изображенное на рис.4.5 – неполным.
Определение. Вершина v семантического дерева называется опровергающей, если I(v) опровергает основной пример некоторого дизъюнкта S. Вершина v называется максимальной опровергающей, если вершина v′, предшествующая v, опровергающей не является.
Определение. Вершина v семантического дерева называется выводящей, если все непосредственно
следующие за ней вершины являются максимальными опровергающими.
Определение. Семантическое дерево
называется замкнутым, если каждый его
лист является максимальной опровергающей вершиной.
Дерево,
изображенное на рис.4.4, замкнуто, а деревья на рис.4.5 и 4.6 незамкнуты.
Следующее
утверждение – знаменитая теорема математической логики, которая является
основой многих алгоритмов доказательства теорем. Она называется теоремой
Эрбрана.
Теорема 4.6. Множество дизъюнктов S невыполнимо тогда и только
тогда, когда любое полное семантическое дерево множества S имеет конечное замкнутое поддерево.
Доказательство
теоремы 4.6 использует известное математике утверждение, которое называется
леммой Кенига. Сформулируем ее.
Лемма. Если Т –
бесконечное дерево, из каждого узла которого выходит конечное число дуг. Тогда
дерево Т содержит бесконечный
путь, начинающийся от корня.
Доказательство
леммы Кенига приводить не будем. С ним можно познакомиться по книге С. Клини,
указанной в списке литературы.
Приведем
доказательство теоремы 4.6. Докажем вначале необходимость. Пусть множество
дизъюнктов S
невыполнимо и Т – полное семантическое дерево для S. Рассмотрим максимальный путь в
дереве Т. По определению полного семантического дерева для каждой атомарной
формулы А эрбрановского базиса B,
либо А, либо А
принадлежит I().
Это означает, что I()
есть H-интерпретация
множества S. Поскольку S невыполнимо, то I()
опровергает основной пример D′
некоторого дизъюнкта D из S.
Дизъюнкт D′ конечен,
поэтому путь должен проходить через максимальную опровергающую
вершину дерева Т. В каждом максимальном пути отметим такую вершину. Пусть Т –
корневое поддерево дерева Т, листьями которого являются отмеченные вершины. В
силу леммы Кенига. Т′ – конечное поддерево дерева
Т. Дерево T′
по построению является замкнутым. Необходимость доказана.
Докажем
достаточность. Пусть полное семантическое дерево Т содержит конечное замкнутое
поддерево T′.
По определению поддерева (см.начало данного параграфа) отсюда следует, что
каждый максимальный путь дерева Т содержит опровергающую вершину. Множество
всех максимальных путей полного семантического дерева исчерпывает все H-интерпретации множества S. Следовательно S ложно при всех H-интерпретациях. По теореме
4.5 S невыполнимо.
Основная проблема
автоматического доказательства теорем
заключается в построении универсальной
процедуры, которая позволяла бы проверить,
является ли предложение логики предикатов
общезначимым или нет.
Тьюринг, Черчь.
Доказали, что такой универсальной
процедуры не существует.
Эрбран.
Предложил алгоритм построения
интерпретации (эрбрановской интерпретации),
опровергающей формулу .
Если
— общезначима, то опровергающей
интерпретации не существует, и алгоритм
в этом случае останавливается через
конечное число шагов.
Эрбрановский
универсум предложения
ЭУ — это множество объектов
(область определения эрбрановской
интерпретации), на котором принимают
значения термы предложения .
Алгоритм
(построения эрбрановского универсума)
Пусть
— предложение PrL
и S
– соответствующее
множество дизъюнктов. Итерационная
схема:
Определение
(Эрбрановской интепретации) Пусть S
– множество дизъюнктов, H
– эрбрановский универсум, соответствующий
S.
Множество
H
называется эрбрановской
интерпретацией для S,
если
Теорема
(об эрбрановских интерпретация) Пусть
— универсальное предложение (в СНФ) и S
– соответствующее множество дизъюнктов.
Предложение
выполнимо (истинно в некоторой
интерпретации) тогда и только тогда,
если
выполнимо в эрбрановской интерпретации.
Замечание.
Если
невыполнимо в эрбрановской интерпретации,
то не существует интерпретации, в которой
истинно.
Основным примером
дизъюнкта
S
называется предложение ’,
полученное из
путем замены в
переменных на
константы.
По теореме об эрбрановских
интерпретациях:
если
выполнимо в некоторой интерпретации,
то
истинно и в эрбрановской интерпретации.
Для того чтобы предложение
было истинно в эрбрановской интерпретации,
достаточно, чтобы были истинны в
эрбрановской интерпретации все основные
примеры дизъюнктов
S.
Если
невыполнимо, то не существует и
подтверждающей
эрбрановской интепретации. Т.е. найдется
конечное множество основных примеров
дизъюнктов
S,
опровергающих .
Метод семантических
деревьев –
регулярная процедура построения всех
основных примеров дизъюнктов. Если
невыполнимо, то на некотором шаге метода
будет построено множество основных
примеров дизъюнктов
S,
опровергающих .
Основной пример атома
(в методе семантических деревьев)
Пример 1.
Рассмотрим предложение
Семантическим деревом
для S
называется дерево T
со следующими свойствами:
Пример 1
(продолжение). Требуется проверить
выполнимость следующего предложения:
Соответствующее множество
дизъюнктов имеет вид:
Построение семантического
дерева T
Выводы.
Все ветви дерева T
противоречивы, следовательно, не
существует эрбрановской интерпретации,
подтверждающей множество дизъюнктов
Невыполнимое множество
основных примеров дизъюнктов
(в это множество включаются только те
основные примеры дизъюнктов, которые
были использованы для объявления
некоторой ветви противоречивой) имеет
вид:
т.е. следующая формула
неподтверждаема:
Пример 2.
Требуется проверить выполнимость
следующего предложения:
Выводы.
Левая крайняя ветвь содержит только
основные примеры атомов, а правая –
только их отрицания и являются
непротиворечивыми. Каждой из этих ветвей
соответствует эрбрановская интерпретация.
Следовательно, исходное предложение
является выполнимым.
Задание 6.
Методом семантических таблиц требуется
проверить выполнимость следующего
предложения:
Здесь b
– константа, f(),
g()
– функциональные символы, P(),
Q()
— предикаты. Если предложение
невыполнимо, нужно построить невыполнимое
множество основных примеров дизъюнктов.
Множества
H(S), A,
F,
у всех Н
— интерпретаций сов-падают. Различаются
только значения предикатов, которые
могут быть либо равны атомам из
эрбрановского базиса А,
либо противоположны им. Каждый атом Аi
А входит в
одну интерпретацию один раз — либо как
Аi,
либо как
Аi.
Пара Аi
и
Аi
называется контрарной.
Определение.
Полным
семантическим деревом Т(S)
множества дизъюнктов S
называется растущее вниз бинар-ное
дерево, в котором из самой верхней
вершины — корня (узел 0-го
уровня) выходит пара рёбер А1
и А1
, из каждого узла
i -го уровня
— пара рёбер Аi
и
Аi
.
Очевидно,
при счетном эрбрановском базисе число
уровней дерева Т(S
) и длина
ветвей в нем (число узлов) счетны. Каждая
ветвь в Т(S )
задаёт одну Н
– интерпре-тацию, а все дерево описывает
полное множество Н-интер-претаций
множества дизъюнктов S.
Рассмотрим
полное семантическое дерево Т(S),
соот-ветствующее некоторой невыполнимой
формуле В.
Если S –
множество дизъюнктов, соответствующее
В, то это
озна-чает, что каждая Н
— интерпретация опровергает хотя бы
один из его дизъюнктов Di.
Поскольку каждый дизъюнкт Di
содержит конечное число литер, то его
опровержение должно произойти в некотором
внутреннем узле полного семантического
дерева Т(S).
Определение.
Узел j
полного семантического дерева Т(S)
называется опровергающим,
если все интерпретации
I(j), содержащие
его, опровергают некоторый основной
при-мер дизъюнкта Di
S,
а все узлы, лежащие выше
j , не
опро-вергают ни одного из Di
S.
Для
определённости будем считать, что атомы
базиса P = И,
Q=И, R=И, а их
отрицания — ложны. Тогда
а)
узел 2 будет опровергать дизъюнкт D4
= PS
,
б)
узел 4 будет опровергать дизъюнкт D1
=
P
Q
S,
в)
узел 7 будет опровергать дизъюнкт D2
=
Q
R
S,
г)
узел 8 будет опровергать дизъюнкт D3
=
P
R
S.
Если
некоторый узел
j полного
семантического дере-ва Т(S)
является
опровергающим, то поддерево, выходящее
из него, можно не рассматривать, поскольку
все интерпре-тации, проходящие по этим
узлам, будут опровергающими. Следовательно,
его можно не показывать на схеме.
Определение.
Семантическое дерево Тз(S)
называется
закрытым,
если каждая его ветвь заканчивается
опровер-гающим узлом.
Семантическое
дерево Т(S) в
Примере 2 является за-крытым. Для таких
деревьев применяют специальные
изо-бражения, на которых опровергающие
узлы перечёркивают и отбрасывают
поддеревья, выходящие из них. Дерево
Тз(S)
из Примера
2 примет при этом следующий вид:
Теорема
Эрбрана.
Множество дизъюнктов S
невы-полнимо
когда любому полному семантическому
дереву T(S)
соответствует
конечное закрытое семантическое дерево
Тз(S).
Существование
закрытого семантического дерева
Тз(S)
указывает на то, что любая Н
— интерпретация приводит к появлению
ложных дизъюнктов в S
, что эквивалентно опровержимости S
.
Алгоритм
проверки невыполнимости формул при
помощи семантического дерева.
1.
Формула В
представляется в виде пренексной
нормаль-ной формы В
с матрицей М
в виде конъюнкции дизъ-юнктов.
2.
Путем устранения кванторов существования
В
приво-дится к скулемовской форме,
бескванторная часть которой рассматривается
как множество дизъюнктов S.
3.
Строится эрбрановский универсум H(S)
и эрбрановский
базис А.
4.
Строится семантическое дерево по
уровням. В каждом из них производится
проверка узлов j
на опровержимость
(бу-дут ли интерпретации I(j)
опровергать
хотя бы один дизъ-юнкт Di
из S).
Если
узел j является
опровержимым, то узел отме-чается (обычно
— зачеркиванием) и дальнейшее построение
дерева из него прекращается.
Если
узел j не
является опровержимым, то построение
дерева из него продолжается.
5.
Если на некотором шаге дальнейшее
построение дерева оказалось невозможным
(поскольку все построенные кон-цевые
узлы оказались опровержимыми), то
множество дизъ-юнктов S
, а,
следовательно, и исходная формула
В – невы-полнимы.
Если
построение семантического дерева
продолжает-ся, то на вопрос о невыполнимости
S
нельзя дать ни поло-жительный, ни
отрицательный ответ.
