авторефераты диссертаций БЕСПЛАТНАЯ БИБЛИОТЕКА РОССИИ

КОНФЕРЕНЦИИ, КНИГИ, ПОСОБИЯ, НАУЧНЫЕ ИЗДАНИЯ

<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ


Pages:     | 1 || 3 |

«Томский политехнический университет На правах рукописи НОВОСЕЛЬЦЕВ Виталий Борисович ФОРМАЛЬНАЯ ТЕОРИЯ СТРУКТУРНЫХ ...»

-- [ Страница 2 ] --

Доказательство.

Утверждение теоремы означает следующее: если ПВ F:AX выведено с помощью правил SR на основании информации об исходной схеме S модели M, то, независимо от интерпретации I, для любых двух кортежей типа S|I, таких что |I имеет для них смысл, компоненты, соответствующие атрибутам A и X в этих кортежах, совпадают и связаны соотношением, задаваемым |I. – Рассмотрим поочередно схему и все правила и покажем, что они позволяют выводить из ПВ, удовлетворяющих исходной схеме, только те ПВ, которые также ей удовлетворяют.

(0) Очевидно. Независимо от интерпретации I, в S|I не может быть двух кортежей таких, что в них присутствуют одни и те же компоненты A|I, и кортежи одновременно совпадают и не совпадают по этим компонентам.

ПВ (1) F:AX,Y – антецедент правила – удовлетворяет схеме S. Это означает, что любые два кортежа, для которых |I имеет смысл, совпадающие по A|I, совпадают также по всему набору X|I,Y|I.

Следовательно, эти кортежи совпадают и по набору X|I. Поскольку весь набор X|I,Y|I является результатом применения отображения F|I к A|I, то X|I получается применением того же F|I к A|I с последующей проекцией на атрибуты X.

(2) (правило суперпозиции). Пусть опять посылками правила являются ПВ, удовлетворяющие схеме S. Рассмотрим два кортежа s и t, для которых реализации посылок имеют смысл, причём s и t совпадают по компонентам A|I. Предположим, что правило (2) некорректно, это означает, что s и t не совпадают по какой-либо компоненте из набора X|I, Z|I, x|I. Несовпадение по фрагменту из X|I, Z|I противоречит тому, что F:AX,Z удовлетворяет схеме S, т. е. s и t совпадают, в частности, по Z|I, которые вычисляются применением F|I к A|I (с выполнением условия достижимости P|I). Последнее означает, что s и t должны совпадать и по x|I, поскольку f:Zx удовлетворяет схеме S. Отметим, что в качестве второй посылки правила суперпозиции всегда берётся ФС из (развёртки) исходной схемы, именно поэтому p – это условие допустимости x. Условие, при котором f|I обеспечивает возможность вычисления x|I по Z|I не может быть более слабым, чем условие, при котором вычислены Z|I, и условие, при котором в S|I допускается присутствие x|I – оно определяется конъюнкцией P&p. Набор X|I, Z|I, x|I вычисляется последовательным применением F|I к A|I и затем f|I к соответствующим результатам предыдущего отображения, т.е.

суперпозицией отображений. – Этим показано, что правило (2) исчисления SR корректно.

(3) (правило ветвления). Предположим, что ПВ из заключения правила не удовлетворяет исходной схеме, если посылками являются ПВ, удовлетворяющие этой схеме. Введём обозначения для ПВ, из формулировки правила:

1 F1:AX,x/Q&p, F2:AX,x/Q&-p и if p then F1 else F2 fi:AX,x/Q Пусть задана интерпретация I. Рассмотрим два кортежа s и t таких, что для них (обоих – одновременно) имеет смысл либо 1|I, либо 2|I.

Очевидно, что в каждом из этих случаев для s и t имеет смысл и |I.

Пусть s и t совпадают по компонентам A|I и пусть для них имеет смысл 1|I. Если наше предположение о том, что ПВ из заключения правила не удовлетворяет схеме, является верным, то s и t должны не совпадать по какой-либо компоненте из X|I, x|I, а это противоречит первой посылке правила. В рассматриваемом случае программный терм из заключения правила вырождается до F1, кортежи s и t, совпадая по A|I, совпадают и по компонентам X|I, x|I, а соотношение между A|I, и X|I, x|I определяется реализацией терма if p then F1 else F2 fi при выполнении p. Второй случай (для s и t имеет смысл 1|I) рассматривается аналогично. – Корректность правила ветвления исчисления SR показана.

(4) Наконец, исследуем вопрос корректности правила введения рекурсии.

Будем обозначать:

1 F1:AX,x/Q&p;

2 F2:AX,x/Q&-p;

1 g1:n1 ( A)n1 ( X );

…;

s gs:ns ( A)ns ( X ) k k k k 1 1 s s h=if p then F 1 else F 2[h/ g 1]...[h/ gs] fi:A X / Q Отметим, что, хотя в правиле (4) это явно и не указано, в антецеденте предполагается достижимость nkii(A) по A и X по nkii(X), (i=1,...,s), и эти ПВ удовлетворяют исходной схеме S наряду с прочими посылками правила. Как и прежде предположим, что заключение правила – – не удовлетворяет схеме S. Рассмотрим два кортежа s и t из типа S|I, которые совпадают по компонентам A|I. В силу предположения, s и t должны различаться хотя бы по одной компоненте множества X|I. Пусть для s и t одновременно имеет смысл 1|I (удовлетворено условие p), тогда для s и t имеет смысл и 1|I. – Сделанное предположение входит в противоречие с первой посылкой правила, а программный терм в заключении правила вырождается в F1.

Пусть теперь для s и t одновременно имеют смысл (i=1,...,s) и 2|I.

i Вообще говоря, кортежи (размеченного) типа S|I могут иметь вид (см.

рис. 3.1):

true: … A, …, X, … p: … – нерекурсивная ветвь -p: … – рекурсивная ветвь -p.n i(p): … n i(A), …, nkii(X), …, ki ki здесь подразумевается, что все значимые элементы являются проинтерпретированными.

Мы находимся в рекурсивной ветви (-p), когда кортежи s и t включают фрагмент, помеченный селектором -p.nkii(p) и совпадают по A|I, следовательно, они совпадают по nkii(A) (по правилу суперпозиции и в силу наличия в антецеденте неявных ПВ «перевычисления аргументов»), совпадают по nkii(X) (по правилу суперпозиции и в силу i) и, наконец, кортежи обязаны совпадать по X (по правилу суперпозиции и в силу наличия неявных ПВ «перевычисления результатов» вида G:…nkii(X)X/Q&-p). Таким образом, мы пришли к противоречию с высказанным предположением, и правило (4) исчисления SR также является корректным.

Перейдём теперь к вопросу исследования полноты правил исчисления SR. Для этого нам надо показать, что если некоторое ПВ не может быть выведено из информации о схеме S по правилам SR, то это ПВ не удовлетворяет схеме S. Введём понятие замыкания набора атрибутов относительно схемы S, которое понадобится нам при доказательстве теоремы о полноте исчисления.

Определение 3.4. Пусть S(r) = r.(A,X, … | filter) и пусть A – некоторый набор атрибутов схемы S. Замыканием A+ для A относительно S будем называть объединение всех таких атрибутов X, что ПВ F:AX может быть получено с использованием правил SR из информации о схеме S.

Важное свойство замыкания A+ определяется следующей леммой:

Лемма*. ПВ F:AX выводимо по правилам SR, если и только если X A+.

Доказательство: Пусть X = x1,…,xn и пусть X A+. Из определения A+ следует, что для каждого i, i=1,...,n по правилам SR выводимо ПВ Fi:A…,xi,…, из которого по правилу сужения (0) может быть получено ПВ Fi:Axi. Используя схему аксиом N:AA и правило суперпозиции, получаем Fi:AA,xi. Повторяя эти рассуждения для каждого i, в конце концов, выводим ПВ F:AX. Обратное очевидно следует из определения A+.

Сформулируем и докажем теперь теорему о полноте приведённого исчисления.

Теорема 3.2. Исчисление SR является полным относительно понятия ПВ, удовлетворяющего схеме.

Доказательство. Пусть S – исходная схема и пусть ПВ F:AX не может быть выведено на основании информации о схеме S с помощью правил SR.

Для доказательства теоремы мы должны построить интерпретацию I такую, что в S|I имеются кортежи s и t, для которых |I имеет смысл и которые, совпадая по компонентам A|I, различаются хотя бы по одной компоненте из X|I. Рассмотрим интерпретацию I, такую, что в S|I содержаться два кортежа s и t, компоненты которых совпадают для атрибутов из A+ и различаются для всех прочих атрибутов схемы S. Предположим противное, что ПВ 1 F1:BY является выводимым, но не удовлетворяет S, и определяется это на зафиксированных кортежах. Из предположения следует, что 1 имеет смысл для s и t и что B A+ (в противном случае кортежи не совпали бы по некоторому атрибуту из B). Кроме того, s и t должны различаться по компонентам из Y, т. е. Y A+ (но, вообще говоря, неверно, что YA+=).

Пусть у-атрибут, yY \ A+. Поскольку B A+, то ПВ G:AB выводимо по лемме*. Отсюда, с учётом 1 по правилу суперпозиции имеем G;

F1:AY, значит Y A+, а сделанное предположение неверно. Итак, ПВ, выведенные с помощью правил SR, удовлетворяют исходной схеме.

Покажем теперь, что не удовлетворяет S, в частности, при интерпретации I. Предположим обратное. Поскольку A A+, заключаем, что должно выполняться X A+, так как иначе s и t, совпадая по компонентам A|I, не совпадали бы по компонентам X|I. Отсюда опять по лемме* заключаем, что ПВ F:AX может быть выведено по правилам SR. Это противоречит сделанному предположению, а значит, не удовлетворяет схеме S, в частности, на кортежах s и t рассматриваемой интерпретации I. – Таким образом мы показали полноту правил SR.

3.2. Стратегия и алгоритм вывода в классе РДС Известны эффективные стратегии поиска доказательства теоремы (3.1) в классе линейных программ (когда используются только правила (1) и (2) исчисления SR) и в классе ветвящихся программ (с добавлением к двум первым правилам исчисления правила ветвления). При использовании правила введения рекурсии основная трудность связана с определением множеств A и X – аргументов и результатов ПВ из заключения правила (в синтезированной программе применению этого ПВ будет соответствовать вызов построенной рекурсивной процедуры). Определение множеств A и X может сопровождаться достаточно большими временными затратами – в остальном, применение правила введения рекурсии не ухудшает общей оценки сложности предлагаемых алгоритма и стратегии. Дело в том, что вывод для подзадачи, сформулированной во второй строке правила (4), проводится теми же средствами, что и основной вывод теоремы существования, и полностью включается в последний.

3.2.1. Описание алгоритма Предлагаемый алгоритм использует некоторую ограниченную стратегию поиска решения задачи T=(A0,X0,S), что позволяет ему работать с полиномиальными затратами ресурсов по отношению к длине описания РДС модели M [Новосельцев 1981].

Входной информацией для алгоритма является описание модели M и формулировка задачи T. Доказательство теоремы существования решения (3.1) заключается в последовательном применении правил SR к аксиомам и ранее полученным утверждениям. Аксиомами являются ФС из описания схемы модели M. Поиск доказательства ведётся от данных к целям методом, обратным по отношению к стандартным целеориентированным («прямая волна» – [Новосельцев 1985а]), при этом всё время преследуется цель расширить множество достижимых из данных атрибутов и ослабить условия, при которых показана достижимость 1.

В процессе построения доказательства (планирования) всегда фиксируется текущая схема. Это означает, что предметные аксиомы выбираются из числа явно присутствующих в наборе filter данной схемы.

Сначала текущей объявляется схема, на которой поставлена задача T. Когда дальнейший вывод на текущей схеме становится невозможным, текущей становиться какая-либо её подсхема, для которой определён вход (осуществляется «спуск в подсхему»). Последнее означает, что показана достижимость некоторых атрибутов, определённых в подсхеме, причём условия их достижимости совпадают с теми, при которых эти атрибуты имеют смысл в описании. Если текущая схема не имеет необработанных Термин «прямая волна» не должен вводить в заблуждение. Предлагаемая здесь и в последующих разделах методология остается «обратной» по отношению к целеориентированному подходу (см. п.1.2), а «прямая волна» – есть не более, чем термин, используемый при характеристике стратегий в области вычислительных моделей.

подсхем, то после окончания работы с ней текущей становиться схема, для которой данная является подсхемой («подъём из подсхемы»). Если осуществлён подъём из подсхемы, повторных спусков в неё не производится, а во множество достижимых атрибутов включается только те условия, которые совпадают с условием общей части подсхемы. Этим достигается то, что, производя поиск доказательства на текущей схеме, мы анализируем только её собственные условия. Попытка применения правила рекурсии предпринимается для рекурсивной схемы непосредственно перед подъёмом из последней.

Предлагаемый алгоритм по сути своей является алгоритмом построения замыкания A0+ для заданного в T набора атрибутов A0. Тотальная информация о планировании на текущей схеме запоминается в форме нового ПВ (актуального только в процессе решения конкретной задачи T), таким образом, планирование на подсхемах с совпадающими именами из D проводиться с учётом полученной ранее информации («бесповторность»). В случае успешного завершения доказательства из последнего удаляются ненужные данные (использование предметных аксиом, которые не являются существенными для решения задачи T), после чего извлекается схема программы. Подробнее эти вопросы, а также определение класса, которому принадлежат синтезированные программы, обсуждаются в следующих разделах.

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

Ck – множество у-атрибутов исходной схемы, достижимость которых установлена в текущий момент;

по-аксиома – проблемно-ориентированная или предметная аксиома – ФС из (развёртки) исходной схемы;

вход в подсхему – наличие в Ck у-атрибутов, которые принадлежат подсхеме текущей схемы;

A0 и S берутся из формулировки задачи T.

Описание алгоритма:

«установить i=0, С0=A0»;

«поднять флаг “продолжать доказательство”»;

«текущей схемой объявить S»;

while «поднят флаг “продолжать доказательство”» do if «имеется по-аксиома текущей схемы, аргументы которой входят в Ci» then «применить правило композиции, и, если возможно, правило ветвления»;

«Ci+1: к Ci добавить новые у-атрибуты либо изменить условия достижимости»;

«установить i=i+1»;

«если определился вход в подсхему, запомнить её»

else if «имеется подсхема, в которую определён вход» then «объявить её текущей схемой»

else if «текущая – рекурсивная схема» then «применить правило введения рекурсии;

установить i=i+1»;

«определить Ci+1»

else «объявить текущей внешнюю схему»

fi fi fi;

if «текущая – исходная и нет по-аксиом, аргументы которых входят в Ci» then «опустить флаг “продолжать доказательство”» fi od.

Использование специальных структур данных, различные тактики выбора очередной по-аксиомы для использования её в доказательстве позволяют получать весьма эффективные реализации приведённого алгоритма. Подробнее этот вопрос рассматривается ниже.

3.2.2. Корректность алгоритма построения вывода Здесь нас интересует проблема корректности алгоритма. Покажем, что каждый у-атрибут, попавший в некоторое Ci, содержится в A0+ и обратно – каждый элемент A0+ попадает в некоторое Ci.

Теорема 3.3. Приведённый здесь алгоритм корректно вычисляет A0+.

Доказательство.

(i) Индукцией по i покажем, что если некоторый у-атрибут e помещается в Ci, то eA0+.

База индукции (i=0). eA0+, и по схеме аксиом (0) и правилу (1) получаем A0e.

Индукция. Пусть i0 и Ci состоит из атрибутов, которые принадлежат A0+.

Пусть также на i+1-ом шаге используется ПВ F:BY и eY. BA0+, поскольку BCi, следовательно, по лемме* имеется G:A0B. Используя правила композиции и сужения, получаем G;

F:A0e, т. е. e A0+.

(ii) Покажем теперь, что если у-атрибут e входит в A0+, то e попадает в некоторое Ci. Точнее, докажем более общее утверждение: если на основании информации о схеме S по правилам SR выведено ПВ G:A0B, то множество у-атрибутов B содержится в некотором Ci.

Вывод ПВ представляет собой последовательность применений правил SR к по-аксиомам и ранее полученным предложениям вычислимости (начальное ПВ N:A0A0 получается в результате использования схемы аксиом). Доказательство проводим индукцией по длине вывода.

База индукции (минимальная длинна вывода).

Вывод заканчивается применением схемы аксиом – A0 состоит в точности из B, очевидно, BC0. Длинна вывода – два – схема аксиом (0) и правило сужения (1). – Здесь, очевидно, также BC0.

Индукция. Предположим, сделанное утверждение истинно для выводов, длина которых не превосходит k, и пусть вывод ПВ F:AB имеет длину k+1. Если получается по правилу сужения, то B принадлежит Ck, которое найдётся по предположению для вывода, предшествующего получению. Пусть B получено применением правила суперпозиции, например, из полученных ранее 1 F1:AZ и 2 f:Zb (B=Zb).

Вывод каждого из двух последних ПВ имеет длину меньше k+1.

Следовательно по предположению, найдётся такое Ci (ik+1), что ZCi. По способу введения правила композиции 2 является по-аксиомой – функциональной связью из набора filter исходной схемы S. Отсюда заключаем, что b (а, следовательно, и B=Zb) попадает в Ci+j, где j – число применений правил SR между получением в выводе ПВ 1 до использования по-аксиомы 2 (включительно).

(iii) Правила ветвления и введения рекурсии в контексте доказываемой теоремы можно не различать – здесь нам не важен способ подтверждения предположения, появляющегося в последнем правиле, достаточно просто знать, что мы это делать умеем.

Итак, пусть ПВ F:AB получено по правилу ветвления, и длина вывода равна k+1. Пусть также получено из 1 F1:ABB1,b/Q&p и 2 F2:AB1,b/Q&-p. Длина вывода как 1, так и 2 меньше k+1, B следовательно найдутся Ci и Cj, которые содержат BB1,b/Q&p и B1,b/Q&-p, B соответственно, причём при построении Ci и Cj обсуждаемый алгоритм работает от одних и тех же исходных данных A0. Отсюда видно, что атрибуты множества B и, в частности, b/Q будет включён в Cmax(i,j)+1, в силу того, что правило ветвления применяется сразу же, если показана достижимость атрибута при альтернативных условиях.

Поскольку по лемме* принадлежность атрибута e замыканию A0+ означает выводимость ПВ F:A0e, можно заключить, что обсуждаемый алгоритм корректно строит A0+.

3.2.3. Особенности введения рекурсии Представим некоторые соображения по определению множеств A и X.

Предположим, что в процессе планирования мы подошли к рассмотрению рекурсивной детерминированной схемы S()=.(A,…if p…;

S(),… fi | filter).

Не умаляя общности, предположим для простоты, что все подсхемы за исключением S являются элементарными. По сделанному предположению схема S стала текущей с «входом», определяемым множеством A (множеством у-атрибутов схемы S, для которых показана достижимость).

Опишем на содержательном уровне процесс, который позволяет определить множества аргументов и результатов рекурсивного ПВ из заключения правила введения рекурсии. Сначала, не применяя правила (4) исчисления SR для схемы S, выводим из атрибутов A всё, что возможно. Во множество аргументов Arg включаем все входные атрибуты A. Для этих атрибутов показана достижимость при условии, которое приписано постоянной части схемы S (условие «входа» в S). После этого определяем замыкание A+ и объявляем его окончательным множеством аргументов Arg.

Во множество результатов Res помешаем у-атрибуты из постоянной части схемы S не попадающие в Arg, для которых показана достижимость от Arg при условии нерекурсивной ветви, и такие, что вовлечены в левые части ФС вида.f:…,..b,….с – «выводящие» из рекурсивного вхождения схемы.S(). Наконец, транзитивное замыкание полученного множества Res+ атрибутов объявляем окончательным множеством результатов рекурсивного ПВ.

Замечание. Если любое из транзитивных замыканий окажется пустым, применение правила введения рекурсии оказывается невозможным.

Замечание. Если транзитивное замыкание строить «в лоб», затраты времени могут стать экспоненциальными по числу атрибутов. Этих затрат можно избежать, анализируя циклы в графе, который соответствует рекурсивной схеме. При этом атрибуты вида a и r.a отождествляются.

Рассмотрим подробнее соображение из последнего замечания.

Предположим, в качестве входных атрибутов схемы S выступают a1 и a (множество A) и в наборе filter содержаться ФС (запишем их сокращённо):

a1r.a2, a2r.a1, a3r.a4, a4r.a5, a5r.a3, a1, a3r.a4.

уровни шаги атрибуты получен из i+0 k+1 a1 задан 2 a3 задан 1 3 a2 4 a4 5 a6 1, 2 6 a1 7 a5 3 8 a3 Рис. 3.2. Фрагмент информационной структуры Проанализируем фрагмент информационной структуры, используемой при планировании, в которую в процессе доказательства заносятся сведения о достижимых атрибутах (табл. 1). На шестом шаге устанавливается достижимость a1A – выявляется цикл длины 2: a1a2a1. Аналогично, на восьмом шаге обнаруживается цикл длины 3: a3a4a5a3 для a3A. Можно сделать вывод, что a1 и a3 одновременно перевычисляются в результате трехкратного выполнения первого и двукратного выполнения второго циклов.

Эти неформальные соображения, обобщенные для случая произвольной рекурсивной схемы, позволяют строить транзитивное замыкание с затратами, пропорциональными O(L), где L – число атрибутов, явно упомянутых в описании схемы.

Многие технические трудности, возникающие при решении проблемы синтеза в классе РДС-моделей, удаётся преодолеть за счёт правильного подбора информационных структур применяемых алгоритмов и знания природы РДС-моделей.

3.3. Проблемы реализации систем построения вывода Предлагаемая здесь методология неоднократно использовалась при реализации как промышленных систем [Новосельцев 1985в], так и исследовательских проектов, выполняемых под руководством автора [Новосельцев, Калайда и Шагисултанов 1991], [Новосельцев и Ларионов 2002], [Новосельцев и Малахов 2004]. Элементы обсуждаемого подхода в различных вариантах включались во внешние проекты.

Как показывает практика, теория РДС-моделей вкупе с исчислением SR допускают весьма эффективные реализации разнообразных когнитивных систем. В силу того, что задача установления выводимости тесно связана с нахождением транзитивных замыканий специальных отношений, естественные варианты реализации опираются на прекрасно зарекомендовавшие себя и весьма эффективные подходы. Прежде всего, среди последних имеет смысл выделить алгоритм Армстронга [Ульман 1983] и алгоритм упоминавшегося ранее Диковского [Диковский 1983б]. – В разных модификациях эти алгоритмы обладают полиномиальными оценками с невысокими степенями (линейные либо квадратичные), хотя и связаны с существенно более бедными по сравнению с описываемыми здесь моделями.

В первом случае речь идет о связях на атрибутах реляционных схем в базах данных, а во втором рассматриваются линейные вычислительные модели.

Оценки, связанные с алгоритмическими характеристиками исчисления SR, приводились в предыдущих разделах. Здесь мы попытаемся получить сложностные оценки базовой версии алгоритма, приведенной в п.3.2.1.

Ясно, что стратегия работы алгоритма не является в чистом виде стратегией «прямой волны» (п.3.1.3). – Это своеобразная стратегия «вширь вглубь» с ограниченным бектрекингом, т.е. получение «всего возможного» в текущем отношении, затем «спуск» во внутреннюю схему, «прямая волна» в ней (с возможными, в свою очередь, «спусками»), наконец «подъём» и продолжение работы в текущем отношении.

Для любого элемента из доказательства, имеющего смысл в описании (развертки) отношения при некотором условии P, конъюнкция условий при аргументах доставляющего его ПВ и условия самого предложения вычислимости (S) совпадает с P либо удовлетворяет требованию S P (п.2.3).

Учитывая сказанное, а также помня дисциплину определения схем С-модели и стратегию, реализуемую описанным в п.3.2.1 алгоритмом, можно сделать вывод, что программа, извлекаемая из доказательства, имеет строго вложенную структуру операторов разветвления. Такие программы образуют класс хорошо структурированных программ, определенный классиками «структурного подхода» [Дейкстра, Дал и Хоор 1975]. Одним из положительных моментов, связанным с произведенной фиксацией класса, является то, что синтезированные структуры достаточно легко анализировать и, следовательно, модифицировать «вручную», а это также является востребованным при практических реализациях.

Спецификация задачи T=(A0,X0,S) в контексте реализации описывается структурой (множеством) вида, естественно связанной с разверткой:

N0 k Nj N S`(r)=r.(( S`0i (a0i) ) ( (p j ( S`jm(a jm) ) ) ) f s), (3.3) i j m s где смысл и значения используемых символов совпадают с таковыми в определении (2.2).

Особенности алгоритма планирования таковы, что основные временные затраты производятся на этапе применения ПВ, т.е. главную роль в оценке играет последнее слагаемое выражения (3.3). Предложение вычислимости может применяться либо для получения новых достижимых элементов, либо для модификации условий уже имеющихся в доказательстве элементов – в последнем случае необходимо повторное применение ранее использованных ПВ с тем, чтобы «пронести» по фрагменту дерева вывода вновь полученные условия. Фрагмент доказательства, на котором производится модификация условий полученных элементов, ограничен общей частью текущего подотношения из структуры (3.3). Таким образом сложность поиска на полной развёртке является линейной комбинацией затрат на подотношениях развёртки (это наихудшая оценка – без учета выигрыша от «бесповторности»).

Итак, рассматриваемое отношение содержит N собственных ПВ, вариантная часть отношения состоит из k альтернативных ветвей. В этих предположениях затраты на планирование выражаются соотношением T` = L0 + (L1 + … + Lk) + L k, где (3.4) L0 – длина (количество использованных ПВ) участка доказательства с однократным применением ПВ, Li (i = 1,…,k) – длина участка, соответствующего i-той ветви вариантной части, L – длина участка с повторным применением ПВ, причём L0 + (L1 +…+ Lk) + L = N.

Критическая ситуация возникает при максимальной длине L, когда L0 = 0, а длина вариантной ветви – два ПВ, в этом случае (3.4) принимает вид T` = 2 k + k (N - 2 k) (3.5) Очевидно, что выражение (3.5) достигает максимума при k(N) = (N+2)/4, в этом случае оценка T`, как функции от N, принимает вид T`( N) = О(N 2) (3.6) В реальных задачах k не является функцией от N, а мажорируется некоторой константой. Отсюда можно заключить, что, практически, алгоритм имеет линейную по длине (3.3) сложность. Затраты памяти оцениваются аналогичным образом и, следовательно, также являются линейными по длине (3.3).

Учитывая результаты п.3.2.3, можно заключить, что полный алгоритм п.3.2.1 (с использованием правила введения рекурсии) максимальной теоретической оценкой имеет О(N3), а реально является не более, чем квадратичным по длине исходного описания модели.

3.4. Выводы Представленные в главе исчисление SR и подход к установлению выводимости формул в этом исчислении являются весьма привлекательными для реализации широкого круга прикладных когнитивных систем, учитывая показанные свойства полноты и эффективной разрешимости теории.

Следует также подчеркнуть, что описанная теория РДС-моделей может служить естественным формальным базисом популярного объектно ориентированного подхода. – Свойства иерархичности, инкапсуляции и наследования естественным образом присущи представленной теории. Более того, малозначимое в рамках представленного исследования замечание о динамичности множества первичных типов (п.2.1) в контексте ООП является довольно существенным – оно позволяет выстраивать иерархию в двух направлениях (обеспечивая, по мере необходимости, как агрегацию, так и детализацию понятий).

Интересным в рассмотренной теории является и то, что в настоящее время на ее основе ведется чрезвычайно успешное аспирантское исследование, связанное с построением альтернативного теории Кодда формализма для организации рекурсивных баз данных.

Наконец, опираясь на механизм «схем» теории РДС-моделей, можно ввести понятие «реализуемых предикатов» и на этой основе строить когнитивные системы с использованием исчислений высших порядков.

Глава 4. Модальная логика и обратный метод 4.опр- 4.теор- Необходимость исследований в области автоматического доказательства теорем определяется постоянно растущим спросом на интеллектуальные системы программирования и невозможностью (или малой эффективностью) использования существующих информационных технологий для слабо формализованных предметных областей, а также предметных областей с модальными связями. Популярные нечеткие логики далеко не всегда уместны и адекватны, а работа с модальностями в рамках традиционных подходов, как правило, реализуется введением эклектичных механизмов, снижающих степень уверенности в корректности реализованного на таком базисе программного обеспечения. Модальные же теории естественным образом включают понятия необходимости, возможности, персонифицированности и т.д.

Традиционным инструментом поиска вывода является метод резолюций, применяемый в классическом Прологе [Робинсон 1970], а также в таких системах для модальных логик как *SAT [Giuchinglia and Sebastiani 1996б] и DLP [Horrocks and Patel-Schneider 1998]. Не менее мощным, но существенно реже используемым, является обратный метод [Маслов 1964].

Наиболее эффективная программа автоматического установления выводимости для модальных систем, основанная на обратном методе, реализована лишь недавно [Voronkov 1999]. Успешность применения обратного метода, в значительной степени, обусловлена его настройкой на анализируемую формулу и возможностью применения эффективных критериев борьбы с избыточностью пространства вывода, что способствует сокращению ресурсных характеристик поиска (об обратном методе см.

великолепную работу [Маслов и Минц 1983]). Следует отметить, что обратный метод ориентирован на формирование пространства вывода (а не только самого вывода) в виде леса. – Очевидно, что навигация по частично упорядоченным структурам, как минимум, не менее эффективна, чем управление в однородном множестве с эквивалентной суммарной мощностью.

В качестве базового исчисления в работе рассматривается модальная логика знания KT (хотя все полученные результаты достаточно легко распространяются, в частности, на автоэпистемическую логику KT45 – см.

[Новосельцев и Ларионов 2002]). Логика KT является более богатой системой по сравнению с минимальной модальной логикой К (за счет добавления аксиомы Т: АА) и интересна тем, что аксиома Т отвечает свойству рефлексивности бинарного отношения R структуры модальной логики [Фейс 1974]. Логика знания имеет большое значение при реализации информационных систем, когда модальный оператор принимает трактовку «известно», а схема Т как раз и требует, чтобы то, что известно, являлось истинным.

Модальные теории с эффективными стратегиями планирования могут быть успешно использованы в автоматизации проектирования (когда не известны строгие формализмы анализируемой предметной области), в экспертных и других когнитивных системах. Концепции ряда наиболее перспективных современных систем автоматизированного проектирования (САПР) предусматривают совместное использование традиционных технологий и модальных компонентов ([Тарасов 1993], [Yoshikawa 1989], [Treur 1991], [Кашуба 1998], [Смирнов и Юсупов 1992]). Специфика баз проектных знаний состоит в том, что они включают знания о предметной области и знания о решениях ранее встреченных проблем. Иногда на содержательном уровне выделяют два альтернативных типа проектных знаний (по признакам их значимости): глубинные, основанные на некоторой фундаментальной теории (например, законах механики Ньютона) и поверхностные (эвристические), которые базируются на интерпретации отдельных фрагментов индивидуального опыта конструкторов. Для любой из соответствующих предметных областей такая категоризация может быть преобразована (простым переименованием) в категоризацию «известно/возможно», которая как раз и характерна для системы КТ. – Подчеркнем, что степень субъективности разделения проектных знаний не является предметом данного исследования.

Практический интерес к модальным теориям и методам установления выводимости, отличным от метода резолюций, подчеркивается обширной библиографией – здесь упоминается только незначительная часть публикаций.

План установления выводимости формулы в Kх (здесь – КТ и КТ45) описывается некоторой разрешающей процедурой, реализации которой осуществляется в четыре этапа (см. [Новосельцев и Бурлуцкий 2001] и [Новосельцев и Ларионов 2002]):

I. Построение базовых исчислений для Kх – прямого секвенциального исчисления Kхseq и настроенного на анализируемую формулу Ф обратного исчисления KхФinv (в последнем случае формулами KхФinv являются все подформулы исходной Ф).

II. Введение исчислений путей KхФpath и KхФIP, кодирующих вывод (связывающих подформулу с примененным к ней в процессе вывода правилом) в базовых исчислениях Kхseq и KхФinv, соответственно.

III. Замена вывода исходной Ф формулы в Kх на опровержение отрицания Ф в KхФIP (из соображений технического удобства) с применением стратегий сокращения пространства вывода.

IV. Отображение полученного в KхФIP вывода в исходную систему.

4.1. Базовые понятия и соглашения Термины и определения большей частью заимствованы из классических работ по математической логике, таких как [Фейс 1974], [Мендельсон 1976] и [Барвайс 1983]. – Здесь же приводятся употребляемые ниже базовые термины и соглашения в целях устранения возможных разногласий.

Логика высказываний рассматривает предложения (декларативные фразы), о которых можно точно сказать, что они либо истинны, либо ложны.

Высказывания составляют элементарные фразы языка логики высказываний.

Их также принято называть атомарными формулами или атомами. Литералом называют либо атом, либо его отрицание. Пропозициональные переменные в работе обозначаются малыми латинскими буквами, а формулы – прописными.

Для описания множеств или мультимножеств формул используются прописные греческие буквы.

Формула логики высказываний называется общезначимой, если она истинна, независимо от значений истинности составляющих ее пропозициональных переменных. Формула называется выполнимой, если у нее существует хотя бы одна модель. Формула, которая не является выполнимой, называется невыполнимой или противоречивой. Формула, не являющаяся ни общезначимой, ни противоречивой, называется нейтральной.

Таким образом, все множество формул логики высказываний распадается на три подмножества, содержащие соответственно общезначимые, невыполнимые и нейтральные формулы. Общезначимые формулы также принято называть тавтологиями. Если рассматривается формула А, то тот факт, что она является тавтологией, записывать следующим образом:

А Пусть Г – множество формул, тогда запись Г А обозначает, что все интерпретации, в которых истинны все формулы из Г, обращают в истинную и формулу А. В этом случае А называется логическим следствием Г.

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

предложений, рассматриваемых как общезначимые, и множества правил вывода, т.е. функций на формулах, которые позволяют конструктивно строить (выводить) новые общезначимые предложения из аксиом и уже полученных общезначимых предложений. – В такой трактовке общезначимые предложения, построенные указанным образом, называются теоремами.

Доказательством теоремы называют упорядоченный список аксиом, применений правил вывода и уже известных теорем, позволяющих получить (вывести) данную теорему.

Предположим, что задана некоторая дедуктивная система. Тот факт, что формула А доказуема (выводима) в этой системе записывается следующим образом:

А Это обозначение можно считать сокращением для А или иначе, А является аксиомой данной системы.

Если же в данной системе задано множество формул Г, то запись Г А означает, что А доказуема с использованием формул из Г (выводима из Г);

при этом элементы из множества Г рассматриваются как дополнительные аксиомы. В такой трактовке элементы из Г называются гипотезами.

Множество Г называют синтаксически невыполнимым, если Г Л.

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

Некоторое выражение независимо от дедуктивной системы, если его нельзя вывести с помощью этой системы. Система называется минимальной, если каждая аксиома независима от остальной системы. Система адекватна (корректна, справедлива), если все теоремы являются общезначимыми формулами, т.е. если для произвольной формулы А А влечет А Система полна, если любая общезначимая формула является теоремой, т.е. система полна, если для произвольной формулы А А влечет А.

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

называются соответственно модальным оператором общности и модальным оператором существования.

4.1.1. Синтаксис и семантика логики КТ Далее в этой главе мы будем говорить о модальной логике знания KT.

Модальные операторы воздействуют на формулы логики высказываний, изменяя их смысл следующим образом. Пусть А – произвольная формула, тогда А трактуется в рамках языка логики КТ как «известно, что А», а А трактуется как «противоположное к А неизвестно». Формула логики КТ определяется подобно формуле логики высказываний индуктивно, но с добавление модальных операторов общности и существования:

Определение 4.1. В логике КТ всякое высказывание является формулой;

если А и В являются формулами, то ~А, (AB), (AB), (AB), (AB), А и А также являются формулами;

других формул в логике КТ нет.

На модальные операторы и накладывается соотношение двойственности:

А ~ ~ A.

Это соотношение позволяет определять оператор через оператор, другими словами модальные формулы можно записывать, используя один лишь модальный оператор общности.

Семантический анализ формул системы КТ зависит от параметров, неявно вносимых модальными операторами. Формулу А обычно трактуют как t A(t). Семантический анализ этой формулы должен осуществляться с учетом неявно подразумеваемого параметра t в модальном операторе общности. Для этого в [Крипке 1971] вводится метод специфического семантического анализа: семантика возможных миров. В ней модальная формула оценивается в рамках некоего «универсума» различных «возможных миров», т.е. анализ истинности некой модальной формулы зависит от рассматриваемого возможного мира. Кратко приведем эту семантику.

Под универсумом W понимают множество миров, связанных отношением доступности R. Пусть a и b – два мира из универсума W, тогда факт доступности мира b из мира a обозначается aRb. Пару (W, R) при этом называют структурой.

Здесь и далее L обозначает множество атомов модального языка КТ.

Оценка V – это отображение из WL в {И, Л}, которое для каждого мира w из универсума W сопоставляет каждой пропозициональной константе из L определенное значение истинности. Тройка (W, R, V) называется моделью Крипке или просто моделью. Запись (W, R, V) w А означает, что А истинно в мире w для модели (W, R, V).

Для семантической оценки формул из L выделяют конкретный мир w из универсума W вместе с рассматриваемой оценкой V и вводят понятие семантического следования между моделями и формулами языка.

Определение 4.2. Отношение семантического следования определяется индуктивно:

Базис:

1. (W, R, V) w И 2. (W, R, V) w Л Индукционный шаг:

1. (W, R, V) w А, если V(w, A) = И и А – константа из L.

2. (W, R, V) w АВ, если (W, R, V) w А только когда (W, R, V) w В.

3. (W, R, V) w А, если для любого x W при wRx имеем (W, R, V) х А.

Из соотношения двойственности и пункта 3 индукционного шага определения семантического следования непосредственно вытекает правило:

(W, R, V) w А, если существует x W такой, что wRx и (W, R, V) х А Понятие общезначимой модальной формулы вводится в три этапа.

1. Вводится понятие общезначимой формулы в модели (выполнимой формулы): формула А из L общезначима в модели (W, R, V) тогда и только тогда, когда А подтверждается во всех мирах этой модели, т.е. если V(w, A) = И для всех миров w из W. Символьная запись общезначимости в модели выглядит следующим образом: (W, R, V) А.

Вводиться понятие общезначимой формулы в структуре: формула А из L 2.

общезначима в структуре (W, R) тогда и только тогда, когда А общезначима в любой модели (W, R, V). Символьная запись общезначимости в структуре выглядит следующим образом: (W, R) А.

Вводится понятие общезначимой модальной формулы: формула А из L 3.

общезначима тогда и только тогда, когда А общезначима в любой структуре (W, R). Символьная запись общезначимости модальной формулы выглядит следующим образом: А.

Подобно классическому исчислению высказываний для модальной логики знания КТ строится дедуктивная система:

Пусть А, В, С – произвольные формулы логики КТ.

1. Схемы аксиом:

((A(BС)) ((AB) (AС))) (A(BA)) ((~A~B) ((~AB) A)) 2. схема К: 3. схема Т:

(AB) ( А B) А A Правила вывода:

1. modus ponens 2. правило вывода необходимости А (АВ) А_ В А Известна важная теорема, характеризующая связь между семантическим отношением и синтаксическим отношением для логики знания (доказательство ее приведено в [Гольдблат 1987]).

Теорема 4.1. Формула А является теоремой логики КТ тогда и только тогда, когда А истинна во всех структурах, в которых R рефлексивно.

Также широко известен тот факт (см., например, [Фиттинг 1983]), что произвольную модальную формулу можно свести к модальной формуле в отрицательной нормальной форме. В дальнейшем мы будем рассматривать только модальные формулы в отрицательной нормальной форме (исходя, исключительно, из технических соображений).

4.1.2. Мультимножества и секвенции Как и предыдущий, данный раздел в значительной степени является реферативным – здесь фиксируются и, возможно, модифицируются необходимые в дальнейшем термины и соглашения, опирающиеся, главным образом, на материалы [Минц и др. 2000].

Пусть – финитное мультимножество и A – некоторые его элемент.

Через, A или A, обозначим объединение мультимножества и элемента A. Это означает, что если мультимножество имеет k копий элемента A, то мультимножество, A имеет k+1копию элемента A.

Аналогично, объединение двух мультимножеств и обозначим через,. В этом случае, если мультимножество имеет k копий элемента A, а мультимножество имеет m копий элемента A, то, имеет k+m копий элемента A.

Будем говорить, что мультимножество является мультиподмножеством мультимножества, если для любого элемента A из, если A встречается в k раз, то тогда A должен встречаться и в по крайней мере k раз. Символьная запись отношения мультиподмножественности выглядит следующим образом:. Тот факт, что A является элементом (членом) мультимножества обозначается A.

Мультимножественной разностью двух мультимножеств и.

называют мультимножество такое, что если элемент встречается в k.

раз и в m раз и km, то он встречается в k - m раз, в противном случае.

он не встречается в никогда.

Аналогично, мультимножественной суммой двух мультимножеств и называют мультимножество + такое, что если элемент встречается в k раз и в m раз, то тогда он встречается в + k + m раз.

Традиционно в монографиях по математической логике (например, [Мендельсон 1976] или [Барвайс 1983]) под секвенцией понимают структуру вида:, где = A1,..., An, = В1,..., Вm – множества формул. Каждой секвенции стандартным образом сопоставляется формула (так называемый формульный образ секвенции): ИA1...AnВ1...ВmЛ. Эта формула ~A1...~AnВ1...ВmЛ.

эквивалентна следующей: Последнее дает основание говорить о секвенции как о множестве формул.

С другой стороны, для определения секвенции довольно часто используется подход, несколько отличающийся от классического (см., например, [Драгалин 1979], [Воронков 1996] или [Воронков 2000]). Этот подход заключается в следующем: под секвенцией понимают (как и в традиционном случае) структуру вида:, но и здесь не множества, а мультимножества формул. Таким образом, и формульный образ секвенции есть не множество, а мультимножество формул.

Такая трактовка секвенции дает хорошие результаты при доказательстве теорем полноты, и поэтому далее в работе под секвенцией мы будем понимать финитное мультимножество формул.

Секвенцию будем называть подсеквенцией секвенции, если является мультиподмножеством. Пусть дана секвенция = A1,...,An, тогда A1,..., An, аналогично, A1,...,An.

Пусть дана секвенция = A1,...,An. Секвенцию будем называть выполнимой, если существует модель Крипке для всех формул A1,...,An.

Для исчисления секвенций KTseq, которое является секвенциальным вариантом описанной выше дедуктивной системе КТ, в этой работе мы будем использовать традиционные понятия вывода и, соответственно, дерева вывода (см. [Bachmair L. Gansinger H. 2000]). Для устранения разногласий ниже приведены используемые в работе варианты этих определений.

Под выводом в исчислении секвенций KTseq будем понимать конкретную последовательность применений правила вывода. Под деревом вывода секвенции Ф будем понимать любое дерево, образованное выводами и имеющее Ф своим корнем.

Пусть предполагается, что некоторая секвенция ~Ф в KTseq является общезначимой. Тогда ее отрицание Ф должно быть противоречием. В этом случае доказательство ~Ф будет эквивалентным опровержению Ф. – Известно, что такой подход, зачастую, является технически более удобным.

4.1.3. Прямое и обратное исчисление секвенций для логики знания Пусть Ф – формула логики KT. Для анализа Ф удобнее использовать не саму систему KT, а эквивалентное ей исчисление секвенций KTseq (см.

[Wallen 1990]). Справедлива следующая теорема (полноты KTseq): Ф невыполнима в KT тогда и только тогда, когда существует опровержение Ф в KTseq. Доказательство теоремы приведено в [Fitting 1983], оттуда же заимствовано и подходящий вариант исчисления секвенций KTseq (здесь p – пропозициональная переменная):

Аксиомы: Г, p, ~p Правила вывода:

Г, A, В ();

Г, A Г,В ();

Г,A ();

Г, A ( ) Г,A, Г,AВ Г,AВ Г, A Как отмечалось ранее, поиск опровержения мы переносим в инверсное исчисление KTФinv (формулами KTФinv являются все подформулы исходной Ф, что, собственно, и определяет настройку на анализируемую формулу).

Исчисление KTФinv приводится ниже:

Аксиомы: p, ~p Правила вывода:

Г, A, A (C);

Г, A,В ();

Г, A (l);

Г, В (r);

Г,, AВ Г, A Г,AВ Г,AВ Г, A ();

Г ();

Г, A ( ).

Г,A Г,A Г, A Заметим, что в общем случае неочевидно, как в KTФinv находить опровержение произвольной секвенции, поэтому непосредственное доказательство теоремы полноты KTФinv, представляется затруднительным.

KTФinv Для доказательства полноты мы используем лемму подсеквенциальности, которая позволяет «переносить» найденное в KTseq опровержение Ф в исчисление KTФinv..

Лемма подсеквенциальности. Пусть Ф – формула KT и Г – секвенция, состоящая из подформул Ф и имеющая опровержение в KTseq, тогда существует секвенция такая, что Г и имеет опровержение в KTФinv..

Доказательство. Доказательство ведется индукцией по длине вывода Г в KTseq.

Рассмотрим правило вывода () в KTseq:

Г, А, В () Г, АВ (Г, А, В), Предположим, что существует секвенция имеющая опровержение в KTФinv. Необходимо найти секвенцию ` (Г, АВ), имеющую опровержение в KTФinv. В зависимости от того, встречаются ли А и В в, мы получаем три различных случая:

1) Пусть А, В. Мы имеем = (, А, В), где Г. Вывод для этого случая имеет вид:

, А, В (r), АВ, В (l), АВ, АВ (C), АВ 2) Пусть А. В. Мы имеем = (, А), где Г. Вывода для этого случая имеет вид:

, А, В (r), АВ 3) Пусть А. В. Тогда ` =.

Рассмотрим лишь случай с модальностью, для остальных правил вывода из исчисления KTseq – () и (), – доказательство проводится аналогично.

Итак, правило вывода ( ) в KTseq:

Г, А ( ).

Г, А (Г, А), Предположим, что существует секвенция имеющая опровержение в KTФinv. Необходимо найти секвенцию ` (Г, А), имеющую опровержение в KTФinv. В зависимости от того, встречается ли А в, мы получаем два различных случая:

1) Пусть А. Мы имеем = (, А), где Г. Вывод для этого случая имеет вид:

, А ( ).

, А 2) Пусть А. Тогда ` =.

Теперь может быть доказана KTФinv).

Теорема 4.2. (полноты Формула Ф системы KT является невыполнимой тогда и только тогда, когда она имеет опровержение в KTФinv.

Доказательство: Доказательство проведем методом от противного.

Предположим, что формула Ф является невыполнимой, тогда из теоремы полноты для KTseq (прекрасное доказательство приведено в [Fitting 1983]) формула Ф имеет опровержение в KTseq. Согласно лемме подсеквенциальности, существует некая подсеквенция секвенции Г, имеющая опровержение в KTФinv. Секвенция Г имеет только две подсеквенции – саму Г и пустую секвенцию, но последняя, очевидно не имеет опровержения, следовательно Ф имеет опровержение в KTФinv.

4.2. Исчисление путей для логики КТ Построим такое исчисление, которое максимально приспособлено для практического применения. В таком исчислении поиск дерева вывода для целевой формулы Ф исходной системы КТ должен быть лаконичным, наглядным и технически простым, и, кроме того, должен порождать доказательство Ф в KTseq (с использованием соответственных преобразований).


Заметим, что для облегчения задачи поиска вывода, вместе с каждым уже опровергнутым вхождением некой подформулы в формулу Ф, мы также хотели бы иметь информацию о правилах вывода исчисления KTФinv, которые можно применить к этой подформуле в данном вхождении (уже упоминавшаяся «бесповторность вывода»). С учетом сказанного, введем понятие пути следующим образом (подобное понятие для системы К было использовано в работе [Voronkov 2000]).

Определение 4.3. Пусть С – формула системы KTseq, С1 и С2 – ее подформулы.

Путем в Ф или Ф-путем будем называть любую конечную последовательность символов l, r, l, r,,, которая удовлетворяет следующим правилам:

Пустой путь есть Ф-путь.

Предположим, что – Ф-путь, тогда если С имеет вид С1С2, то l и r есть Ф-пути, и есть -путь;

если С имеет вид С1С2, то l и r есть Ф-пути, и есть -путь;

если С имеет вид С1, тогда есть Ф-путь, и есть -путь;

если С имеет вид С1, тогда есть Ф-путь, и есть -путь.

Определение 4.4. Подформула формулы Ф на пути, обозначаемая Ф|, определяется индуктивно по следующим правилам:

Для пустого пути Ф| есть сама Ф.

Предположим, что – Ф-путь и Ф| = С, тогда если С имеет вид С1С2, то Ф|l С1, Ф|r С2;

если С имеет вид С1С2, то Ф|l С1, Ф|r С2;

если С имеет вид С1, то Ф| С1;

если С имеет вид С1, то Ф| С1.

4.2.1. Прямое исчисление путей Построим прямое исчисление путей KTФpath (или просто исчисление путей) следующим образом. Пусть 1,…,n – Ф-пути. П = 1, …, n, П = 1,…,n, и Г – некоторые последовательности путей. Тогда аксиомами исчисления путей являются любые формулы вида: Г, 1, 2, где p = Ф|1, ~p = Ф|2, для некоторой пропозициональной переменной р.

Определим правила вывода исчисления KTФpath:

Г, l, r ();

Г, l Г,r ();

Г, Г, П, П, ();

( ).

Г, П, П, Для того, чтобы связать введенное исчисление путей KTФpath и вывод в нем с выводом в исчислении KTseq, введем понятие образа формулы.

Определение 4.5. Образом формул секвенции путей или дерева вывода в исчислении путей KTФpath называется, соответственно, последовательность выводов или дерево вывода, полученное из первоначальных заменой каждого пути на формулу Ф|.

Прежде чем непосредственно приступить к доказательству теоремы полноты KTФpath, докажем следующую лемму.

Лемма (бимоделирования для KTФpath).

1. Пусть D – дерево вывода пустого пути в KTФpath Тогда образ формул из D является деревом вывода формулы Ф в KTseq.

2. Пусть D – дерево вывода секвенции A1,…,An в KTseq и 1,…,n – такие пути, что Ф|i Ai, i =1,…,n. Тогда существует дерево вывода D для 1,…,n в KTФpath такое, что D является образом формул дерева вывода D.

3. Пункты 1 и 2 справедливы, если везде «дерево вывода» заменить на «опровержение»

Доказательство. Пункт 1 доказывается тривиально, путем прямого анализа правил вывода в KTФpath., п.3 непосредственно следует из пп. 1 и 2.

Доказательство пункта 2 будем проводить методом индукции по длине вывода в D. Рассмотрим только случай, когда последним выводом является вывод по правилу (). Остальные случаи доказываются аналогично.

Не умаляя общности, можно предположить, что An = ВС и An является основной формулой последнего вывода. Тогда дерево вывода D имеет вид:

D1 D A1, …, An-1, B A1, …, An-1, C () A1, …, An-1, BC Очевидно, что nl и nr являются путями в Ф. Применяя индукционную гипотезу к деревьям вывода D1 и D2, получаем деревья вывода D1 и D такие, что D1 и D2 являются их образами формул.

Определим D как дерево вывода:

D1 D 1, …, n-1, nl 1, …, n-1, nr () 1, …, n-1, n Очевидно, что D является образом формул D.

Теперь можно приступить к доказательству следующей теоремы.

Теорема 4.3. (теорема полноты для KTФpath). Формула Ф логики KT невыполнима тогда и только тогда, когда пустой путь имеет опровержение в KTФpath.

Доказательство. По теореме полноты для KTseq невыполнимость Ф эквивалентна существованию опровержения Ф в KTseq.

Пусть пустой путь имеет опровержение в KTФpath.. По лемме бимоделирования существует опровержение в KTseq формулы Ф|, т.е. Ф.

Пусть D - опровержение формулы Ф в KTseq. По лемме бимоделирования существует опровержение D в KTФpath, чьим образом формул является D. Очевидно, что D есть опровержение.

4.2.2. Обратное исчисление путей Подобно тому, как было задано обратное исчисление секвенций КТФinv, определим обратное исчисление путей KTФIP.

Пусть 1,…,n – Ф-пути. П 1,…,n, П 1,…,n и Г – некоторые последовательности путей. Тогда аксиомами исчисления путей являются любые формулы вида: 1, 2, где p = Ф1, ~p = Ф2, для некоторой пропозициональной переменной р.

Правила вывода исчисления KTФpath следующие:

Г, l (l);

Г, r (r);

Г, Г, Г, l, r ();

Г,, (C);

Г,, Г, П, ();

П, Г (+);

() П, П, Г, Для KTФIP, так же как и для KTФpath, справедлива лемма бимоделирования в следующей формулировке:

Лемма (бимоделирования для KTФIP).

1. Пусть D – дерево вывода в KTФIP.. Тогда образ формул D является деревом вывода формулы Ф в KTinv.

2. Пусть D - дерево вывода секвенции А1,…,Аn в KTФIP и 1,…,n – такие Фi =Ai, i =1,…,n. Тогда существует дерево вывода D для пути, что 1,…,n в KTФIP такое, что D является образом формул дерева вывода D.

3. Пункты 1 и 2 справедливы, если везде “дерево вывода” заменить на “опровержение”.

Доказательство аналогично доказательству соответствующей леммы для KTФpath.

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

Теорема 4.4. (теорема полноты KTФIP) Формула Ф из системы КТ невыполнима тогда и только тогда, когда пустой путь имеет опровержение в исчислении KTФIP.

4.3. Анализ избыточностей и полнота KTФ,*IP Установим несколько важных свойств деревьев вывода в KTФpath, которые в дальнейшем помогут избавиться от избыточных секвенций в пространстве поиска вывода.

Определение 4.6. Модальная длина пути есть число вхождений операторов и в путь.

Лемма (о секвенциях с равной модальной длиной). Пусть П – секвенция путей, входящая в дерево вывода пустого пути в KTФpath. Тогда любые пути в П имеют одинаковую модальную длину.

Доказательство. Учитывая тот факт, что для любого правила вывода, если заключение П удовлетворяет требованию Леммы, то и все посылки этого вывода удовлетворяют требованию леммы, мы получаем доказательство непосредственной индукцией по числу выводов в дереве вывода.

Определение 4.7. Путь называется префиксом пути, если для некоторого пути – будем обозначаем это.

Определение 4.8. Префикс пути называется собственным, если ( ) – будем обозначать это.

Определение 4.9. Секвенция путей П называется свободной от префиксов, если для любых вхождений в П различных путей 1, 2, путь 1 не является префиксом пути 2.

Лемма (о секвенциях, свободных от префиксов). Любая секвенция путей, входящая в дерево вывода пустого пути является свободной от префиксов.

Доказательство. Аналогично доказательству предыдущей леммы.

Достаточно заметить, что свойство имеет силу для всех посылок вывода, всякий раз, когда оно имеет силу для его заключения.

Определение 4.10. Будем говорить, что два пути 1 и 2 образуют -вилку, если выполняется одно из следующих условий:

1=l1, 2=r2, для некоторых путей, 1, 2 или (симметрично) 1=r1, 2=l2, для некоторых путей, 1, 2.

Определение 4.11. Пути 1 и 2 называются ромборазделенными, если 1 11 и 2 22 для некоторых путей 1, 2, 1, 2 таких, что пути 1 и 2 имеют равную модальную длину и (1 2).

Лемма (о секвенциях, образующих -вилку). Пусть П – секвенция путей, входящая в дерево вывода пустого пути в KTФpath. Тогда не существует пары путей 1 и 2 в секвенции П, образующих -вилку.

Доказательство. Доказательство ведем от противного. Предположим, что два пути 1 и 2, входящие в секвенцию путей П образуют -вилку.

Допустим, что 1=l1 и 2=r2 для некоторых путей, 1, 2.

Рассмотрим ветвь В дерева вывода пустого пути, на которой лежит секвенция П, и верхнюю секвенцию на этой ветви, где l и r впервые появились. Допустим, что l появляется раньше, чем r (другой случай симметричен). Тогда дерево вывода содержит следующее поддерево:

Г1, l Г1, r () Г1, Г2, l Г2, r () Г2, Поскольку Г1, появляется в дереве вывода выше, чем Г2,r, то Г должна содержать префикс. – Это противоречит лемме о секвенциях, свободных от префиксов, так как последовательность путей Г2,r должна быть свободной от префиксов.

Лемма (о ромборазделенных путях). Пусть П – секвенция путей, входящая в дерево вывода в KTФpath. Тогда в П не существует ромборазделенной пары путей 1, 2.

Доказательство. Доказательство проводим от противного. Предположим, 1,2, что пара путей входящих в секвенцию П является ромборазделенной. Тогда, по определению ромборазделенных путей, существуют такие пути 1, 2, 1, 2, что 1 11, 2 22, (1 2). Причем пути 1 и 2 имеют одинаковую модальную длину.

Рассмотрим ветвь В дерева вывода пустого пути, на которой лежит секвенция П, и верхнюю секвенцию на ветви В, где 1 и 2 появились впервые. Не умаляя общности, предположим, что 1 встречается ранее 2 (другой случай симметричен). Тогда дерево вывода содержит следующее поддерево:

Г1, 1 () Г1, 1, Г2, 2 () Г2, 2, Поскольку 2 имеет модальную длину, несложно видеть, что все секвенции путей между Г2, 2 и Г1,1,1 содержат формулу с модальной длиной по крайней мере +1. Следовательно секвенция Г1,1,1 содержит путь модальной длины по крайней мере +1, и путь модальной длины. Это противоречит лемме о секвенциях с равной модальной длиной, поскольку все пути в секвенции путей Г1,1, должны иметь одинаковую модальную длину.

1, Определение 4.12. Будем говорить, что пара путей является -вилку противоречивой, если пути образуют либо являются ромборазделенными.


Определение 4.13. Обозначим через KTФ,*IP исчисление, полученное из KTФIP:

удалением всех секвенций путей, содержащих пути различной модальной длины;

удалением всех секвенций путей, содержащих противоречивую пару путей.

В введенном исчислении KTФ,*IP справедлива следующая лемма.

Лемма (подсеквенциальности для KTФ,*IP). Пусть D – дерево вывода пустого пути в KTФpath, и в D имеется фрагмент (вывод) вида Г1, …, Гn Г кроме того, пусть имеются секвенции путей 1,…,n такие, что каждая i есть подсеквенция соответствующей секвенции Гi.

Тогда существует дерево вывода D для в KTФ,*IP из 1,…,n такое, что является подсеквенцией Г.

Здесь не приводится полного доказательства леммы, поскольку оно во многом схоже с соответствующим доказательством для КТФinv, описанным выше, и в дальнейшем будет доказана теорема полноты с более сильными критериями избыточности. Заметим лишь следующее. Согласно лемме о ромборазделенных путях и лемме о секвенциях, образующих -вилку, каждая секвенция путей из Г1,…,Гn не содержит противоречивой пары путей.

1,…,n Поскольку являются мультиподмножествами Г1,…,Гn, соответственно, получаем, что ни одна из 1,…,n также не содержит противоречивую пару путей. Более того, если ищется дерево вывода из 1,…,n, то, поскольку есть мультиподмножество Г, то и не содержит противоречивой пары путей. Аналогично проверяется, что не содержит секвенцию путей с парами путей различной модальной длины.

Приведенные пять лемм описывают свойства исчисления KTФpath, опираясь на которые мы можем теперь сформулировать и доказать теорему KTФ,*IP.

полноты для Эта теорема гарантирует строгое логическое обоснование применения рассмотренных выше критериев избыточности в разрешающей процедуре, основанной на обратном методе.

Теорема 4.5. (полноты KTФ,*IP) Формула Ф системы КТ невыполнима тогда и только тогда, когда имеет опровержение в исчислении KTФ,*IP.

Доказательство.

предположим, что формула Ф невыполнима. По теореме полноты для KTФpath, секвенция имеет опровержение в KTФpath. По лемме подсеквенциальности для KTФ,*IP, существует подсеквенция из, имеющая опровержение в KTФ,*IP. Очевидно, что пустая секвенция не имеет опровержения в KTФ,*IP, поэтому имеет опровержение в KTФ,*IP.

Предположим, что имеет опровержение в KTФ,*IP. По лемме бимоделирования для KTФIP секвенция Ф имеет опровержение в KTФinv.

Поскольку в KTФinv каждая секвенция, имеющая опровержение является невыполнимой, то Ф – невыполнима.

4.4. Выводы В этом разделе с целью создания приемлемых условий программной реализации алгоритма обратного метода для модальных систем построены специальные исчисления путей: прямое и обратное. Исчисления позволяют проследить последовательность вывода с использованием соответствующего (построенного) бинарного дерева, которое наглядно отображает шаги вывода проверяемой формулы из заданных аксиом. Достоверность и корректность планирования при этом опираются на доказанные в главе леммы и теоремы.

Предлагаемый в главе механизм вывода является достаточно естественным и наглядным для человека и допускает контроль со стороны прикладного эксперта или технического специалиста. Он (механизм) также хорошо приспособлен для практических реализаций, в частности, машин вывода в различных системах принятия решения, экспертных и других когнитивных комплексах. Естественность и наглядность становятся весьма существенными, поскольку составной частью любой KBS по сложившейся традиции должна быть мощная подсистема, объясняющая найденные решения.

Глава 5. Ф-упорядочение 5.

5.

В предыдущих разделах рассматривались свойства исчисления путей, позволяющие избавиться от избыточных секвенций в дереве вывода.

Приведем утверждения, описывающие полезные свойства множества всех возможных деревьев вывода в исчислениях путей. Здесь и ниже нашей целью является ограничение поиска опровержения только некоторым подмножеством деревьев вывода, что достигается введением специального упорядочения на множестве Ф-путей.

5.1. Определения и соглашения Рассмотрим метод резолюций с одной из наиболее популярных стратегий упорядочения для классической логики. Метод сортирует литералы в дизъюнктах и затем требует, чтобы правило резолюций применялось только тогда, когда наибольшие литералы в обоих дизъюнктах были бы разрешимы.

Введем подобные ограничения на построение деревьев вывода для рассматриваемой модальной логической системы КТ. Преобразуем классическое упорядочивание литер на модальный случай и будем называть его Ф-упорядочением.

В случае классического исчисления предикатов, можно использовать любое упорядочение на подформулах Ф (или на Ф-путях), которое принимает во внимание префиксное отношение. Непосредственный перенос подобного упорядочения на модальные системы невозможен по причине того, что не каждое упорядочение на путях сохраняет свойство полноты. В подтверждение этого тезиса рассмотрим следующий вывод:

l, rl l, rrl l, rl r, rrl () l, rl, rrl В этом дереве существенно, что любой ()-вывод применяется выше правила (), потому что правило () не применимо к верхним секвенциям. Тем не менее, если мы определим упорядочение на пути, в которых rl l является наименьшим в первой предпосылке, то мы исключим возможность применения правила () первым и не сможем найти доказательство. – Таким образом, определение Ф-упорядочения в модальных логиках является более сложным, чем в классическом исчислении предикатов.

Для решения проблемы введения упорядочения зафиксируем ряд определений, соглашений и обозначений.

Определение 5.1. Два пути называются братьями, если один из них имеет вид l, а другой – r, либо один имеет вид r, а другой – l.

Братьями, например, являются пути rl l и rl r из рассмотренного выше вывода. Ясно, что каждое правило вывода конъюнкции или дизъюнкции обуславливает пару братьев.

Обозначения. В дальнейшем тексте работы символом ‘’ обозначается любой из символов ‘’ или ‘’, символом (подстрочным) ‘*’ – любой из символов ‘r’ или ‘l’, а символом ‘‘ любой из символов ‘ ’ или ‘’.

Определение 5.2. Пусть задана формула Ф. Ф-упорядочением с обозначением ‘ ’ будем называть отношение полного порядка на множестве всех Ф-путей, удовлетворяющее следующим условиям:

1. 1 2, всякий раз когда:

a) модальная длина 1 строго больше модальной длины 2, или b) 1 и 2 имеют одинаковую модальную длину, последний символ – *, а последний символ 2 –, или c) 1 и 2 имеют одинаковую модальную длину и 2 1 (заметим, что этот и предыдущий случаи не являются исключающими, но и не противоречат один другому);

2. не существует пути между двумя братьями, то есть не существует Ф-путей 1, 2, 3 таких, что 1 2 3, где 1, 3 – братья.

Содержательно, отношение позволяет управлять порядком применения правил – сначала правила применяются к формулам, большим относительно. Помимо этого отношение требует, чтобы заключение любого правила было меньше, чем любая его предпосылка в мультимножественном упорядочении. Условие (1а) гарантирует, что заключение меньше посылки при применении правил () или (+). Условие (1b) введено для того, чтобы применение () или (+) к секвенции, содержащей путь * не дало неполное исчисление. Условия (1с-d) и (2) являются не только техническими и служат для облегчения доказательств утверждений этого параграфа, но и однозначно определяют любые два пути по отношению к порядку, что важно в плане реализации.

Приведем пример Ф-упорядочения. Пусть дана модальная формула Ф:

Ф a (~ab)~bb В этой формуле существуют Ф-пути, отображенные в следующей таблице:

№ Ф/ 0 a(~ab)~bb 1 l a 7 l a 2 r (~ab)~bb 3 rl (~ab) 8 rl ~ab 11 rll ~a 12 rlr b 4 rr ~bb 5 rrl ~b 9 rrl ~b 6 rrr b 10 rrr b Каждый путь имеет индекс. Легко убедиться, что упорядочение i j (ji) является Ф-упорядочением.

l r 1 l r 7 3 l r 8 5 l r 11 12 9 Рис. 5.1. Ф-упорядочение и пути в формуле Обозначение. Будем использовать запись 1 2, если 1 2 или 1 = 2.

Для классической логики можно доказать полноту метода резолюций с упорядочением чисто семантическими рассуждениями [Bachmair, Gansinger 2000]. В случае модальной логики необходимо доказать, что стратегия выбора наибольшей формулы (или пути) в дизъюнкте совместима с критериями избыточности, рассмотренными ранее в этой работе. Поэтому доказательство полноты будем проводить в два этапа. На первом этапе докажем полезные свойства деревьев вывода в KTФpath, а на втором этапе перенесем их в обратное исчисление KTФIP, используя подходящий вариант леммы подсеквенциальности.

Следует отметить, что в отличие от рассмотренных ранее критериев избыточности, в доказательстве полноты появляются технические трудности, которые заключаются в том, что определение упорядочения формулируется в терминах посылок вывода, в то время как доказательство полноты для KTФpath развиваются из следствий. Этот факт приводит к некоторому усложнению определения упорядочения на путях, хотя и не является принципиальным препятствием.

Итак, покажем, что Ф-упорядочение существует для любой формулы Ф, и опишем алгоритм, который упорядочивает Ф-пути.

Алгоритм, работает с секвенциями из множества путей, эти секвенции будем обозначать Sn Sn-1 … S0. Содержательно, смысл приведенной записи заключается в том, что для любых путей Si и Si-1 мы имеем. Пути, принадлежащие одинаковым Si, еще не упорядочены, но должны быть упорядочены позднее в ходе работы алгоритма.

На каждом шаге алгоритма выбирается некоторое множество Si из секвенции, содержащее один или более членов, и Si заменяется двумя или Si1…Sik=Si.

более множествами Si1 … Sik такими, что Алгоритм заканчивает работу тогда, когда каждое множество содержит только один член.

Алгоритм (упорядочения):

1. Первоначально Si определяется как множество путей в формуле Ф модальной длины i.

2. Для всех Si, исключая последнее, делаем 3. выбираем пути 1, …, n в Si, заканчивающиеся ;

4. преобразуем Si в Si \ {1, …, n} {1} … {n};

5. преобразуем S0 в S0 \ {} {};

6. Пока существуют Si с более чем одним членом, делаем 7. выбираем в Si пути l и r, являющиеся братьями, такие, что Si;

8. выбираем L и R – множества всех префиксов соответственно из l и r;

9. преобразуем Si в Si \ (LR) R L {r} {l}.

Замечание. Заметим, что некоторые множества, например, L или R, могут быть пусты, в этом случае они не включаются в секвенцию.

Когда алгоритм завершится, секвенция состоит из одноэлементных множеств. В этом случае мы допускаем, что, если секвенция имеет вид …{} … {} ….

Покажем, как Ф-упорядочение на рис. 5.1 можно получить с помощью описанного алгоритма. Разбивающие шаги будем обозначать —, надписывая номер соответствующей строки (шага) в алгоритме. Вместо одноэлементных множеств {i} будем писать i.

{7, 8, 9, 10, 11, 12} {0, 1, 2, 3, 4, 5, 6}— {11, 12} 10 9 8 7 {0, 1, 2, 3, 4, 5, 6}— {11, 12} 10 9 8 7 {1, 2, 3, 4, 5, 6} 0— 12 11 10 9 8 7 {1, 2, 3, 4, 5, 6} 0— 12 11 10 9 8 7 {3, 4, 5, 6} 2 1 0— 12 11 10 9 8 7 {5, 6} 4 3 2 1 0— 12 11 10 9 8 7 6 5 4 3 2 1 0.

Докажем лемму, которая будет гарантировать, что описанный выше алгоритм упорядочивания удовлетворяет определению Ф-упорядочения.

Лемма. Любое упорядочение, полученное алгоритмом на формуле Ф, является Ф-упорядочением.

Доказательство. Во-первых, убедимся, что алгоритм завершится в том случае, если все множества Si состоят из одного элемента. Для этого мы должны показать, что в строке 7 алгоритма упорядочения мы всегда можем выбрать двух братьев l и r в Si таких, что Si.

Доказательство этого факта непосредственно следует из следующего Замечания. Каждое множество Mi состоящее более чем из одного элемента, полученное после строки 5 алгоритма, получено следующим способом. Существует множество путей 1, …, n одинаковой модальной длины такое, что i не является префиксом j при условии, что ij и множество { | для некоторых k, k, причем k Mi с имеют одинаковую модальную длину} Такое множество Si всегда будет содержать требуемую пару братьев, а именно k l и kr.

Во-вторых, мы должны показать, что упорядочение по алгоритму удовлетворяет всем условиям из определения Ф-упорядочения.

Условие 1а удовлетворяется в строке 1 алгоритма.

Условие 1b удовлетворяется в строках 2 – 4.

Проверим, выполняется ли условие 1с. Оно будет выполняться в строке в случае, когда 1 и 2 имеют различную модальную длину, и в строке 5, когда 2. Предположим теперь, что 1 и 2 имеют одинаковую модальную длину. Тогда условие 1с может быть нарушено только в строке 9. Покажем что это не так.

Из замечания к алгоритму следует, что (1) никакой путь в Si\(LR) не является префиксом пути в LR{r, l};

(2) никакой путь в R не является префиксом пути в L{r, l};

(3) никакой путь в L не является префиксом r либо l;

(4) r не является префиксом l. Условие выполняется в строке 9 алгоритма.

Поскольку на любом шаге алгоритма упорядочения мы получаем Ф-упорядочение, то справедливо важное Следствие. Ф-упорядочение существует.

Цель введения понятия Ф-упорядочения – доказать существование опровержения в форме, связанной с этим упорядочением. Ясно, что Ф-упорядочение сокращает пространство поиска вывода только таких специальных опровержений. Приведем еще несколько определений, необходимых для дальнейшего рассмотрения.

Обозначение. Пусть – путь, Г – секвенция путей. Запись Г будет служить сокращением утверждения « для любого из Г».

Определение 5.3. ()-вывод в KTФpath Г, l Г, r () Г, будем называть относящимся к Ф-упорядочению, если l Г и r Г.

Аналогично для ()-вывода:

Определение 5.4. ()-вывод в KTФpath Г, l Г, r () Г, будем называть относящимся к Ф-упорядочению, если l Г и r Г.

– Ф-упорядочение. Дерево вывода в KTФpath будем Определение 5.5. Пусть называть относящимся к, если каждый ()- и каждый ()-вывод из этого дерева относится к.

Лемма (о существовании вывода относящегося к ). Пусть Ф – невыполнимая формула и – некоторое Ф-упорядочение. Тогда существует опровержение в KTФpath, которое относится к.

Попытка прямого доказательства этой леммы (индукцией по длине пути без учета дополнительных соображений) может оказаться неудачной – не исключено получение вывода, не относящийся к Ф-упорядочению. Пример тому достаточно тривиален. Пусть и 1 – некоторые пути, причем 1 2l.

Рассмотрим секвенцию 1, 2. Мы можем применить правило вывода () из KTФpath для того, чтобы получить эту секвенцию:

1, 2l 1, 2r () 1, Фактически этот вывод является единственным способом вывода 1, 2.

Тем не менее, этот вывод не относится к.

Условия, наложенные на вывод для того, чтобы он относился к, сформулированы в терминах посылок вывода, но в таком индуктивном доказательстве мы можем расширить заключение только новым выводом. Для того, чтобы разрешить эту проблему, попытаемся избежать секвенций путей, которые приводят в описанное выше безвыходное положение, разрешая использовать только секвенции специального вида. Это так называемые -компактные секвенции путей.

Определение 5.6. Пусть 1, …, n – Ф-пути и – Ф-упорядочение. Секвенция путей Г = 1, …, n называется -компактом, если для каждого i=1,…,n выполняются следующие условия:

если i – -путь, тогда il Г и ir Г;

если i – -путь, тогда il Г и ir Г.

Используя введенные выше обобщенные обозначения для дизъюнкции, конъюнкции и модальностей, можно переформулировать определение -компактности:

Определение 5.7. Пусть 1,…,n – Ф-пути, и – Ф-упорядочение. Секвенция путей Г 1,…,n называется -компактом, если для каждого i=1,…,n и для каждого -пути i в Г мы имеем i* Г. Заметим, что i* i гарантируется i* Г условиями Ф-упорядочения, следовательно требование можно заменить на i* Г\{i}.

Следующая лемма утверждает, что компактная секвенция Г не может привести к безвыходной ситуации.

Лемма (о -компактах). Пусть – Ф-упорядочение, тогда посылка каждого ()-вывода – -компакт;

если Г – -компактная секвенция, встречающая в дереве вывода пустого пути, то каждый ()-вывод, имеющий секвенцию Г своим заключением, относится к ;

если Г – -компактная секвенция, встречающаяся в дереве вывода пустого пути, и если Г содержит по крайней мере один -путь или -путь, то существует ()-вывод, все посылки которого – -компакты.

Доказательство. Докажем, что посылка каждого ()-вывода П, () Г, П, -компактом, то есть для каждого в посылке, если * является является Ф-путем, тогда * П, \{}.

Докажем * П. Случай, когда П является подобным.

По лемме о секвенциях с равной модальной длиной, все пути в П, имеют одинаковую модальную длину, таким образом * имеет равную модальную длину с любым путем в П. По условию (1b) определения Ф упорядочения, имеем * П.

Проверим, является ли этот путь -компактом, то есть для каждого ли пути в предпосылке выполняется условие, что если * является Ф путем, тогда * П, -{}.

Покажем * П. (Случай, когда П является аналогичным).

1. По лемме о секвенциях с равной модальной длиной, все пути в имеют одинаковую модальную длину, так * имеет П, одинаковую модальную длину с любым путем в П. По условию (1b) определения Ф-упорядочения, мы имеем * П.

2. Докажем, что каждый ()-вывод, имеющий секвенцию Г своим заключением, относится к. Рассмотрим ()-вывод. В этом случае секвенция Г имеет вид П,, а сам вывод:

П, l, r ();

П, -компактом, l П, и r П,, Поскольку П, является следовательно вывод относится к.

Рассмотрим ()-вывод. В этом случае, как и в предыдущем, секвенция Г имеет вид П,, а вывод:

П, l П,r (), П, заметим, что П, является -компактом, l П, и r П,, следовательно и ()-вывод относится к.

Предположим, что секвенция Г содержит по крайней мере один 3.

путь. Нам надо доказать, что существует ()-вывод, все предпосылки которого являются -компактами.

Рассмотрим множество путей: S = {* | Г и * – Ф-путь}. По сделанному предположению это множество не пусто. Поскольку является линейным упорядочением, то это множество имеет наименьший элемент относительно отношения. Не умаляя общности, можно предположить, что это путь l. Тогда Г имеет вид П, для некоторой секвенции путей П. Рассмотрим вывод:

П, l, r () П, Докажем, что посылка этого вывода является -компактом.

Последнее равносильно доказательству того, что (3a) ** П, всякий раз, как только ** является Ф-путем;

(3b) для каждого пути П мы имеем * П, *, всякий раз, как только * является Ф-путем;

(3c) l* r и l* r Докажем последовательно каждый из этих пунктов.

3а) Поскольку П, – -компакт, * П. Очевидно, что * – префикс **, таким образом, по определению Ф-упорядочения (условие 1с), мы имеем ** *. Это влечет ** П.

3b) Поскольку П, – -компакт, * П, поэтому остается доказать * *, то есть * r. Заметим, что *S и l – наименьший элемент S, следовательно * l. По лемме о секвенциях, свободных от префиксов, * и l не совпадают, таким образом * l. С другой стороны по этой лемме, * не может быть префиксом l. К тому же, мы имеем * l и l является братом r, тогда по условию 2 определения Ф упорядочения, * r.

3с) Докажем случай l* r (второе утверждение о дизъюнкции доказывается аналогично).

Доказательство будем вести методом от противного. Предположим, что r l*. Поскольку относится к префиксному отношению, мы также имеем r l* l. Это противоречит условию 2 из определения Ф-упорядочения, поскольку путь l* расположен между двумя братьями.

Теперь, опираясь на предыдущую лемму, можно доказать ранее сформулированную лемму о существовании вывода, относящегося к.

Лемма (о существовании вывода, относящегося к ). Пусть Ф – невыполнимая формула и есть Ф-упорядочение. Тогда существует опровержение в KTФpath, которое относится к.

Доказательство. Доказательство проводиться индукцией по длине вывода.



Pages:     | 1 || 3 |
 





 
© 2013 www.libed.ru - «Бесплатная библиотека научно-практических конференций»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.