 |
Метод семантических деревьев
|
|
|
|
Исчисление семантических деревьев похоже на исчисление по Бету и используется для доказательства непротиворечивости формул, представленных в сколемовской нормальной форме.
Пусть j - предложение, представленное в сколемовской нормальной форме, S - соответствующее j множество дизъюнктов. Если предложение j выполнимо, то оно истинно в некоторой эрбрановской интерпретации. Соответственно, все основные примеры дизъюнктов из S истинны в этой интерпретации. Если предложение j не выполнимо, любая попытка подтвердить основные примеры дизъюнктов из S обречена на неудачу. Это может быть обнаружено за конечное число шагов путем построения конечного множества не выполнимых в эрбрановской интерпретации основных примеров. Согласно теореме Эрбрана эти основные примеры не выполнимы во всех интерпретациях.
Следовательно, вопрос о том, как построить процедуру, которая, имея на входе предложение j и соответствующее множество дизъюнктов,
· останавливается после конечного числа шагов, выдавая в качестве результата конечное множество основных примеров, если j невыполнимо;
· если j выполнимо, процедура, в общем случае, не дает никакого ответа за конечное время, при этом она осуществляет построение эрбрановской интерпретации, на которой истинно j.
Используя эрбрановское множество основных термов и соответствующее ему множество основных примеров, метод доказывает противоречивость множества дизъюнктов путем построения семантического дерева.
Деревом называется связный граф без циклов, одна из вершин которого (единственная) называется корнем. Из корня может быть достигнута любая вершина дерева. Две вершины дерева, связанные ребром (ветвью), находятся в отношении предшествования. T – обозначение дерева; xρy означает: x и y - смежные вершины дерева, вершина x является непосредственным предшественником вершины y, а вершина y – непосредственно следует за вершиной x. В семантическом дереве вершинам x, y соответствуют элементы множества основных примеров с отрицанием или без, входящие в эрбрановское множество.
|
|
|
Пусть S ={C1,…, Cn}– множество дизъюнктов; P1,…, Pl – атомы, входящие в дизъюнкты множества S, {a1,…, an,,…} – эрбрановский универсум множества S.
Семантическим деревом для S называется дерево Т, удовлетворяющее условиям:
1. Корнем дерева является произвольная точка. Вершины, отличные от корня, являются основными примерами атомов P1,…, Pl на эрбрановском универсуме H. Каждая вершина Pi имеет две последующие вершины, а именно Pi +1 (ai1,…, aik) и 
(ai1,…,aik).
2. Каждая ветвь дерева Т, содержащая основные примеры Pi1(al1,… alk),…, Piq(aq1,…, aqk) представляет конъюнкцию этих основных примеров.
3. Дизъюнкция всех конъюнкций ветвей дерева Т для непротиворечивого множества S является общезначимой формулой.
4. Если в какой-либо вершине дерева Т находится атом P(ai1,…,aik), то ни на какой непротиворечивой ветви дерева, проходящей через эту вершину, не может встретиться атом 
.
5. Если при построении дерева Т в какой-либо ветви получена конъюнкция литералов, которая вступает в противоречие с каким-либо основным примером одного из дизъюнктов C1,…, Cn множества S, то эта ветвь считается противоречивой. Множество литералов этой ветви образует неподтверждаемое множество основных примеров.
Построение семантического дерева для множества S начинается с произвольной точки, которая является корнем дерева. Одна из смежных с корнем вершин обозначается именем одного из основных примеров, 
, а другая - 
. Если множество S содержит дизъюнкт, состоящий из единственного литерала P(ai1,…,aik), то ветвь, содержащая противоречива, а вершина является заключительной вершиной данной ветви. Построение продолжается по левой ветви, Рис. 10.
|
|
|
·
| |||
|
Предположим, что – не заключительная вершина. Тогда из нее исходят две ветви к двум вершинам дерева, которые обозначаются каким-либо другим атомом предложения, еще не встречавшимся в этой ветви. Цель построения: достичь заключительной вершины, исчерпав все атомы из S, если противоречивость ветви не обнаружится раньше.
Определения:
1. Множество дизъюнктов S опровергается семантическим деревом, если существует семантическое дерево для S, все ветви которого противоречивы.
2. Ветвь семантического дерева множества дизъюнктов S называется полной, если для всех основных примеров P(ai,…,an) каждого атома Р в этой ветви содержатся P(ai,…,an) или Ø P(ai,…,an).
Пусть дано предложение
.
Соответствующее теоретико-множественное представление для него имеет вид:
где цифры под множествами, обозначающими дизъюнкты, указывают номер дизъюнкта. Поскольку в списке аргументов литералов множества S отсутствуют константы, необходимо выбрать любую константу из предметной области. Пусть это будет a. Тогда эрбрановский универсум будет иметь вид H={a, f(a), f(f(a)), f(f(f(a))),…}.
Множество основных примеров получается подстановкой в литералы поочередно всех основных термов из эрбрановского множества: { P(a), Q(a), P(f(a)), Q(a), Q(f(a)),… }.
Семантическое дерево Т для S изображено на рисунке 11. Противоречивая ветвь дерева завершается значком. Справа от него указан номер дизъюнкта, ответственного за противоречие.
Вторая ветвь дерева представляет конъюнкцию
.
Второй дизъюнкт множества S имеет вид 
Поэтому формула 
должна быть истинной для всех основных термов.
Конъюнкция 
вступает в противоречие со вторым дизъюнктом множества S, так как
Следовательно, рассматриваемая ветвь дает противоречие со вторым дизъюнктом из множества S.
Порядок выбора очередного элемента из Н для подстановки в атомы из множества S произволен.
Примем без доказательства следующую формулировку теоремы Эрбрана: если множество дизъюнктов S невыполнимо, то S опровергается семантическим деревом.
|
|
|
Фактически теорема Эрбрана дает возможность при проверке выполнимости предложения (непротиворечивости множества дизъюнктов S) использовать методы логики высказываний, например, метод семантических таблиц или метод резолюций.
·
Если S не выполнимо, то существует множество основных примеров, для которых конъюнкция дизъюнктов из множества S ложна. Таким образом, для множества дизъюнктов S эрбрановская интерпретация определяет все основные примеры и, используя систематическую процедуру (например, семантическое дерево), позволяет определить множество основных примеров, на которых данное предложение ложно.
Если S выполнимо, эта процедура будет продолжаться бесконечно.
Приведем пример выполнимого множества дизъюнктов. Пусть дано предложение 
Преобразуя это выражение к сколемовской нормальной форме, получим
Соответствующее множество дизъюнктов имеет вид
S={{ØP(x,y), P[a, f(x,y)]}}.
Эрбрановский универсум для этого множества дизъюнктов имеет вид H={a, f(a,a), f(a, f(a,a)), f(f(a), a), f(f(a,a), f(a,a)),…}.
Основными примерами атомов из S являются {P(a,a), P(a, f(a,a)), P(f(a,a), a), P(f(a,a) f(a,a)),…}. Семантическое дерево для множества S представлено на рис. 12.
|
     
         ·
|
Часть ветвей этого бесконечного семантического дерева противоречива. Остальные ветви по своей конструкции не являются противоречивыми, так как конъюнкция их атомов не противоречит единственному дизъюнкту множества S.
|
|
|
