Скачать 13.21 Кбайт
Обратный метод С.Ю. Маслова
Так как формула Ф находится в дизъюнктивной нормальной форме, то секвенциальное исчисление содержит лишь одно ПРАВИЛО ВЫВОДА:
n–кратное ® B, A1, C; ® B, A2, C; … ® B, An, C;
правило ® & ® B, A1 & A2 & … & An, C
Для полноты исчисление содержит еще одно правило — n-кратное правило ® Ъ. Однако применение n-кратного правило ® Ъ (применение его "сверху вниз") и соответственно контрприменение правила (применение правила "снизу вверх") при данном типе формул является тривиальным: все запятые (,) можно просто заменить знаками дизъюнкции (Ъ) во всей формуле Ф (соответственно, при контрприменении правила — наоборот). Условимся, что тривиальное n-кратное правило ® Ъ будет применяться автоматически в самом начале поиска вывода любой формулы. Заметим, что правило сечения является допустимым для введенного секвенциального исчисления, а структурные правила избыточны.
АКСИОМАМИ данного исчисления являются секвенции вида ® A, X, ~X, B, которые содержат контрарную пару литер.
ВЫВОДОМ формулы Ф называется дерево, полученное применением правил вывода, в концевых вершинах которого стоят аксиомы, а в корне дерева — формула Ф.
Пусть Ф = ~c Ъ b&a Ъ ~a&d&c Ъ ~b&~d Ъ ~b&d Ъ ~a&c&~d Ъ ~c&x&y (или
~c Ъ ba Ъ ~adc Ъ ~b~d Ъ ~bd Ъ ~ac~d Ъ ~cxy, где знак & опущен)
Построим некоторое дерево поиска вывода данной Ф формулы в сформулированном секвенциальном исчислении. Начинаем построение дерева с исходной формулы Ф. Используя свойство обратимости правил вывода, сначала контрприменяем правило ® Ъ, а потом — последовательно — правило ® &. Строим дерево поиска вывода снизу вверх (см. рис.1), последовательно "расщепляя" дизъюнкты формулы Ф до литер (расщепляемые дизъюнкты обозначены в квадратных скобках). Продолжаем этот процесс построения дерева до тех пор, пока в узлах дерева не будет получена контрарная пара литер (этот узел помечается знаком Д) или во всех концевых вершинах дерева останутся только литеры формулы Ф (в этом случае формула Ф — невыводима):
Д Д Д
® ~c, a, d, ~b~d, ~bd, ~a, … ® ~c, a, d, ~b~d, ~bd, c, … ® ~c, a, d, ~b~d, ~bd, ~d, …
Д [6] Д
® ~c, a, ~a, … ® ~c, a, d, ~b~d, ~bd, ~ac~d, ~cxy ® ~c, a, c, …
Д Д
® ~c, b, ~adc, ~d, ~b, … ® ~c, b, ~adc, ~d, d, …
Д [5]
® ~c, b, ~adc, ~b, … ® ~c, b, ~adc, ~d, ~bd, ~ac~d, ~cxy [3]
[4]
® ~c, b, ~adc, ~b~d, ~bd, ~ac~d, ~cxy ® ~c, a, ~adc, ~b~d, ~bd, ~ac~d, ~cxy
[2]
® ~c, ba, ~adc, ~b~d, ~bd, ~ac~d, ~cxy
рис.1
Все концевые секвенции дерева поиска "замкнуты" ("замкнутость" секвенции будем обозначать знаком Д), т.е. содержат контрарную пару литер, например: a и ~a — в секвенциях 3 (лев.) и 6 (лев.), b и ~b — в секвенции 4 (лев.). Наличие одной контрарной пары литер достаточно для определения "замкнутости" какой-либо секвенции, поэтому все другие литеры и формулы "замкнутой" секвенции несущественны и помечены многоточием. Так как все концевые вершины дерева поиска вывода представляют аксиомы исчисления (помечены знаком Д), то получен вывод формулы Ф.
Отметим несколько особенностей полученного дерева вывода:
1. Во всех концевых вершинах содержатся только те литеры (возможно "нерасщепленные" дизъюнкты), которые принадлежат исходной формуле Ф, причем если Ф выводима, то во всех концевых вершинах содержатся контрарные пары литер.
2. Нет необходимости продолжать "расщепление" дизъюнктов формулы дальше, если получена хоть одна контрарная пара литер.
3. Правило вывода ® & при контрприменении действует локально, т.е. добавляет на каждом уровне построения дерева лишь одну новую в каждую ветвь дерева.
4. При построении дерева поиска вывода были использованы некоторые интуитивные соображения: например, нецелесообразно работать ("расщеплять") с последним дизъюнктом формулы Ф, в составе которого встречаются литеры Х и У, так как эти литеры ни в каких дизъюнктах больше не встречаются. Видимо, более целесообразно работать с теми дизъюнктами, которые лучше "зацеплены" с другими дизъюнктами.
n–кратное ® B, A1, C; ® B, A2, C; … ® B, An, C;
правило ® & ® B, A1 & A2 & … & An, C
Для полноты исчисление содержит еще одно правило — n-кратное правило ® Ъ. Однако применение n-кратного правило ® Ъ (применение его "сверху вниз") и соответственно контрприменение правила (применение правила "снизу вверх") при данном типе формул является тривиальным: все запятые (,) можно просто заменить знаками дизъюнкции (Ъ) во всей формуле Ф (соответственно, при контрприменении правила — наоборот). Условимся, что тривиальное n-кратное правило ® Ъ будет применяться автоматически в самом начале поиска вывода любой формулы. Заметим, что правило сечения является допустимым для введенного секвенциального исчисления, а структурные правила избыточны.
АКСИОМАМИ данного исчисления являются секвенции вида ® A, X, ~X, B, которые содержат контрарную пару литер.
ВЫВОДОМ формулы Ф называется дерево, полученное применением правил вывода, в концевых вершинах которого стоят аксиомы, а в корне дерева — формула Ф.
Пусть Ф = ~c Ъ b&a Ъ ~a&d&c Ъ ~b&~d Ъ ~b&d Ъ ~a&c&~d Ъ ~c&x&y (или
~c Ъ ba Ъ ~adc Ъ ~b~d Ъ ~bd Ъ ~ac~d Ъ ~cxy, где знак & опущен)
Построим некоторое дерево поиска вывода данной Ф формулы в сформулированном секвенциальном исчислении. Начинаем построение дерева с исходной формулы Ф. Используя свойство обратимости правил вывода, сначала контрприменяем правило ® Ъ, а потом — последовательно — правило ® &. Строим дерево поиска вывода снизу вверх (см. рис.1), последовательно "расщепляя" дизъюнкты формулы Ф до литер (расщепляемые дизъюнкты обозначены в квадратных скобках). Продолжаем этот процесс построения дерева до тех пор, пока в узлах дерева не будет получена контрарная пара литер (этот узел помечается знаком Д) или во всех концевых вершинах дерева останутся только литеры формулы Ф (в этом случае формула Ф — невыводима):
Д Д Д
® ~c, a, d, ~b~d, ~bd, ~a, … ® ~c, a, d, ~b~d, ~bd, c, … ® ~c, a, d, ~b~d, ~bd, ~d, …
Д [6] Д
® ~c, a, ~a, … ® ~c, a, d, ~b~d, ~bd, ~ac~d, ~cxy ® ~c, a, c, …
Д Д
® ~c, b, ~adc, ~d, ~b, … ® ~c, b, ~adc, ~d, d, …
Д [5]
® ~c, b, ~adc, ~b, … ® ~c, b, ~adc, ~d, ~bd, ~ac~d, ~cxy [3]
[4]
® ~c, b, ~adc, ~b~d, ~bd, ~ac~d, ~cxy ® ~c, a, ~adc, ~b~d, ~bd, ~ac~d, ~cxy
[2]
® ~c, ba, ~adc, ~b~d, ~bd, ~ac~d, ~cxy
рис.1
Все концевые секвенции дерева поиска "замкнуты" ("замкнутость" секвенции будем обозначать знаком Д), т.е. содержат контрарную пару литер, например: a и ~a — в секвенциях 3 (лев.) и 6 (лев.), b и ~b — в секвенции 4 (лев.). Наличие одной контрарной пары литер достаточно для определения "замкнутости" какой-либо секвенции, поэтому все другие литеры и формулы "замкнутой" секвенции несущественны и помечены многоточием. Так как все концевые вершины дерева поиска вывода представляют аксиомы исчисления (помечены знаком Д), то получен вывод формулы Ф.
Отметим несколько особенностей полученного дерева вывода:
1. Во всех концевых вершинах содержатся только те литеры (возможно "нерасщепленные" дизъюнкты), которые принадлежат исходной формуле Ф, причем если Ф выводима, то во всех концевых вершинах содержатся контрарные пары литер.
2. Нет необходимости продолжать "расщепление" дизъюнктов формулы дальше, если получена хоть одна контрарная пара литер.
3. Правило вывода ® & при контрприменении действует локально, т.е. добавляет на каждом уровне построения дерева лишь одну новую в каждую ветвь дерева.
4. При построении дерева поиска вывода были использованы некоторые интуитивные соображения: например, нецелесообразно работать ("расщеплять") с последним дизъюнктом формулы Ф, в составе которого встречаются литеры Х и У, так как эти литеры ни в каких дизъюнктах больше не встречаются. Видимо, более целесообразно работать с теми дизъюнктами, которые лучше "зацеплены" с другими дизъюнктами.
|
|