Содержание к диссертации
Введение
Глава 1. Логические подходы к управлению знаниями 16
1.1. Подход на базе классических и интуиционистских теорий 18
1.2. Модальные логики 24
1.3. Дескриптивные логики 31
1.4. Выводы 34
Глава 2. Структурные функциональные модели 35
2.1. Язык теории. Основные определения 35
2.2. Нерекурсивные детерминированные С-модели 46
2.3. Рекурсивные детерминированные С-модели 51
2.4. Интерпретация С-модели 57
2.5. Выводы 60
Глава 3. Установление выводимости в РДС-модели 62
3.1. Формальное исчисление. Правила вывода ...62
3.1.1. Исчисление /? 65
3.1.2. Корректность и полнота исчисления ЛЯ 68
3.2. Стратегия и алгоритм вывода в классе РДС 76
3.2.1. Описание алгоритма 76
3.2.2. Корректность алгоритма построения вывода 81
3.2.3. Особенности введения рекурсии 84
3.3. Проблемы реализации систем построения вывода 86
3.4. Выводы 92
Глава 4. Модальная логика и обратный метод 93
4.1. Базовые понятия и соглашения 97
4.1.1. Синтаксиси семантика логики КГ 100
4.1.2. Мультимножества и секвенции 105
4.1.3. Прямое и обратное исчисление секвенций для логики знания...108
4.2. Исчисление путей для логики КТ ...113
4.2.1. Прямое исчисление путей 115
4.2.2. Обратное исчисление путей 118
4.3. Анализ избыточностей и полнота A7*'V 120
4.4. Выводы 127
Глава 5. Ф-упорядоченис 128
5.1. Определения и соглашения 128
5.2. Полнота ЛТЛрбез секвенций, относящихся к у 147
5.3. Предпосылка как критерий избыточности 157
5.4. Выводы 179
Заключение 181
Список цитируемой литературы 187
- Дескриптивные логики
- Рекурсивные детерминированные С-модели
- Корректность алгоритма построения вывода
- Исчисление путей для логики КТ
Введение к работе
Интенсивное проникновение компьютеров во все области человеческой деятельности естественным образом приводит к необходимости моделировать и анализировать все более сложные прикладные области. Если первоначально компьютеры предназначались, преимущественно, для решения строго алгоритмизируемых задач, ассоциированных с теми или иными вычислительными проблемами, то, с недавних пор, информационно-вычислительные комплексы все чаще начинают служить «интеллектуальными помощниками». При этом нередко моделируемые области являются слабо-формализованными, когда анализ конкретной задачи и поиск ее решения подразумевает присутствие «творческого начала» - способности программного комплекса так или иначе моделировать интеллектуальные возможности человека, чтобы решать возникающие задачи, использовать эвристики, обучаться, накапливать и применять накопленный опыт. Такая необходимость обусловлена, как правило, полным отсутствием либо недостаточной степенью формализованности предметной области. Классическими примерами подобных ситуаций могут служить диагностика, проектирование, прогнозирование сложных явлений, а также другие области человеческой деятельности.
Рассматриваемая здесь область исследований в последние годы
привлекает повышенный интерес - с одной стороны, это определяется
революционным повышением технической мощности существующих
компьютерных систем и интенсивностью их использования, а, с другой, -следствием реальных успехов в моделировании ряда специфических интеллектуальных возможностей.
Следуя каноническим требованиям, прежде всего, определим актуальность исследования, его цели и задачи, а также сформулируем выносимые на рассмотрение полученные результаты.
Актуальность исследовании. В последние годы класс систем, позиционируемых разработчиками в качестве интеллекггуальиых (когнитивных), постоянно расширяется. Востребованность человека в получении интеллектуальных услуг становится все более значимой в связи с вовлечением в практику управления и анализа новых составляющих окружающего мира и необходимостью адекватного восприятия/использования этого окружения. - Для достижения указанной цели (интеллектуальной помощи), естественно, необходимо уметь моделировать и/или прогнозировать комплексное поведение компонентов анализируемой предметной области -будь то социология, климатология, медицина, органическая химия или нечто подобное. Упомянутые предметные области {ПО) обладают рядом общих свойств, среди которых важно отмстить следующие: > обилие вовлеченных в модель базовых понятий;
тотальное взаимовлияние этих понятий, приводящее, как правило, к NP (P-SPACE) полноте соответствующих алгоритмов;
отсутствие единой (общей) теории для прикладной области, т.е. существенная необъективность при формировании модели.
Подходы, которые учитывают структуриванность знаний (как правило, во внимание принимается иерархичность описания либо иное упорядочение) всегда являлись и являются базовыми при работе со сложными информационными комплексами, когда на передний план выходят вопросы практической эффективности. Современные логические формализмы, в том числе и нсклассические, позволяют рассчитывать на создание «почти интеллектуальных» комплексов для анализа реальных проблем с учетом семантики входящих в описание конструкций. Важной в плане реализации программных систем является также проблема оценки надежности используемого теоретического аппарата - логические ошибки значительно опаснее технических сбоев.
Термин «знание» очевидным образом ассоциируется с понятием «интеллект», то есть с присущей, насколько это известно, только человеку способностью творчески оперировать абстрактными понятиями и связями между ними. Здесь мы сознательно ограничиваем круг обсуждения, формально (в рамках специальных теорий), представляемыми информационными структурами, которые будем именовать знаниями (уже без
кавычек). Из сказанного сразу же следует, что целью работы является исследование проблем, связанных лишь с теми аспектами интеллектуальной деятельности, которые поддаются логико-математическому анализу.
Одной из важнейших проблем современных компьютерных наук (computer science) является построение инструментальных средств, максимально сокращающих объем специальных навыков, необходимых при использовании информационно-вычислительных технологий. Отмстим три наиболее значимых, на наш взгляд, области, для которых «интеллектуализация» является чрезвычайно важной. По степени вовлеченности пользователей на первое место, несомненно, следует поставить «Всемирную паутину» (World wide web или WWW) с ее гигантскими информационными ресурсами и сопутствующими проблемами менеджмента данных, с быстрорастущим количеством сетевых сервисов и недостатками механизмов реализации этих служб, с необходимостью управления сложной структурой Паутины и т.д.
Второй можно упомянуть нишу прикладных информационных
комплексов. Имеются в виду системы, использующие нетривиальный (как
правило, программно-математический) аппарат для получения результата
(прогноза, классификации), необходимого прикладному пользователю.
Наконец, третья из приводимых здесь областей практической деятельности
относится, главным образом, к науке или инженерии. Речь идет о
(возможном) желании прикладного специалиста самостоятельно и за
короткий срок создать необходимый ему программный продукт. - Здесь одним из наиболее перспективных подходов является разработка систем с возможностями автоматического синтеза программ.
Наиболее распространенными при построении программных комплексов управления и обработки знаний являются дедуктивные системы. Такие системы моделируют процессы проведения формально обоснованных, доказательных рассуждений, характерные для человека. Проблема построения доказательства традиционно понимается как проблема поиска вывода формулы логи ко -математического языка в соответствующем исчислении. Имеются многочисленные работы, связанные как со стандартными логиками (их разрешимыми фрагментами), так и рассматривающие неклассичсские исчисления (интуиционистские, нечеткие, дескриптивные и т.д.). В то же время предлагаемые формализации, зачастую, специфичны, не обладают универсальностью и не предлагают обобщений для классов (пусть и родственных) различных теорий представления и обработки знаний. Кроме того, как отмечалось ранее, далеко не всегда надлежащее внимание оказывается вопросам алгоритмической эффективности предлагаемых подходов.
Наконец, приведем еще одно важное соображение. Большая часть работ,
связанных с проблематикой установления выводимости, ориентированы на
так называемые «целсориептировапные» методы доказательства. - В них
движение происходит от целевого утверждения к аксиомам, что имеет как
положительные, так и отрицательные стороны. «Обратные» по отношению к «цслеориентированным» методы естественнее и не нуждаются в применении сложных механизмов возврата при неудаче (бэктрекинге), хотя и весьма чувствительны к объему пространства вывода. Вопросы повышения эффективности обратных методов исследованы достаточно мало, что также подтверждает полезность приведенных в диссертации результатов.
Цель работы. Диссертация посвящена созданию формальной теории, обеспечивающей создание строгих, достаточно выразительных и, в то же время, эффективных механизмов работы с предложениями логико-математических языков, предназначенных для описания моделей прикладных областей. Моделирование некоторой ПО подразумевает наличие строгой дисциплины описания понятий предметной области и связей (как правило, функционального характера) между этими понятиями. Правила вывода формальной теории служат для установления новых (не присутствующих явно в модели ПО) связей и построения схем реализации найденных связей (программ). Одним из важных принципов при проведении исследовании является использование так или иначе определяемых в пространствах вывода отношений частичного порядка (иерархий), что, как правило, обеспечивает высокую эффективность процедур установления выводимости для рассматриваемых логических систем. Отношения порядка, используемые в
работе, являются естественными, т.е. имеют содержательную трактовку в рамках предлагаемых формализмов.
Помимо этого, формализмы и алгоритмы установления выводимости
обладают свойствами полноты и корректности, а также, (большей частью,
строго подтвержденной) удовл створ ительн ой реализационной
эффективностью. Наконец, выразительные возможности разрабатываемой теории не беднее тех, которые предоставляются классическими системами логических спецификаций предметных областей типа Пролога.
При реализации объявленной программы мы опираемся на известные фундаментальные и частные результаты, ссылки на которые всегда явно отмечены. Проведенные исследования, традиционно относят к области автоматического доказательства теорем на базе дедуктивного подхода. Используемые для достижения сформулированной цели логические системы детально исследуются - для них доказываются теоремы пол і готы и строго формулируются алгоритмы построения вывода. Для алгоритмов также показывается корректность и приводятся сложностью оценки.
Методы исследования. В работе использован инструментарий математической логики, теории множеств, теории алгебраических систем, теории алгоритмов, теории графов.
Научная новизна полученных результатов определяется следующими положениями:
построена формальная теория структурных рекурсивных импликативных моделей ,57?, для нее показаны свойства эффективной распознаваемости и эффективной разрешимости, а также приведены варианты прикладного использования;
для исчисления SR сформулирован базовый обратный алгоритм установления выводимости формул, показана корректность алгоритма и определены его слоэ/сностные характеристики;
предложена бесповторная стратегия вывода, учитывающая структуру модели и естественный порядок на атрибутах;
сформулирован и обоснован подход к установлению выводимости формул для систем классов КТ и КТ45 (55) (модальных логик знания и автоэпистсмичсской логики);
> исследованы алгоритмические аспекты проблемы установления выводимости для предложенного подхода, на основании чего предложены строго обоснованные стратегии сокращения пространства поиска вывода, использующие Ф-упорядочеиие.
Практическая значимость. Все теоретические построения,
приведенные в диссертационном исследовании, формально строго
оооснованы и опираются на новейшие результаты в ооласти автоматического доказательства теорем. Полученные результаты частично использовались в реальных разработках (см. [Новосельцев 1985в], [Новосельцев и Калайда 1986] и [Новосельцев, Калайда и Шагисултанов 1991]) и применяются в настоящее время в ряде аспирантских исследований, которые ведутся под руководством автора. Они также могут быть использованы для реализации и исследования экономических моделей с конкурентным взаимодействием субъектов, децентрализованных комплексов управления сложными прикладными структурами, распределенных информационных систем различного назначения.
Апробации работы. Результаты работы докладывались в профильных семинарах ВМиК МГУ, ММФ СПбГУ, ФПМиК и ММФ ТГУ, АВТФ ТПУ, а также на ряде научных форумов различного уровня, среди которых можно отмстить следующие:
II Всероссийская конференция по прикладной логике - Новосибирск, ИМ СО РАН, 1988,
IX Международная школа ПП-91 «Программное обеспечение у і іравления и ИИ» - Иркутск, ИрВЦ СО РАН, 1991,
Международная конференция «Параллельные вычисления - 91» - Киев, ПК АН Украины, 1991,
Международная конференция «Логика и семантическое программирование» - Новосибирск, ИМ СО РАН, 1992,
5th International Symp. on Applied Logic-Tallinn, 1996,
Международная конференция «Всесибирские чтения по математике и механике. Томск 1997» - Томск, ТГУ, І997,
8th Korean-Russian International Symposium on Science and Technology -KORUS 2004, Томск, ТПУ,
8th WSEAS International Conference on APPLIED MATHEMATICS Puerto De La Cruz, Tcnerife, Canary Islands, Spain, 2005,
9th Korean-Russian International Symposium on Science and Technology -KORUS 2005, Новосибирск, НГТУ.
Результаты, выносимые на защиту:
Формальная теория структурных рекурсивных импликативных моделей SR для описания моделей различных прикладных областей.
Эффективные обратные стратегии и алгоритмы установления выводимости формулы в теории SR,
Формальный подход к установлению выводимости формул для модальных систем классов КТ и КТ45 (55) с использованием обратного метода.
> Строго обоснованные стратегии сокращения пространства поиска вывода в модальных системах на базе Ф-упорядочения, обеспечивающие реализацию надежных и эффективных интеллектуальных программных комплексов.
Объем и структура диссертации. Диссертация включает введение, пять глав, заключение и список литературы; общий объем составляет 207 страниц, включая иллюстрации.
Дескриптивные логики
Как отмечалось выше, подходы к работе с когнитивной информацией начали активно разрабатываться в 60-70-х годах прошлого века и разделились на 2 направления: логические формализмы и представления, основанные не на логике. Последние подходы позиционировались, как предлагающие универсальный инструментарий для различных типов задач. Знания в них представляются разнообразными информационными структурами (семантические сети и матрицы, фреймовые комплексы, потоковые сети и т.д.). Вообще говоря, выразительные возможности некоторых из перечисленных методик приближаются к выразительности естественного языка, при этом, правда, перспективы построения строгих формальных процедур манипулирования знаниями являются столь же отдаленными (возможно, недостижимыми), как и в случае естественного языка. Для работы со знаниями вводятся специальные стратегии, зачастую сильно зависящие от конкретной интерпретации моделируемой предметной области, частных взглядов разработчика и иных моментов субъективного характера. В последнее время в этих областях в качестве инструмента «наведения порядка» стали очень популярны так называемые дескриптивные логики (ДЛ).
Дескриптивные логики являются подмножеством модальных логик, при этом они рассматриваются как специализированные языки, поддерживающие типизацию и композицию [Borgida 1995]. Все ДЛ обладают, как минимум, двумя видами термов: концептами (классами - элементами базового домена) и ролями (бинарными отношениями на домене). Называя вещи своими именами, следует отметить, что ДЛ являются типизированными теориями, снабженными набором конструкторов специального вида. Концепт может быть комбинацией ранее определенных концептов и ролей, которая строится с использованием одного из конструкторов конкретного диалекта дескриптивного языка, что должно обеспечивать моделирование более сложных объектов анализируемой ПО [Borgida 1996]. При этом повторяем, дескриптивные логики позволяют расширять набор конструкторов относительно стандартного набора (конъюнкции, отрицания, квантора всеобщности и т.д.).
Важнейшей особенностью дескриптивных логик, их визитной карточкой, является возможность строить иерархии на концептах. Говорят, что концепт С является подклассом концепта D, если при любой интерпретации I, Q с D. Вводятся также понятия несвязных и согласованных концептов, т.е. определяется некоторый частичный порядок. Предлагаемые механизмы вывода большей частью используют семантические матрицы [Brachman and other 1993].
В тех или других вариантах дескриптивные логики применяются в области баз данных [Buchhcit and others 1997], в лингвистике, медицинских приложениях [Rector and others 1997] - область их применения постоянно растет. Помимо ставших уже классическими вариантов дескриптивных логик, разрабатываются расширения для вероятностных ДЛ [Koller, Levy and Pfeffer 1997], логик с «-арными ролевыми отношениями [Luntz, Sattler and Tobies 1995]. Появляются и другие вариации, увеличивающие выразительность языка и стройность создаваемых с их помощью моделей предметной области.
В настоящее время под руководством автора предлагаемой диссертации ведется аспирантское исследование, в котором предпринимается попытка переформулировать некоторые существующие версии дескриптивных формализмов и решить для них проблему установления выводимости предложений на основе предложенных здесь подходов.
Рекурсивные детерминированные С-модели
При описании этого класса существенно используются понятия детерминированной схемы и развертки, введённые в предыдущих разделах. Определение 2.16. С-модель M={S\,...,Sm) называется рекурсивной детерминированной (РД) С-моделью, если выполнены следующие требования:
1) М- синтаксически замкнута;
2) S\,...f S„- детерминированные схемы;
3) при построении развёртки любой схемы Sj модели М выражения вида a.Sj(...), где а - (различные) префиксы, появляются только в одной из двух альтернативных ветвей Л",-. При этом выражения а,{..,) определяют рекурсивные вхождения исходной схемы, ветвь, в которой имеются рекурсивные вхождения, называется рекурсивной ветвью, а сама S,- --рекурсивной схемой.
Полиномиальная распознаваемость описанных в представленном формализме моделей обеспечивается следующей теоремой.
Теорема2.2. Принадлежность С-модсли M=(S\,...jSm) классу РДС устанавливается конструктивно за конечное время, пропорциональное
(ЩМ\А)=Схт\ Доказательство. Построим конструктивную процедуру проверки выполнения определения 2.16.
1) Требование синтаксической замкнутости проверяется со временем, не превышающим 0{\М\ ). - Рассматриваем последовательно схемы S-, модели М. Для каждой подсхемы из заголовка S, со временем не более 0(Е) выясняем, является ли она элементарной; в случае отрицательного результата со временем 0(М) ищем её имя среди имен схем модели М, если оно там не обнаруживается, заключаем, что М не относится к классу РДС. Грубая оценка этого этапа Мх6 (Л +]Е)х(0(Л )+0{Е)) 0((М]+Е)3) может быть улучшена за счёт использования различных технических приёмов при описании модели, таких как аппарат предописаний, традиционный для языков программирования. Количество первичных схем Е считается фиксированным.
2) Требование детерминированности схем модели заключается в проверке выполнения определения 2.13 - отсутствие вариантной части заголовка, либо вариантная часть в форме if pz ...; ...fi\ время оценки - 0(\Щ).
3) Третий этап проверки - наиболее трудоёмкий. При этом также последовательно рассматриваются схемы модели. Производя развёртку S;, останавливаемся, когда доходим до элементарной подсхемы либо до рекурсивного вхождения схемы a.Sj(...). M-l. Развертка с вычеркиванием ЕСЛИ при этом не использовать дополнительные соображения, напрашивается очевидная оценка 0(\i\f\XlV \ где N- максимальное количество атрибутов в заголовках схем. Однако, затраты на этом этапе можно радикально уменьшить, заметив, что для анализа характера схемы Ss каждую подсхему в сё развертке достаточно рассмотреть один раз. Развёртка, полученная с использованием такой стратегии, схематически изображена на рис.2.3.
В этой развёртке выделены уровни:
первый - совпадает с заголовком исходной схемы, в котором каждая группа атрибутов с совпадающими именами схем (символами из множества D) для дальнейшей развертки имеет по одному представителю;
второй уровень - в развёртках на оставшихся атрибутах также оставлено по одному представителю для групп, а, кроме того, вычеркнуты атрибуты, имена схем которых совпадают с именами схем -непосредственных предшественников;
последующие - строятся аналогично.
Ясно, что глубина такой развертки не превышает \Щ-\. Таким образом, затраты третьего этапа могут быть оценены величиной 0(Л/[х((Л/х(Л/ 1)/2)х(Л/-1))) = 0(\ЩХ). Суммарные затраты па выполнение всех трёх этапов определяются оценкой для третьего этапа, т. е. 0(\М\ ).
Класс РДС-моделей включает в себя класс НДС. Задача для РДС-моделей удовлетворяет определению 2.10. Решение задачи T=(A(},XQ,S) В РДС-модели М, неформально, можно трактовать как нахождение пути в графе, соответствующем схеме S. Реализующий вычисление (программный) терм F строится с использованием ФС, которые явно или опосредованно присутствуют в схеме S. Исчисление, используемое при этом, будет строго описано и исследовано в последующих разделах, здесь проблема синтеза рассматривается на содержательном уровне. Подтерм G терма F отражает факт достижимости одних атрибутов схемы через другие, Простейшими подтермами являются имена ФС схемы S. Условие, при котором в процессе построения F обеспечивается достижимость некоторого атрибута, может не совпадать с условием, при котором этот атрибут описан в исходной схеме (в развёртке исходной схемы). В дальнейшем эти условия мы будем называть условиями достижимости и допустимости атрибута соответственно. Достижимость атрибута определяется (а) наличием в развёртке ФС, результатом которой является этот атрибут, (б) достижимостью аргументов такой ФС и (в) непротиворечивостью условий, при которых в процессе планирования достигнуты аргументы, и условия допустимости результата. Требование (в) является естественным отражением того, что величшгу ПО, имеющую смысл при условии р, нельзя вычислить через другую величину, определённую при дополнительном условии -р. Будем считать, что при использовании ФС f:(t\,...,a„ — а$ для построения терма F, условие достижимости «о определяется конъюнкцией условий достижимости аргументов и условия допустимости результата.
Корректность алгоритма построения вывода
Вывод заканчивается применением схемы аксиом - А0 состоит в точности из й, очевидно, BQC0. Длинна вывода - два - схема аксиом (0) и правило сужения (1). - Здесь, очевидно, также ЛсС0.
Индукция. Предположим, сделанное утверждение истинно для выводов, длина которых не превосходит к, и пусть вывод ПВ O FiA B имеет длину А+1. Если Ф получается но правилу сужения, то В принадлежит СА, которое найдётся по предположению для вывода, предшествующего получению Ф. Пусть В получено применением правила суперпозиции, например, из полученных ранее 0 \ F\iA- Z и &i f:Z- b (B=Z\Jb).
Вывод каждого из двух последних ПВ имеет длину меньше к+\. Следовательно по предположению, найдётся такое С,- (i frfl), что ZciQ. По способу введения правила композиции Ф2 является га-аксиомой -функциональной связью из набора filter исходной схемы S. Отсюда заключаем, что b (а, следовательно, и B=Zub) попадает в Q+j, где у" - число применений правил SR между получением в выводе ПВ Фі до использования ш-аксиомы Ф2 (включительно). (Ш) Правила ветвления и введения рекурсии в контексте доказываемой теоремы можно не различать - здесь нам не важен способ подтверждения предположения, появляющегося в последнем правиле, достаточно просто знать, что мы это делать умеем.
Итак, пусть ПВ b FiA- B получено по правилу ветвления, и длина вывода равна к+\. Пусть также Ф получено из \ F\\A B\tblQ8Lp и 02 F2:A Bub/Q&-p. Длина вывода как Фь так и Фг меньше А+1, следовательно найдутся Q и Су, которые содержат B\,blQ8ip и B\tb/Q&-p, соответственно, причём при построении СІ и Cj обсуждаемый алгоритм работает от одних и тех же исходных данных Л0. Отсюда видно, что атрибуты множества В и, в частности, bIQ будет включён в С„,ах(!-р+\, в силу того, что правило ветвления применяется сразу же, если показана достижимость атрибута при альтернативных условиях.
Поскольку но лемме принадлежность атрибута е замыканию AQ+ означает выводимость ПВ FiAo-їе, можно заключить, что обсуждаемый алгоритм корректно строит AQ . 3.2.3. Особенности введения рекурсии
Представим некоторые соображения по определению множеств А и X. Предположим, что в процессе планирования мы подошли к рассмотрению рекурсивной детерминированной схемы S(a) a.(A,...ifpZ)...; S(v),...fi \ fitter).
Не умаляя общности, предположим для простоты, что все подсхемы за исключением S являются элементарными. По сделанному предположению схема S стала текущей с «входом», определяемым множеством А (множеством у-атрибутов схемы S, для которых показана достижимость).
Опишем на содержательном уровне процесс, который позволяет определить множества аргументов и результатов рекурсивного ГТВ из заключения правила введения рекурсии. Сначала, не применяя правила (4) исчисления SR для схемы S, выводим из атрибутов А всё, что возможно. Во множество аргументов Arg включаем все входные атрибуты А. Для этих атрибутов показана достижимость при условии, которое приписано постоянной части схемы S (условие «входа» в S). После этого определяем замыкание А и объявляем его окончательным множеством аргументов Arg.
Во множество результатов Res помешаем j-атрибуты из постоянной части схемы S не попадающие в Arg, для которых показана достижимость от Arg при условии нерекурсивной ветви, и такие, что вовлечены в левые части ФС вида a.f:...,a.v.b,.,. a.c - «выводящие» из рекурсивного вхождения схемы a(v). Наконец, транзитивное замыкание полученного множества атрибутов Res объявляем окончательным множеством результатов рекурсивного ПВ.
Замечание. Если любое из траЕїзитивньїх замыканий окажется пустым, применение правила введения рекурсии оказывается невозможным.
Замечание. Если транзитивное замыкание строить «в лоб», затраты времени могут стать экспоненциальными по числу атрибутов. Этих затрат можно избежать, анализируя циклы в графе, который соответствует рекурсивной схеме. При этом атрибуты вида а и г.а отождествляются.
Исчисление путей для логики КТ
Построим такое исчисление, которое максимально приспособлено для
практического применения. В таком исчислении поиск дерева вывода для целевой формулы Ф исходной системы КТ должен быть лаконичным, наглядным и технически простым, и, кроме того, должен порождать доказательство Ф в KTscq (с использованием соответственных преобразований).
Заметим, что для облегчения задачи поиска вывода, вместе с каждым уже опровергнутым вхождением некой подформулы в формулу Ф, мы также хотели бы иметь информацию о правилах вывода исчисления AT7 jnv, которые можно применить к этой подформуле в данном вхождении (уже упоминавшаяся «бесповторность вывода»). С учетом сказанного, введем понятие пути следующим образом (подобное понятие для системы К было использовано в работе [Voronkov 2000]).
Определение 4.3, Пусть С- формула системы ATSCC, Сі и Сг- ее подформулы. Путем в Ф или Ф-путсм будем называть любую конечную последовательность символов Л/, лп V/, vr, 3, 0, которая удовлетворяет следующим правилам:
Пустой путь є есть Ф-путь.
Предположим, что % - Ф-путь, тогда
113
если С имеет вид С\/\Съ то ял/ и ялг есть Ф-пути, и я есть л-путь;
если С имеет вид СУСг, толу/И nvr есть Ф-пути, и я есть v-путь;
если С имеет вид ЗСі, тогда кЗ есть Ф-путь, и я есть D-путь;
если С имеет вид ОС], тогда лО есть Ф-путь, и я есть 0-путь.
Определение 4.4. Подформула формулы Ф на пути я, обозначаемая Ф определяется индуктивно по следующим правилам:
Для пустого пути с ФЕ есть сама Ф.
Предположим, что к - Ф-путь и ФЕ - С, тогда
если С имеет вид С\/\Сг, то ФЯЛ =;С, Ф л Сь
если С имеет вид CvC2, то Ф\ы Си Ф\ Г± С2;
если С имеет вид ЗС], то Ф[лпі=;Сі;
если С имеет вид 0С, то Фло Сі.
Построим прямое исчисление путей Л рмь (или просто исчисление путей) следующим образом. Пусть яь...,я„ - Ф-пути. П = щ,..., п„, ПИ = яр,...,я,Д и Г — некоторые последовательности путей. Тогда аксиомами исчисления путей являются любые формулы вида: Г, щ, %г , где р = Ф\п\, /? = Фл2, для некоторой пропозициональной переменной/?.
Определим правила вывода исчисления КТ4 :
Для того, чтобы связать введенное исчисление путей AT paii, и вывод в нем с выводом в исчислении KTscq, введем понятие образа формулы.
Определение 4.5. Образом формул секвенции путей или дерева вывода в исчислении путей tf7 path называется, соотвегственно, последовательность выводов или дерево вывода, полученное из первоначальных заменой каждого пути я на формулу Фп.
Прежде чем непосредственно приступить к доказательству теоремы полноты ЛТ ь докажем следующую лемму.
Лемма (бішоделироватт для КҐ щ ).
\. Пусть D - дерево вывода пустого пути в КҐ р Тогда образ формул из D является деревом вывода формулы Ф в KTSQq.
2. Пусть D - дерево вывода секвенции А і, .../ „ в KTxq и Я,...,я,7-такие пути, что Ф\К А; , V/ =1,...,я. Тогда существует дерево вывода D для п\,...,к„ в ЯТ раи, такое, что D является образом формул дерева вывода D.
3. Пункты 1 и 2 справедливы, если везде «дерево вывода)) заменить на «опровержение))
Доказагельство. Пункт 1 доказывается тривиально, путем прямого анализа правил вывода в АТ4 ., п.З непосредственно следует из пп. I и 2.
Доказательство пункта 2 будем проводить методом индукции но длине вывода в D . Рассмотрим только случай, когда последним выводом является вывод по правилу (v). Остальные случаи доказываются аналогично.
Не умаляя общности, можно предположить, что Ап= BvC и Ап является основной формулой последнего вывода. Тогда дерево вывода D имеет вид:
Очевидно, что 7rnv/ и nnvr являются путями в Ф. Применяя индукционную гипотезу к деревьям вывода D{ и D2 , получаем деревья вывода D\ и D2 такие, что D\ и Ъ{ являются их образами формул.
Доказательство. По теореме полноты для КТ невыполнимость Ф эквивалентна существованию опровержения Ф в КТ5Щ,
Пусть пустой путь с имеет опровержение В AT pyih.. По лемме бимоделирования существует опровержение в КТЖЦ формулы Фє, т.е. Ф.
= Пусть D - опровержение формулы Ф в ATseq. По лемме бимоделароеания существует опровержение D в КТ\. Ч чьим образом формул является D . Очевидно, что D есть опровержение г.
