Обратный метод установления выводимости для автоэпистемической логики и его применение в экспертных системах тема диссертации и автореферата по ВАК РФ 05.13.01, кандидат технических наук Ларионов, Дмитрий Сергеевич

• Ларионов, Дмитрий Сергеевич
• кандидат технических наук
• 2005

Оглавление диссертации кандидат технических наук Ларионов, Дмитрий Сергеевич

ВВЕДЕНИЕ.

1. Актуальность задачи поиска вывода.

2. Цель работы и задачи диссертации.

3. Методы построения алгоритма и исследований.

4. Апробация работы.

5. Научная новизна и практическая ценность результатов работы.

6. Личный вклад.

7. Основные положения, выносимые на защиту.

8. Постановка задачи.

9. Обзор родственных работ.

10. Структура работы.

ГЛАВА I. ЛОГИЧЕСКАЯ СИСТЕМА Б5 (КТ45).

1.1. Синтаксис и семантика модальной логики Б5.

1.1.1. Семантика возможных миров.

1.1.2. Свойство немонотонности автоэпистемической логики.

1.1.3. Автоэпистемическая логика, ее язык, синтаксис и семантика.

1.1.4. Семантика возможных миров автоэпистемической логики.

1.2. Понятие мультимножества и исчисление секвенций для системы 85.

1.2.1. Общая схема обратного метода установления выводимости.

1.3. Прямое исчисление 855е(5 и обратное исчисление 85\,у.

1.4. Выводы по главе.

ГЛАВА II. ИСЧИСЛЕНИЕ ПУТЕЙ ДЛЯ СИСТЕМЫ 85.

2.1. Исчисление путей 85фРАтн (прямое исчисление путей).

2.2. Обратное исчисление путей 85Ф1ЫУ.

2.3. Выводы по главе.

ГЛАВА Ш. УСТРАНЕНИЕ ИЗБЫТОЧНОСТЕЙ ИСЧИСЛЕНИЯ ПУТЕЙ.

3.1. Критерии избыточности для обратного метода.

3.2. Стратегия Ф-упорядочения.

3.2.1. Алгоритм упорядочения.

3.3. Полнота обратного метода исчисления 85% без секвенций, не относящихся к«>-».

3.4. Предпосылка как критерий избыточности.

3.5. Общий алгоритм установления выводимости.

3.6. Выводы по главе.

ГЛАВА IV. ПРИМЕНЕНИЕ ОБРАТНОГО МЕТОДА УСТАНОВЛЕНИЯ ВЫВОДИМОСТИ ДЛЯ МЕХАНИЗМА ВЫВОДА ЭКСПЕРТНЫХ СИСТЕМ.

4.1. Пример оболочки экспертной системы на основе классического нечеткого вывода.

4.2. Практической применение обратного метода установления выводимости для автоэпистемичекой логики.

4.2.1. Оценка актуарных гипотез ПФР.

4.2.2. Анализ производственной мощности предприятия.

4.3. Выводы по главе.

Введение диссертации (часть автореферата) на тему «Обратный метод установления выводимости для автоэпистемической логики и его применение в экспертных системах»

В последнее время интенсивно рассматриваются вопросы автоматизации процессов получения решений компьютерными программами - это связано не только с классическими задачами искусственного интеллекта доказательства теорем и построения советующих экспертных систем, но и с бурным развитием и внедрением в производственный процесс корпоративных информационных ERP-систем, CRM-систем [www.expert-systems.com], программ управления технологическими процессами, задач извлечения данных и знаний: анализ данных, анализ документов, поиск по смыслу в Internet, распознавание текста и так далее [9]. Несмотря на то, что для решения указанных вопросов успешно применяются такие технологии, как нейронные сети, семантические сети и фреймы, набирает рост и интерес к традиционному логическому методу хода рассуждений за счет привлечения неклассических модальных логик. Наличие большого числа эвристик в рассуждениях соответствующих систем, их неспособность всегда четко обосновать свое решение ставят под сомнение применение нелогических способов рассуждений. В свою очередь, вывод, опирающийся на одну из модальных логик, сохраняет строгость и обоснованность классических аксиоматических систем вывода, однако при этом он гибок за счет наличия операторов □ (необходимости) и 0 (возможности). Так же многие модальные логики обладают свойством немонотонности, позволяющим пересматривать свои выводы в процессе рассуждения.

В частности, проблему построения доказательства заданного целевого утверждения для экспертной системы можно свести к проблеме поиска вывода формул определенного логико-математического языка в соответствующем исчислении. Для теорий, основанных на классической логике, исходным пунктом в решении проблемы поиска вывода является, как правило, решение проблемы поиска вывода в исчислении предикатов первого порядка, на базе которого (добавляя те или иные аксиомы и правила вывода) осуществляется формализация различных математических теорий. Имеются многочисленные работы как в области теории логического вывода в классическом исчислении предикатов и теории разрешимых фрагментов этого исчисления, так и в области практического построения алгоритмов программ автоматического поиска вывода. Для автоматизации доказательства недостаточно решить удовлетворительно проблему автоматического поиска вывода в исчислении предикатов, особенно в случае, когда соответствующее теории исчисление имеет дополнительные правила вывода. Такой случай имеет место, например, при задании исчисления с равенством путем добавления не только аксиом, но и правил для равенства. Для успешной формализации желательно, чтобы методика построения алгоритмов автоматического поиска вывода допускала распространение на различные системы. Один из успешных примеров реализации такого алгоритма, реализующего обратный метод установления выводимости для модальной логики КТ, описан в работе В.В. Бурлуцкого [6]. В нем используется логика знаний, где оператор □ интерпретируется как «известно».

Рассмотрим основные подходы для модифицируемых рассуждений. К основным семействам немонотонных логик [33], [34], [7] можно отнести:

• Логики умолчаний [72]. Они позволяют формализовать модифицируемые рассуждения с помощью правил вывода, присущих области применения. Эти знания выражают правила вида «большинство птиц летает» в форме «если непротеворечив (выполним) вывод, что некая отдельная птица может летать, то она летает». Здесь есть возможность выражать правила с исключениями, не перечисляя сами эти исключения.

• Модальные немонотонные логики Мак-Дермотта [62], [63]. Эти логики базируются на аксиоматических системах модальной логики и предназначены для характеризации множеств взаимно «выполнимых» утверждений, которые можно вывести из какого-то задаваемого множества посылок.

• Автоэпистемические логики [67], [68], [69]. Это реконструкция немонотонных логик Мак-Дермотта. Взяв какую-либо систему модальной логики, предполагают, что некий идеально разумный агент рассуждает интроспективным образом в рамках выбранной системы и на основе своих собственных предположений. Рассуждения, проводимые агентом, являются модифицируемыми, ибо относятся к определенному состоянию знаний, которое может оказаться изменчивым. Хотя автоэпистемические логики и логики умолчаний создавались для различных применений, их выразительные возможности часто бывают равносильными [55].

Особо стоит отметить подходы через минимизацию [34], предназначенные для формализации модифицируемых рассуждений и естественно вписывающиеся в рамки классической логики. Вывод в таких системах основан на минимизационных соглашениях для стратегии обращения к неизвестным сведениям. Будучи примененным к базам данных, содержащим только сведения в элементарной логической форме, такое соглашение состоит в опровержении все еще незаписанной информации; истинной предполагается информация, явно присутствующая в базе данных, а вся остальная позитивная информация считается ложной. При обобщении на базы знаний эти соглашения состоят в более громоздких условиях минимальности, связанных с множествами определенных сущностей, удовлетворяющих некоторым формулам данной базы знаний. В качестве указанных минимизационных соглашений могут служить гипотеза замкнутого мира [71], [73], [75], [76], которая формулируется в виде принципов и методов, позволяющих управлять запросами базы знаний немонотонным образом по отношению к эволюции содержимого этой базы. Соглашения могут также принимать вид аксиом или схем аксиом, которые должны быть добавлены к рассматриваемой базе знаний, например, аксиом пополнения [57], [75], [76], [77] или аксиом очерчивания [60], [61] [58], [59]. В логическом программировании, например, в языке Пролог [5], [32], [1] специальные операторы аппроксимируют логическое отрицание с помощью некоторой конечной процедуры отрицания через неудачу [34], [57], [77]. Эти операторы позволяют доказать модифицируемым образом, что некое утверждение нельзя вывести на основе знаний, имеющихся в логической программе. В наиболее общем виде минимизационные соглашения представляются различными операциями разграничения областей истинности предикатов и формул из базы знаний, а также разграничения множеств и областей констант и функций этой базы. Эти операции взаимодействуют согласно определенным приоритетам и являются выразителями специфической рациональности рассуждающего агента

44], [34].

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

Заключение диссертации по теме «Системный анализ, управление и обработка информации (по отраслям)», Ларионов, Дмитрий Сергеевич

4.3. Выводы по главе

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

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

Заключение

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

1. Была сформулирована и теоретически обоснована оригинальная разрешающая процедура для автоэпистемической системы £5 - одной из самых выразительных и полных модальных логик.

2. Был сформулирован и теоретически обоснован интуитивно ясный и наглядный алгоритм поиска вывода для системы 5*5, который опирается на формализацию обратного метода, основанную на исчислении путей.

3. Были исследованы свойства построенного исчисления путей, на основании которых предложены строгообоснованные стратегии сокращения поиска вывода в системе ¿>5.

4. Была предложена и теоретически обоснована стратегия, основанная на Ф-упорядочении, определяющая эффективную последовательность применения правил вывода к дизъюнктам из пространства поиска вывода.

5. Были предложены и теоретически обоснованы эффективные стратегии для системы подобные стратегиям предпосылки для логик К и КТ, позволяющие заметно сокращать пространство поиска вывода уже в процессе порождения дизъюнктов.

6. Было проведено строгое доказательство теоремы полноты для исчисления путей системы 5*5 с учетом всех вышеназванных стратегий.

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

118 различного уровня. Предложенные алгоритмы удовлетворяют принятым современным критериям эффективности. Они были критически сопоставлены с различными традиционными методами поиска вывода.

Теоретическая и практическая ценность работы заключается в следующем:

1. Было проведено глубокое исследование базовых исчислений обратного метода системы Я5 и соответствующих им исчислений путей.

2. Был детально описан и теоретически обоснован механизм вывода для экспертной системы, база знаний которой формализована с помощью одного из самых семантически богатых языков модальной логики 55.

3. Были предложены эффективные и технически легко реализуемые стратегии для системы £5, сокращающие пространство поиска вывода уже в процессе пополнения базы данных дизъюнктов.

4. Реализована программа «Система проверки утверждений на основе модального вывода», показывающая, что особую пользу метод приносит в системах прогнозирования и проверки гипотез.

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

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

В главе IV показано, что применение автоэпистемической логики в качестве механизма вывода экспертной системы является достаточно результативным. Система 5*5 обладает операторами общности и существования, способными отразить нечеткие рассуждения эксперта, так как эвристическая составляющая -неотъемлемая часть работы экспертных систем. Кроме того, свойство немонотонности автоэпистемической логики позволяет вести эволюционирующие рассуждения, то есть позволяет программе отказываться от выводов, сделанных ранее и пересматривать их.

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

Список литературы диссертационного исследования кандидат технических наук Ларионов, Дмитрий Сергеевич, 2005 год

1. Адаменко А.Н., Кучу ков A.M. Логическое программирование и Visual Prolog.-СПб.: БХВ-Петербург, 2003. 992с.: ил.

2. Алексеева Е.Ф., Стефанюк В.Л. Экспертные системы (состояние и перспектива) // Известия АН СССР. Техническая кибернетика. 1984. -№5. - С. 153-167.

3. Барвайс Дж. Справочная книга по математической логике. М.: Наука. -1983.

4. Боброва Т.Ю., Горшкова Н.В., и др. Краткий актуарный сборник. М.: Современная экономика и право. - 88 с.

5. Братко И. Программирование на языке Пролог для искусственного интеллекта: М.: Мир, 1990. 560 е., ил.

6. Бурлуцкий В.В. Реализация обратного метода установления выводимости для модальной логики KT. Диссертация на соискание ученой степени кандидата физико-математических наук. 05.13.01. -Томск, 2001.

7. Вагин В.Н., Головина Е.Ю., Загорянская A.A., Фомина М.В. Достоверный и правдоподобный вывод в интеллектуальных системах. М.: ФИЗМАТЛИТ, 2004. - с. 704

8. Воронков A.A. Метод поиска доказательства// Вычислительные системы. Новосибирск. 1985. - т. 107

9. Гаврилов A.B. Гибридные интеллектуальные системы.-Новосибирск: Изд-во НГТУ, 2003.-164 с.

10. Гнеденко Б. В. Курс теории вероятностей: Учебник Изд. 6-е, - М.:Наука. Гл. ред. физ.-мат. лит., 1988. - 448 с.

11. Давыдов Г.В., Маслов С.Ю. и др. Машинный алгоритм установления выводимости на основе обратного метода// Записки ЛОМИ АН СССР. 1969. -т. 16. -С.8-20

12. Драгалин А.Г. Математический интуиционизм. Введение в теорию доказательств. М.:Наука. - 1979.

13. Ларионов Д.С. Модальная логика для механизма вывода экспертной системы// Труды XXIV Конференции молодых ученых механико-математического факультета МГУ. 2002. -1.-е. 108-110

14. Ларионов Д.С. Оболочка экспертной системы на базе нечеткого вывода// Труды XXII Конференции молодых ученых механико-математического факультета МГУ «Аналитические и численные методы в математике и механике». -2000.-I.-c. 97-101

15. Ларионов Д.С. Использование модальной логики для проектирования оболочек экспертных систем // Известия Томского Политехнического Университета. 2005. - Т. 308. - № 4. - С. 173-177.

16. Larionov D.S. Auto-epistemic Logic for Expert System's Inference Engine // Materials of the 9th Russian-Korean International Symposium on Science and Technology "KORUS-2005".-2005.-Vol. 1.- C. 649-652

17. Ларионов Д.С., Новосельцев В.Б. Оболочка экспертной системы на основе нечетких рассуждений с прямым и обратным выводом // Математическое моделирование.- 2002. Т. 14. - № 9. - С. 48-52.

18. Марселус Д. Программирование экспертных систем на Турбо Прологе: Пер. с англ. М.: Финансы и статистика, 1994. - 256 е.: ил.

19. Мае лов С.Ю. Обобщение обратного метода на исчисление предикатов с равенством// Записки ЛОМИ АН СССР. 1971. - т.20. - С.80-96

20. Маслов С.Ю. Обратный метод установления выводимости в классическом исчислении предикатов.-ДАН СССР, Т. 159, № 1, 1964.-С. 17-20.

21. Маслов С.Ю. Обратный метод установления выводимости для логических исчислений-Труды Мат.института АН СССР, Т.98, 1968.-С. 26-87.

22. Маслов С.Ю. Обратный метод установления выводимости для непредваренных формул исчисления предикатов// ДАН СССР. 1967. - №1. -С. 22-25.

23. Маслов С.Ю. О поиске вывода в исчислениях общего типа.-Зап. науч. семинаров.-ЛОМИ АН СССР, Т.32, 1972.- С. 59-65.

24. Маслов С.Ю. Применение обратного метода к теории разрешимых фрагментов классических исчислений// ДАН СССР. 1966. - №1. - С. 17-20.

25. Маслов С.Ю. Связь между тактиками обратного метода и метода резолюций// Записки ЛОМИ АН СССР. 1969. - т.16. - С.21-26

26. Мендельсон Э. Введение в математическую логику. М.: Наука. - 1976.

27. Минц Г.Е. Резолютивные исчисления для неклассических логик//9-ый Советский Кибернетический симпозиум, М.: ВИНИТИ. 1981.- т.2. - С.34-36

28. Попов Э. В. Экспертные системы: Решение неформализованных задач в диалоге с ЭВМ. М.: Наука. Гл. ред. физ.-мат. лит., 1987.-288 с.

29. Соловьев А. К. Актуарные расчеты в пенсионном страховании. -М.: Финансы и статистика, 2005.-240 е.: ил.

30. Стерлинг Л., Шапиро Э. Искусство программирования на языке Пролог: М.: Мир, 1990.-235 е., ил.

31. Тейз А., Грибомон П., Ж. Луи и др. Логический подход к искусственному интеллекту, т.1 От классической логики к логическому программированию-М.: Мир, 1990.

32. Тейз А., Грибомон П., Юлен Г. и др. Логический подход к искусственному интеллекту, т.2 От модальной логики к логике баз данных.-М.: Мир, 1998.

33. Уотермен Д. Руководство по экспертным системам: Пер. с англ. М.: Мир, 1989.-388 е., ил.

34. Фейс Р. Модальная логика. М.: Наука. - 1974.

35. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем.-М.: Наука, 1983.

36. Bachmair L. Gansinger Н. Resolution theorem proving// Handbook of Automated reasoning, Robinson A. And Voronkov A. Eds. Elsevier science and MIT Press. 2000.

37. Borger E., Grader E. and Gurevich Y. The Classical Decision Problem, Springer Verlag 1997

38. Davis M. Eliminating the Irrelevant from Mechanical Proofs// Proc. Symp. On Experimental Arithmetic, Chicago, 1962.

39. Degtyarev A. And Voronkov A. Equality elimination for the inverse method and extension procedures// Proc. International Joint Conference on Artificial Intelligence (IJCAI), C. Mellish ed., Montreal. 1995. - vol.1. - pp.342-347

40. Fitting, M. Proof methods for modal and intuicionistic logics// Synthese Library, Reidel Pub. Comp. 1983. - vol. 169.

41. Friedman J.A. Semi-decision procedure for the functional calculus// Journal of ACM.- 1963.-vol. 10, №1.-pp.1-25

42. Gelfond M. On stratified autoepistemic theories, Proc. AAAI-87, pp. 207-211, 1987.

43. Gentzen, G. Untersuchungen über das logische Schliesen// Mathematical Zeitschrift-39. 1934. - pp. 176-210, 405-431

44. Giuchinglia F. et al. SAT-based decision procedures for classical modal logics// Journal of automated reasoning. 1999. - To appear in the Special Issues: Satisfiability at the start of the year 2000. (SAT 2000)

45. Goldblatt, R. Logics of time and Computation// Lecture Notes, Center for the Study of Language and Information. 1987. - №7

46. Herbrand J. Recherches sur la theorie de la demonstration. Warsaw, 1930.

47. Horrocks I., Patel-Schneider P., Sebastiani R. An analysis on empirical testing for modal decosion procedures// Logic Journal of the IGPL 2000 - vol. 8, №3 - pp. 293323.

48. HustadtU. and ShmidtR. On evaluating decision procedures for modal logic// IJCAI-97. 1997. - vol.1. - pp.202-207

49. Jackson P. Introduction to Expert Systems. Addison Wesley, 1999.

50. Kleene S. C. Introduction to Mathematics, North-Holand, Amsterdam, 1952.

51. Konolige K. On the relation between default theories and auto-epistemic logic. Proc. IJCAI-87, pp. 394-401, 1987.

52. Kripke S.A. Semantical considerations on modal logic// Reference and Modality, Oxford University Press, London. 1971. - pp. 63-72

53. Kuken K. Negation in logic programming, J. Logic Programming, vol. 4, no. 4, pp. 289-308, 1987

54. Lifschitz V. Computing circumscription, Proc. IJCAI-85, pp. 121-127, 1985.

55. Lifschitz V. Pointwise circumscription: preliminary report, Proc. AAAI-86, pp. 406-410, 1986.

56. McCarthy J. Circumscription: a form of non-monotonic reasoning, Artificial Intelligence, vol. 13, no. 1-2, pp. 27-39, 1980.

57. McCarthy J. Applications of circumscription to formalizing common-sense knowledge, Artificial Intelligence, vol. 28, pp. 89-116, 1986.

58. McDermott D. and Doyle J. Non-Monotonic logic 1 // Artificial Intelligence. -1980. V. 13. - № 1-2. - P. 41-72.m 63. McDermott D. Non-monotonic logic 2: non-monotonic modal theories // J. ACM. -1982.-V. 29.-№ l.-P. 34-57.

59. Mints G. Resolution calculus for the first order linear logic// Journal of Logis, Language and Information. 1993. - №2. - pp.58-93

60. Mints G., Orevkov V. And Tammet T. Transfer of sequent calculus strategies to resolution for S4// Proof Theory of Modal logic. Studies in Pure and Applied logic, Kluwer Academic Publishers. 1996m

61. Mints G., Voronkov A. And Degtyarev A. Inverse method.// Handbook of Automated reasoning, Robinson A. And Voronkov A. Eds. Elsevier science and MIT Press. 2000

62. Moore R.C. Possible-world semantics for auto-epistemic logic // Proc. AAAI-Workshop on Non-Monotonic Reasoning. October 1984. - New Paltz, N.Y., 1984. -P. 344-354.

63. Moore R.C. Semantical considerations on non-monotonic logic // Artificial Intelligence. 1985. - V. 25. - № 1. - P. 75-94.

64. Moore R.C. Autoepistemic logic // Non-Standart Logics for Automated Reasoning (P. Smets et al., eds.). 1988. - P. 105-136.

65. Reuter R. A logic for default reasoning. Artificial Intelligence, vol. 13, no 1-2, pp. 81-131, 1980

66. Reiter R. On closed-world data base, in H. Gallaire and J. Minker (editeurs), Logic and Data Bases, Plenum Press, New York, pp. 55-76, 1978.

67. Robinson J.A. On automatic deduction// Rice Univ. Studies. 1964. - vol.50, №1. - pp. 69-89.

68. Shepherdson J.C. Negation as failture: a comparison of Clark's completed data base and Reiter's closed closed world assumption, J. Logic Programming, vol. 1, no. 1, pp. 51-79, 1984.

69. Shepherdson J.C. Negation as failture II, J. Logic Programming, vol. 2., no. 3, pp. 185-202, 1985.

70. Shepherdson J.C. Negation in logic programming, in J. Minker (editeur), Foundations of Mathematics, vol. 124, pp. 277-318, North-Holland, Amsterdam, 1988.

71. Stalnaker R. A note on non-monotonic modal logic, Dep. of Philosophy. Cornell University, Ithaca, New York, juin, 1980.

72. Tachella A. *SAT system description// Proceedings of the 1999 International Description Logic Workshop (DL'99), P.Lambrix, A.Borgida, M.Lenzerini, R.Moller and P.Pattel-Schneider, Eds. CEUR-WS. 1999. - vol.22. - pp. 142-144

73. Tammet T. Proof strategies in linear logic// Journal of automated reasoning. -1994. vol. 12, №3. - pp.273-304

74. Tammet T. Resolution theorem prover for intuitionistic logic// CADE-13, M.McRobbie and J.Slaney, Eds. Lecture Notes in Computer Science 1996. -vol.1104.-pp.2-16

75. Voronkov, A. K-inverse-K: a theorem prover for K// Automated Deduction. CADE-16, International Conference on Automated Deduction, H.Ganzinger Eds. Lecture Notes in Artificial Intelligence. 1999. - vol.1632, Springer Verlag. - pp.383387

76. Voronkov A. How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi// LICS'2000

77. Voronkov A. Theorem-proving in non-standard logic based on the inverse method// 11th International Conference on Automated Deduction, D. Kapur ed. Lecture Notes in Artificial Intelligence. 1992. - vol.607, Springer Verlag. - pp.648-662

78. Voronkov A. How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi// ACM Transactions and Computational logic.-2001.-vol. 1.- pp. 1-35

79. Wallen, L. Automated deduction in nonclassical logics. The MIT Press. - 1990 1982.-V. 29.-№ l.-P. 34-57.

80. Weidenbach et al. SPASS & FLOTTER version 0.42//CADE-13, M.McRobbie and J.Slaney, Eds. Lecture Notes in Artificial Intelligence. 1996. - vol.1104, Springer Verlag.-pp. 141-1451. Утверждаю»

81. Управляющий ГУ-ОПФР по Томской области

82. В Отделении ПФР по Томской области используется «Система проверки утверждений на основе модального вывода», разработанная Д.С. Ларионовым.

83. Логический вывод программы основан на следующих компонентах:1. автоэпистемических модальных рассуждениях;2. обратном методе выводимости;3. стратегии Ф-упорядочения формул.

84. На ОАО «Манотомь» внедрена программа «Система проверки утверждений на основе модального вывода», разработанная Д.С. Ларионовым.