Допустимые и выводимые правила вывода в нестандартных логиках тема автореферата и диссертации по математике, 01.01.06 ВАК РФ
|
Юрасова, Екатерина Михайловна
АВТОР
|
||||
|
кандидата физико-математических наук
УЧЕНАЯ СТЕПЕНЬ
|
||||
|
Красноярск
МЕСТО ЗАЩИТЫ
|
||||
|
2004
ГОД ЗАЩИТЫ
|
|
01.01.06
КОД ВАК РФ
|
||
|
|
||||
На правах рукописи
Юрасова Екатерина Михайловна
УДК 510.64
ДОПУСТИМЫЕ И ВЫВОДИМЫЕ ПРАВИЛА ВЫВОДА В НЕСТАНДАРТНЫХ ЛОГИКАХ
01.01.06— математическая логика, алгебра и теория чисел
АВТОРЕФЕРАТ
диссертации на соискание учёной степени кандидата физико-математических наук
Красноярск-2004
Работа выполнена в Красноярском государственном университете
Научный руководитель доктор физико-математических наук,
профессор В.В. Рыбаков, Официальные оппоненты: доктор физико-математических наук,
профессор А.Д. Яшин,
кандидат физико-математических наук,
СВ. Бабенышев.
Ведущая организация институт математики им. С.Л. Соболева
СО РАН, г. Новосибирск
Защита состоится 29 декабря 2004 г. в 11 часов на заседании диссертационного совета Д-212.099.02 в Красноярском государственном университете по адресу 660041, г. Красноярск, пр. Свободный, 79.
С диссертацией можно ознакомиться в библиотеке Красноярского государственного университета.
Автореферат разослан (3 И О^^Р^ 2004 г.
Ученый секретарь диссертационного совета кандидат физико-математических наук
доцент
Актуальность темы. Теория нестандартных систем логического вывода сформировалась в начале двадцатых-тридцатых годов 20-го века в работах Лукасевича, Льюиса, Геделя и Тарского, как результат анализа поведения аксиоматических систем оснований математики и парадоксов материальной импликации. Нестандартные логики по сравнению с классической логикой, отличаются большим разнообразием синтаксиса и семантики. Поэтому к концу 20-го века возникло много новых направлений исследований, связанных с применением идей и методов нестандартной логики в программировании, теории искусственного интеллекта, представлении знаний и других областях науки (см., например, [15, 23, 25, 30]).
Большое влияние на становление теории нестандартных систем логического вывода оказано классической теорией доказательств, одним из центральных моментов которой являются правила вывода, поскольку от них зависит эффективность доказательств. Первыми работами, непосредственно посвященными изучению правил вывода, были работы Лося (1955), Тарского (1956) и Сушко (1958). При исследовании правил вывода естественно возник вопрос о том какие правила можно присоединять к логическим системам, сохраняя при этом множество доказуемых теорем системы. Такой класс правил, получивших название допустимых правил вывода, был определен П. Лоренценом [20] в 1955 году. Оказалось, что это в точности допустимые правила вывода - правила, относительно которых данная логика замкнута.
В нестандартных логиках, как правило, класс допустимых правил вывода шире класса выводимых правил вывода. Примеры допустимых, но не выводимых правил вывода, были получены Р. Харропом [16], Г.Е. Минцем [5, 6]. Логика, в которой множества допустимых и выводимых правил вывода совпадают, называется структурно-полной. Большинство базисных логик, например, Н, К4, 54, 55 и др., не являются структурно-полными. Структурная полнота не является инвариантом заданной логики, она зависит от выбора аксиоматической системы. Однако, во многих распространенных классах логик правила вывода обычно фиксированы и выбор аксиоматической системы зависит от изменения множества аксиом. Именно для таких классов логик имеет смысл понятие структурной полноты. Исследования, связанные со структурной полнотой, можно найти, например, в работах [13, 24, 29, 31]. В [10] Циткину удалось описать все наследственно структурно-полные суперинтуиционистские логики, т.е. логики, всякое расширение которых является
ло получено полное описание наследственно структурно-полных модальных логик над К4 [26]. Однако уже для структурно-полных 84-логик малой глубины (меньше 5) класс структурно-полных логик шире класса наследственно структурно-полных логик. Поэтому особый интерес представляет описание классов структурно-полных логик над 54, К4.
После того как выяснилось, что для большинства нестандартных логик класс допустимых правил шире класса выводимых правил, возникли вопросы алгоритмической разрешимости распознавания допустимых правил вывода. Проблема нахождения алгоритма, распознающего допустимость правил вывода в интуиционистской логике была сформулирована в обзоре проблем X. Фридмана [14], родственная проблема существования конечного базиса для допустимых правил этой логики была поставлена А.В. Кузнецовым (см. [14] (проблема 42), [4]). Проблема алгоритмического распознавания допустимости в интуиционистской логике была решена положительно Рыбаковым [7], после чего вопрос о существовании конечного базиса был решен отрицательно так же Рыбаковым [8, 9]. Естественно возник вопрос построения бесконечного базиса, который позже был построен Иемхофф для интуиционистской логики [17]. Затем Рыбаков построил, также бесконечный, базис для логики 84 [28]. На основе техники, разработанной В.В. Рыбаковым, проблема допустимости была решена для различных индивидуальных транзитивных логик (см. например [1, 2, 11, 3]).
Ранее было отмечено, что ценность допустимых правил вывода заключается в том, что такие правила позволяют нам сократить и упростить выводы в дедуктивной системе заданной логики. Другой причиной, по которой изучаются данные правила вывода, являются различные приложения. Так, в работе Л.Л. Максимовой [22] приведено исследование свойств строгой разрешимости модальных и интуиционистских исчислений, рассмотрена проблема строгой разрешимости проективного свойства Бета над интуиционистским пропозициональным исчислением. Для доказательства строгой разрешимости проективного свойства Бета над интуиционистским пропозициональным исчислением достаточно решить проблему разрешимости по допустимости суперинтуиционистских логик с таким свойством. Максимовой [21] было показано, что существует точно 16 суперинтуиционистских логик, обладающих проективным свойством Бета. Из результатов В.В. Рыбакова [27] следует разрешимость проблемы допустимости для всех логик с таким свойством, кроме логик под номером 9, 13, 15 из полного списка логик с проективным свойством Бета [22]. Несмотря на то, что Рыбаков получил достаточно общий критерий допустимости правил вывода для финитно-аппроксимируемых логик [27], данный критерий не является уни-
версальным, поскольку одним из условий является наличие свойства ветвления ниже к. Так, логика, указанная под номером 9 в полном списке логик с проективным свойством Бета, не обладает свойством ветвления ниже к ни для какого к. Решение проблемы распознавания допустимых правил вывода в данной логике представлено в настоящей диссертационной работе.
Несмотря на глубокую разработку направления допустимых правил вывода, большинство результатов было получено для транзитивных логик. В настоящее время особый интерес представляют нетранзитивные логики, так как основные результаты и техники, использующиеся для исследования допустимых правил вывода в транзитивных логиках, применять непосредственно при изучении допустимых правил вывода в нетранзитивных логиках не удаётся. При исследовании допустимых правил вывода основным инструментом является реляционная семантика (или семантика Крип-ке, [18, 19]), причем центральную роль играют ^характеристические модели Крипке. Однако при построении ^характеристической модели возникает немало вопросов. На самом деле, построение ^характеристической модели является достаточно ясным только для расширений модальной логики К4 и интуиционистской логики. В случае нетранзитивной логики данные модели описаны только для очень малого списка логик, в частности, для К (см., например, [12]). В случае нетранзитивных временных логик описание упомянутых выше моделей представляется еще более сложной задачей.
Цель работы.
1. Исследовать на разрешимость по допустимости правил вывода суперинтуиционистскую логику, порожденную классом всех конечных корневых фреймов ¥, удовлетворяющих условию
(жПук.-I{уЯх)&уНгк,уНи) Эь(гШкиШ),
где Я - отношение на фрейме Положительное решение данной задачи позволяет обосновать предположение о строгой разрешимости проективного свойства Бета над логикой которое было выдвинуто в статье Л.Л. Максимовой [22].
2. Исследовать на разрешимость по допустимости логику с оператором "завтра".
3. Получить описание конечных корневых 54-фреймов ширины 2, порождающих структурно-полные логики.
Методика исследования. В исследовании применяются общие методы теоретико-модельной и алгебраической семантики для пропозициональ-
ных нестандартных логик. Например, метод фильтрации, метод канонических моделей, метод редуцирования правил вывода. Л также в исследовании использованы алгоритмический и семантический критерии допустимости правил вывода, критерий структурной полноты логики, некоторые результаты теории модальных напарников суперинтуиционистских логик.
Научная новизна. Все результаты, полученные в диссертации, являются новыми и снабжены подробными доказательствами. Результаты совместных работ получены в нераздельном соавторстве.
Основные результаты. В диссертации получены следующие основные результаты
1. Получен алгоритмический критерий распознавания допустимых правил вывода для М-логики порожденной классом всех конечных корневых фреймов F, удовлетворяющих условию
{xRyk.->{yRx)k,yRzkyRu) -)■ 3v(zRvkuRv), где R - отношение на фрейме F.
2. Доказано, что логика ® Grz и суперинтуиционистская логика, порожденная классом всех конечных корневых фреймов F, удовлетворяющих условию
(xRyk~>(yRx)kyRzkyRu) -4 3v(zRvkuRv),
где R - отношение на фрейме F, разрешима относительно допустимости правил вывода.
3. Получен алгоритмический критерий распознавания допустимых правил вывода для логики с оператором "завтра".
4. Получены необходимые и достаточные условия того, что ¿4-логика
ширины 2, порожденная конечным корневым фреймом без узлов с двухэлементным первым слоем, является структурно-полной.
Теоретическая и практическая ценность. Все полученные результаты носят теоретический характер и могут быть использованы в дальнейших исследованиях допустимых правил вывода в нестандартных логиках, а также в таких областях как теория моделей, теория графов и computer science.
Апробация работы. Результаты диссертации докладывались на
• XXXVП-ме:ждународной научной студенческой конференции "Студент и научно-технический прогресс" (Новосибирск, 1999),
• XXXVIH-международной научной студенческой конференции "Студент и научно-технический прогресс" (Новосибирск, 2000),
• XXXIX-международной научной студенческой конференции "Студент и научно-технический прогресс"(Новосибирск, 2001),
• XL-международной научной студенческой конференции "Студент и научно-технический прогресс" (Новосибирск, 2002),
• международной конференции "Ломоносовские чтения" (Москва, 2000),
• международной конференции "Логика и приложения", посвященной 60-летию со дня рождения Ю.Л. Ершова (Новосибирск, 2000),
• международной конференции "Дифференциальные уравнения и симметрия"
(Красноярск, 2000),
• международной конференции "Алгебра и ее приложения", посвященной 70-летию со дня рождения В.П.Шункова и 65-летию В.М.Бусаркина (Красноярск, 2002),
• международной научной конференции "Молодая наука - XXI веку" (Иваново, 2001),
• II Всесибирском конгрессе посвященном Софье Ковалевской (Красно -ярск, 2002),
• международной конференции "Мальцевские чтения" (Новосибирск, 2003),
• международной конференции "Алгебра, логика и кибернетика", посвященной 75-летию со дня рождения А.И.Кокорина (Иркутск, 2004).
Публикации. По теме диссертации опубликовано 22 работы [32]-[53].
Структура и объём работы. Диссертация состоит из введения, четырех глав, заключения и библиографического списка, включающего 103 наименования. Объём работы 103 страницы машинописного текста. СОДЕРЖАНИЕ РАБОТЫ
Во введении обосновывается актуальность выбранной в диссертационной работе темы. Даётся краткий обзор, теории допустимых правил вывода.
Описывается современное состояние вопросов, рассмотренных в диссертационной работе, сформулирован предмет, цель и методы проведения исследования, указаны основные его результаты. Приведены список конференций, на которых была проведена апробация работы, и даётся обзор всех разделов диссертации.
В первой главе представлены необходимые сведения о синтаксисе и семантике модальных, суперинтуиционистских и временных логик, а также методика применения ^характеристических моделей в исследованиях допустимых правил вывода.
В разделе 1.1 даны необходимые сведения о синтаксисе пропозициональных логик, рассмотрены примеры базисных логических систем.
В разделе 1.2 приведены некоторые важные понятия семантики Крип-ке. Даны необходимые факты из алгебраической семантики для модальных пропозициональных логик.
В разделе 1.3 дается описание ^характеристических моделей Крипке для модальных логик и ряд свойств ^характеристической модели. Приведены критерии допустимости правил вывода и структурной полноты модальных К4-логик с использованием га-характеристических моделей.
Во второй главе представлено решение проблемы допустимости правил вывода для модальной 54-логики Цъ, порожденной классом всех конечных корневых фреймов ¥, удовлетворяющих условию
{х!1ук-1{уЯх)ку11гкуНи) 3фЯи&иЯи),
где Я - отношение на фрейме Данная проблема решена также для модальной логики (12®^гг, откуда следует разрешимость по допустимости суперинтуиционистской логики порожденной классом всех конечных корневых фреймов ¥, удовлетворяющих условию {х!1у!к,-1(уКх)&,уВ,г&суКи) —> Зу(гНь&.и11у).
В разделе 2.1 приведены необходимые сведения, касающиеся связи между модальными и суперинтуиционистскими логиками. В данном разделе представлены результаты, полученные В.В. Рыбаковым при исследовании проблемы допустимости правил вывода для модальных логик над К4. В конце раздела введены определения необходимые при исследовании логик А*1> Я2> Ц2 ® Огг. Также введена модификация понятия свойства реализации возможностей, которая является важным моментом при исследовании логик
В разделе 2.2 представлено решение проблемы разрешимости по допустимости для логик Данные логики не обладают свойством ветвления ниже к ни для какого к, наличие которого является одним
из условий в алгоритмическом критерии допустимости правил вывода (см. [27], теорема 3.5.2). Однако исследование логики ^ можно свести к работе над логикой 54.2, которая обладает свойством ветвления ниже 1 и к которой применим алгоритмический критерий допустимости правил вывода (см. [27], теорема 3.5.2). Пользуясь вышеуказанным свойством логики (12> в данном разделе разработан алгоритмический критерий распознавания допустимости правил вывода в модальных логиках Ц2 и № ® Сгг. И ввиду известной связи между модальными и суперинтуиционистскими логиками (см. [27], теорема 3.2.2) получено решение проблемы разрешимости по допустимости для суперинтуиционистской логики
Основными результатами данного раздела являются следующие теорема и ее следствие:
Теорема 2.2. Модальные логики цъ, ^2®разрешимы относительно допустимости правил вывода.
Следствие 2.1. Суперинтуиционистская логика цх, наименьший модальный напарник г^) и наибольший модальный напарник логики ц\ над 54 разрешимы относительно допустимости правил вывода.
В третьей главе приведены результаты исследований проблемы допустимости правил вывода для временной нетранзитивной логики оператором "завтра". Ранее допустимость правила вывода определялась его поведением на верхних слоях специальной п-характеристической модели Крипке [27]. В данной работе свойства правила вывода определяются через его поведение в ограниченной окрестности каждой из точек ^характеристической модели. Эта новая техника используется для доказательства разрешимости по допустимости логики и ряда других свойств данной логики.
В разделе 3.1 определена исследуемая временная нетранзитивная логика с оператором "завтра", введены необходимые определения и обозначения. Приведены результаты, касающиеся связи правила вывода и его редуцированной формы.
Основными результатами раздела 3.2 являются построение п-харак-теристической модели для логики и описание свойств модели
С/»с(п). Определен класс характеристических фреймов для логики С и показано, что логика является финитно-аппроксимируемой и разрешимой.
В разделе 3.3 построен алгоритмический критерий распознавания допустимых правил вывода в логике Основными результатами раздела 3.3 являются
Теорема 3.3. Модальная логика С разрешима относительно допустимости правил вывода.
Теорема 3.4. Логика С не является структурно-полной.
В четвертой главе приведено исследование структурно-полных 54-логик. В разделе 4.1 даются необходимые предварительные сведения о структурно-полных логиках, представлены некоторые общие свойства структурно-полных финитно-аппроксимируемых 54-логик.
В разделе 4.2 получены необходимые и достаточные условия того, что 54-логика Л(-Р) ширины 2, порожденная конечным корневым фреймом без узлов с двухэлементным первым слоем, является структурно-полной. Сгусток С ф го(Л{Р) фрейма F с отношением R будем называть узлом, если Ух Е СУу(х11уУ уНх) и С ф БЬ^). Основным результатом раздела 4.2 является
Теорема 4.1. Логика А(.Р) ширины 2, порожденная конечным корневым фреймом F без узлов таким, что ||571(.Р)|| = 2, является структурно-полной тогда и только тогда, когда F удовлетворяет следующим условиям:
1) сгустки первого слоя являются одноэлементными;
2) конакрытие для двух несравнимых сгустков является одноэлементным;
3) не существует конакрытия для двух несравнимых сгустков из разных слоев;
4) для любого слоя фрейма, отличного от корня, существует конакрытие;
5) все слои, кроме корня, состоят из двух сгустков.
В разделе 4.3 представлены результаты, касающийся ширины структурно-полных табличных 54-логик.
В заключений подведены итоги проведенных исследований, указываются возможности применения разработанных в диссертационной работе методов.
Список литературы
[1] Бабенышев СВ. Разрешимость проблемы допустимости правил вывода в модальных логиках 54.1 и 54.2 и суперинтуиционистской логике КС// Алгебра и логика. — 1992. — Т.31. — № 4. — С. 341-360.
[2] Безгачева Ю.В. Допустимые правила вывода в логиках ширины 2// Международная конференция по модальной логике: Тез. сообщ. Новосибирск, ун-т. — Новосибирск, 1994. — С. 19-21.
[3] Кияткин В.Р. Правила вывода с метапеременными и логические уравнения в предтабличной модальной логике РМ1// Сибирский математический журнал. — 2000. — Т.41. — № 1. — С. 88-97.
[4] Кузнецов А.В. О суперинтуиционистских логиках// Математические исследования. — 1975. — Т.2. — № 10. — С. 150-157.
[5] Минц Г.Е. Допустимые и производные правила// Записки научного семинара ЛОМИ АН СССР. — 1968. — № 8. — С. 189-191.
[6] Минц Г.Е. Производность допустимых правил// Записки научного семинара ЛОМИ АН СССР. — 1972. — № 32. — С. 85-99.
[7] Рыбаков В.В. Критерий допустимости правил в модальной системе S4 и интуиционистской логике// Алгебра и логика. — 1984. — Т.23. — № 5. — С. 369-384.
[8] Рыбаков В.В. Базисы допустимых правил логик 54 и Int// Алгебра и логика. — 1985. — Т.24. — С. 55-68.
[9] Рыбаков В.В. Базисы допустимых правил модальной системы Grz и интуиционистской логики// Математический сборник. — 1985. — Т.128. — № 3. — С. 321-338.
[10] Циткин А.И. О структурной полноте суперинтуиционистских логик//
у Докл. АН СССР. — 1978. — Т.19. — №. 4. — С. 816-819.
[11] Besgacheva U.V. Admissible Rules for the Logic LinTGrz// Bulletin of Section of Logic. — 1997. — V.26. — № 2. — P. 60-67.
[12] Chagrov A., Zakharyaschev M. Modal logics. — Oxford: Oxford University Press. — 1997. — 589 p.
[13] Dziobiak W. Structural Completeness of Modal Logics Containing K4// Bull. Sect. Logic Pol. Acad. Sci. — 1983. — V.12. — № 1. — P. 32-36.
[14] Friedman H. One hundred and two problems in mathematical logic// The Journal of Symbolic Logic. — 1975. — V.40. — № 3. — P. 113-129.
[15] Halpern J., Moses Y. Towards a theory of knowledge and ignorance// Logics and Models of Concurrent Systems. — Springer, Berlin. — 1985. — P. 459-476.
[16] Harrop R. Concerning formulas of the types А —> В V С, А :B(X) in intuitionistic formal systems// The Journal of Symbolic Logic. — 1960. — V.25. — № 1. — p. 27-32.
[17] Iemhoff R. On the admissible rules of intuitionistic propositional logic// Journal of Symbolic Logic. — 2001. — V.66. — № 2. — P. 402-428.
[18] Kripke S.A. Semantic analysis of modal logic// Zeitschrift fur mathematische Logik und Grundlagen der Mathematik. — 1963. — V.9. — P. 67-96.
[19] Kripke S. Semantic analysis of intuitionistic logic// Formal systems and recursive functions. — 1965. — P. 92-130.
[20] Lorenzen P. Einfiing in Operative Logik und Mathmatik. — Berlin -Gottingen - Heidelberg. — 1955. — 412 p.
[21] Maksimova L.L. Intuitionistic logic and implicit definability// Annals of Pure and Applied Logic. — 2000. — 105. — № 1-3. — P. 83-102.
[22] Maksimova L.L. Strongly Decidabile Properties of Modal and Intuitionistic Calculi// Logic Journal of IGPL. — 2000. — V.8. — № 6. — P. 797-819.
[23] Pratt V. Time and Information in Sequental and Concurrent Computation// Intern Workshop TPPP'94. — Sendai. Japan. Lect. Not. in Соmр. Sci. 907. — Springer-Verlag. — 1994. — P. 1-24.
[24] Prucnal T. The Structural Completeness the Medvedev's Logic// Reports on Math. Logic. — 1976. — V.6. — P. 103-105.
[25] Rosenschtein S.I. Formal theories of AI in knowledge and robotics// New General Computing. — 1985. — V.3. — P. 345-357.
[26] Rybakov V.V. Hereditarily Structurally Complete Modal Logics// J. of Symbolic Logic. — 1995. — V.60. — № 1. — P. 266-268.
[27] Rybakov V.V. Admissibility of logical inference rules. — Amsterdam, New-York: Elsevier Publishers. — 1997. — 617 p.
[28] Rybakov V.V. Construction of an explicit basis for rules admissible in modal system 54// Mathematical Logic Quarterly. — 2001. — V.47. — № 4. — P. 441-446.
[29] Tokarz M. On Structural Completeness of Lukasiewicz logics// Selected Papers on Lukasiewicz Sentential Calculi, Wroclow. — 1977. — P. 171176.
[30] Vakarelov D. Modal Logics for Knowledge Representation Systems// Preprint № 7. — Sofia Univ. — 1988. — 29 p.
[31] Wojtylak P. On Structural Completeness of Many-valued Logics// Studia Logica. — 1978. — V.37. — № 2. — P. 139-147.
Работы автора по теме диссертации
[32] Голованова Е.М. Строение шкал, адекватных структурно-полным логикам ширины 2// Материалы XXXVII международной научной студенческой конференции "Студент и научно-технический прогресс". -Новосибирск, 1999. - С. 28-29.
[33] Голованова Е.М. Описание структурно-полных логик глубины не больше 4// Материалы XXXVIII международной научной студенческой конференции "Студент и научно-технический прогресс". - Новосибирск,
2000. - С. 5-6.
[34] Голованова Е.М. Структурно-полные 54-логики малой глубины// "Ломоносовские чтения-2000". Материалы по фундаментальным наукам. -Изд-во МГУ, 2000. - С. 331.
[35] Голованова Е.М. Об одном классе структурно-полных 54-логик ширины 2// Материалы международной конференции "Логика и приложения". -Новосибирск, 2000. - С. 35.
[36] Голованова Е.М. Об одном классе структурно-полных 54-логик// Труды международной конференции "Симметрия и дифференциальные уравнения". - Красноярск, 2000. - С. 76-79.
[37] Голованова Е.М. О разрешимости по допустимости некоторого класса 54-логик, не обладающих свойством ветвления// Материалы XXXIX международной научной студенческой конференции "Студент и научно-технический прогресс". - Новосибирск, 2001. - С. 5-6.
[38] Голованова Е.М. Описание структурно-полных табличных 54-логик ширины 2// Материалы XXXIX международной научной студенческой конференции "Студент и научно-технический прогресс". - Новосибирск, 2001. - С. 6-7.
[39] Голованова Е.М. О разрешимости по допустимости некоторого класса 54-логик// Тезисы международной научной конференции "Молодая наука - XXI веку". - Иваново, 2001. - С. 62.
[40] Голованова Е.М. Описание корневых фреймов без узлов, порождающих структурно-полные табличные 54-логики ширины 2// Тезисы международной научной конференции "Молодая наука- XXI веку".-Иваново,
2001. - С. 63.
[41] Голованова Е.М. О ширине структурно-полных табличных логик// Сборник тезисов докладов "Интеллект - 2001". - Красноярск, 2001. -С. 4-6.
[42] Голованова Е.М. Критерий допустимости правил вывода для некоторого класса S4-логик, не обладающих свойством ветвления// Материалы XXXIV научной студенческой конференции КрасГУ: Сб. ст. Краснояр. гос. ун-т. - Красноярск, 2001. - С. 43-52.
[43] Голованова Е.М. Описание структурно-полных табличных S4-логик ширины 2// Труды XXXIX международной научной студенческой конференции. - Новосибирск, 2001. - С. 217-222.
[44] Голованова Е.М. Разрешимость по допустимости некоторого класса S4-логик, не обладающих свойством ветвления// Труды XXXIX международной научной студенческой конференции "Студент и научно-технический прогресс". - Новосибирск, 2001. - С. 223-228.
[45] Голованова Е.М. О структурно полноте табличных S4-логик// Материалы XL международной научной студенческой конференции "Студент и научно-технический прогресс". - Новосибирск, 2002. - С. 6-7.
[46] Голованова Е.М. Условие структурной полноты табличной S4-логики ширины 2 без узлов// Тезисы докладов международной конференции "Алгебра и ее приложения". - Красноярск, 2002. - С. 38-39.
[47] Голованова Е.М. Строение конечных корневых S4-фреймов ширины 2, порождающих структурно-полные логики// II Всесибирский конгресс женщин-математиков: Сб. ст. Краснояр. гос. ун-т. - Красноярск, 2002. 201 с. - С. 23-26.
[48] Голованова Е.М. Нетранзитивная временная логика дискретного времени// Материалы межрегиональной научно-практической конференции "Молодежь Сибири - Науке России". - Красноярск, 2003. - С. 128-132.
[49] Голованова Е.М. Критерий допустимости правил вывода для некоторого класса 54-логик, не обладающих свойством ветвления// Сиб. мат. журнал. — 2003 — Т.44 — № 4. — С. 726-736.
[50] Golovanov M.I., Rybakov V.V., Yurasova Е.М.// Л necessary condition for rules to be admissible in temporal tomorrow-logic// Bulletin of the sction of Logic. — 2003 — V.32 — № 4. — P.213-220.
[51] Голованов М.И., Юрасова Е.М. Допустимость правил вывода во временной нетранзитивной логике// Материалы международной конференции "Алгебра, логика и кибернетика". - Иркутск, 2004. - С. 134-136.
[52] Юрасова Е.М. Условие допустимости правил вывода во временной логике с дополнительным оператором "Завтра"// Материалы международной конференции "Алгебра, логика и кибернетика". - Иркутск, 2004. -С. 221-222.
[53] Голованов М.И., Юрасова Е.М. Критерий допустимости правил вывода логики с оператором "Завтра"// Красноярск, Крага. университет, 2004, Деп. в ВИНИТИ — 22.10.04. — № 1654-В2004.
Подписано в печать Ц И 01 Бумага типографская Усл. печ л. 1
Тираж 100 экз Заказ №306'.
Формат 60 х 86/16 Печать офсетная Уч.-изд. л. 1,1 Цена договорная.
Редакционно-издательский центр Красноярского государственного университета 660041, Красноярск, пр Свободный, 79
Р256 04
ВВЕДЕНИЕ
1 ПРЕДВАРИТЕЛЬНЫЕ СВЕДЕНИЯ О ДОПУСТИМЫХ ПРАВИЛАХ ВЫВОДА В НЕСТАНДАРТНЫХ ЛОГИКАХ
1.1 Модальные, временные и суперинтуиционистские логики
1.2 Семантика Крипке.
1.3 Допустимые и выводимые правила вывода.
2 ДОПУСТИМОСТЬ ПРАВИЛ ВЫВОДА ДЛЯ НЕКОТОРОГО КЛАССА 54-ЛОГИК, НЕ ОБЛАДАЮЩИХ СВОЙСТВОМ ВЕТВЛЕНИЯ
2.1 Предварительные сведения.
2.2 Алгоритмический критерий допустимости правил вывода для некоторого класса .94-логик, не обладающих свойством ветвления.
3 ДОПУСТИМОСТЬ ПРАВИЛ ВЫВОДА ДЛЯ ЛОГИКИ £ С ОПЕРАТОРОМ "ЗАВТРА"
3.1 Предварительные сведения.
3.2 Свойства логики С.
3.3 Условие допустимости правил вывода в логике С.
4 СТРУКТУРНО-ПОЛНЫЕ 54-ЛОГИКИ
4.1 Структурно-полные 54-логики: необходимые предварительные сведения
4.2 Описание структурно-полных 54-логик ширины 2, порожденных конечным корневым фреймом с двухэлементным первым слоем.
4.3 О ширине структурно-полных табличных 54-логик.
Актуальность темы. Теория нестандартных систем логического вывода сформировалась в начале двадцатых-тридцатых годов 20-го века в работах Лукасе-вича, Льюиса, Геделя и Тарского, как результат анализа поведения аксиоматических систем оснований математики и парадоксов материальной импликации. Однако нестандартные логики по сравнению с классической логикой, отличаются большим разнообразием синтаксиса и семантики. Поэтому к концу 20-го века возникло много новых направлений исследований, связанных с применением идей и методов нестандартной логики в программировании, информатике, теории искусственного интеллекта, представлении знаний и других областях знаний (см., например, [40, 41, 54, 80, 83, 99]).
Большое влияние на становление теории нестандартных систем логического вывода оказано классической теорией доказательств, одним из центральных моментов которой являются правила вывода, поскольку от них зависит эффективность доказательств. Первыми работами, непосредственно посвященными изучению правил вывода, были работы Лося (1955), Тарского (1956) и Сушко (1958). При исследовании правил вывода естественно возник вопрос о том какие правила можно присоединять к логическим системам, сохраняя при этом множество доказуемых теорем системы. Такой класс правил, получивших название допустимых правил вывода, был определен П. Лоренценом [71] в 1955 году. Оказалось, что это в точности допустимые правила вывода - правила, относительно которых данная логика замкнута. Несколько ранее проблема допустимых правил вывода для интуиционистской логики изучалась II.С. Новиковым, который наряду с понятием производного правила вывода (допустимого правила вывода) рассматривал понятие сильного производного правила вывода. В работе [16] Новиков затронул дедуктивные аспекты производных правил вывода в интуиционистской логике. Вслед за Лоренценом и Новиковым изучением допустимых правил вывода занимался С.10. Маслов [11, 12, 13], им исследовалась возможность применения выводимых и допустимых правил вывода в различных сферах деятельности.
В нестандартных логиках, как правило, класс допустимых правил вывода шире класса выводимых правил вывода. Примеры допустимых, но не выводимых правил вывода, были получены Р. Харропом [55], Г.Е. Минцем [14, 15]. Логика, в которой множества допустимых и выводимых правил вывода совпадают, называется структурно-полной. В настоящее время известно, что большинство базисных логик, например, Я, А'4, 54, S5 и др., не являются структурно-полными. Структурная полнота не является инвариантом заданной логики, она зависит от выбора аксиоматической системы. Однако, во многих распространенных классах логик правила вывода обычно фиксированы и выбор аксиоматической системы зависит от изменения множества аксиом. Для таких классов логик имеет смысл понятие структурной полноты. Поэтому исследования, касающиеся структурной полноты, представляют интерес для многих ученых. Токарз установил структурную полноту некоторых логик Лукасевича [97], Прукнал доказал структурную полноту логики Медведева конечных задач [82], Войтыляк показал, что конечные классы многозначных логик являются структурно-полными [103]. Дзиобяк нашел полное описание локально конечных структурно-полных модальных логик, расширяющих К4 [46]. В [29] Циткину удалось описать все наследственно структурно-полные суперинтуиционистские логики, т.е. логики, всякое расширение которых является структурно-полным. Позже Рыбаковым было получено полное описание наследственно структурно-полных модальных логик над КА [89]. А, именно, модальная логика А является наследственно структурно-полной тогда и только тогда, когда А не содержится ни в одной из двадцати специальных табличных логик. Однако уже для структурно-полных бЧ-логик малой глубины (меньше 5) класс структурно-полных логик шире класса наследственно структурно-полных логик. Поэтому особый интерес представляет описание классов структурно-полных логик над SA, К А.
После того как выяснилось, что для большинства нестандартных логик класс допустимых правил шире класса выводимых правил возникли вопросы алгоритмической разрешимости задачи распознавания допустимых правил вывода. Проблема нахождения алгоритма, распознающего допустимость правил вывода в интуиционистской логике была сформулирована в обзоре проблем X. Фридмана [50], родственная проблема существования конечного базиса для допустимых правил этой логики была поставлена А.В. Кузнецовым (см. [50] (проблема 42), [9]). Положительное решение проблемы Кузнецова давало бы и положительное решение проблемы Фридмана. Проблема алгоритмического распознавания допустимости в интуиционистской логике была решена положительно Рыбаковым [18], после чего вопрос о существовании конечного базиса был решен отрицательно так же Рыбаковым [19, 20]. Естественно возник вопрос построения бесконечного базиса, который позже был построен Ием-хофф для интуиционистской логики [59]. Затем Рыбаков построил, также бесконечный, базис для логики 54 [91]. Развивая методы, использованные для решения проблемы допустимости для интуиционистской логики, В.В.Рыбаков доказал разрешимость проблемы допустимости правил вывода в таких важных логиках, как QL, Grz, SA, К А и в некоторых других логиках [21]-[28], [84]—[88]. В частности, была доказана разрешимость проблемы допустимости правил вывода во всех расширениях логики S"4.3, что является обобщением результата Файна [48] о разрешимости данных логик. На основе техники, разработанной В.В. Рыбаковым, проблема допустимости была решена для различных индивидуальных транзитивных логик (см. например [1, 2, 37, 5]).
При решении данных вопросов основным инструментом являлась реляционная семантика (или семантика Крипке, [64, 65]), причем ключевым моментом были специальные модели Крипке - n-характеристические модели. Так, разрешимость проблемы допустимости в логике эквивалентна разрешимости квазиэквациональной теории свободных алгебр многообразия, порожденного этой логикой. С помощью техники, позволяющей представить свободные алгебры из многообразия модальных алгебр «-характеристическими моделями, была решена проблема распознавания допустимых правил вывода для широкого класса модальных транзитивных логик. Отметим, что описание свободных модальных и псевдобулевых алгебр для многообразий модальных и псевдобулевых алгебр, соответствующих индивидуальным логикам, является распространенной задачей при исследовании нестандартных логик (см. [3, 17, 18, 31, 34, 35]). Особую важность представляло описание свободных алгебр не для индивидуальных многообразий, а для всех многообразий финитно-, аппроксимируемых транзитивных логик, которое и было дано Рыбаковым в [90].
Ранее было отмечено, что ценность допустимых правил вывода заключается в том, что такие правила позволяют нам сократить и упростить выводы в дедуктивной системе заданной логики. Другой причиной, по которой изучаются данные правила вывода, являются различные приложения. Так, в работе JI.JI. Максимовой [74] приведено исследование свойств строгой разрешимости модальных и интуиционистских исчислений, рассмотрена проблема строгой разрешимости проективного свойства
Бета над интуиционистским пропозициональным исчислением. Для доказательства строгой разрешимости проективного свойства Бета над интуиционистским пропозициональным исчислением достаточно решить проблему разрешимости по допустимости суперинтуиционистских логик с таким свойством. Максимовой [73] было показано, что существует точно 16 суперинтуиционистских логик, обладающих проективным свойством Бета. Из результатов В.В. Рыбакова [90] следует разрешимость проблемы допустимости для всех логик с таким свойством, кроме логик под номером 9, 13, 15 из полного списка логик с проективным свойством Бета [74]. Несмотря на то, что Рыбаков получил достаточно общий критерий допустимости правил вывода для финитно-аппроксимируемых логик [90], данный критерий не является универсальным, поскольку одним из условий является наличие свойства ветвления ниже к. Так, логика, указанная под номером 9 в полном списке логик с проективным свойством Бета, не обладает свойством ветвления ниже к ни для какого к.' Решение проблемы распознавания допустимых правил вывода в данной логике представлено в настоящей диссертационной работе. Также с работой Л.Л.Максимовой [74] связано исследование логики S40a/v, не обладающей свойством ветвления, на разрешимость по допустимости правил вывода. Данная задача была решена в [93] и позволила обосновать предположение о строгой разрешимости интерполяционного свойства над логикой S4, которое было выдвинуто в статье Л.Л.Максимовой [74].
Несмотря на глубокую разработку направления допустимых правил вывода, большинство результатов было получено для транзитивных логик. В настоящее время особый интерес представляют нетранзитивные логики, так как основные результаты и техники, использующиеся для исследования допустимых правил вывода в транзитивных логиках, применять непосредственно при изучении допустимых правил вывода в нетранзитивных логиках не удаётся. Как было отмечено, при исследовании допустимых правил вывода центральную роль играют n-характеристические модели Крипке: для всякого правила вывода в модальной логике существует конечное, с точностью до изоморфизма, множество n-характеристических моделей Крипке, на элементах которого можно проверять истинность правила, для выяснения его допустимости. Однако при построении n-характеристической модели возникает немало вопросов. На самом деле, построение n-характеристической модели является достаточно ясным только для расширений модальной логики К4 и интуиционистской логики. В случае нетранзитивной логики данные модели описаны только для очень малого списка логик, в частности, для К (см., например, [42]). В случае нетранзитивных временных логик описание упомянутых выше моделей представляется еще более сложной задачей. Цель работы.
1. Исследовать на разрешимость по допустимости правил вывода суперинтуиционистскую логику, порожденную классом всех конечных корневых фреймов F, удовлетворяющих условию xRyk^{yRx)kyRzkyRu) -л Sv(zRvkuRv), где R - отношение на фрейме F. Положительное решение данной задачи позволяет обосновать предположение о строгой разрешимости проективного свойства Бета над логикой ц 1} которое было выдвинуто в статье JI.JI. Максимовой [74].
2. Исследовать на разрешимость по допустимости логику с оператором "завтра".
3. Получить описание конечных корневых ^-фреймов ширины 2, порождающих структурно-полные логики.
Методика исследования. В исследовании применяются общие методы теоретико-модельной и алгебраической семантики для пропозициональных нестандартных логик. Например, метод фильтрации, метод канонических моделей, метод редуцирования правил вывода. А также в исследовании использованы алгоритмический и семантический критерии допустимости правил вывода, критерий структурной полноты логики, некоторые результаты теории модальных напарников суперинтуиционистских логик.
Научная новизна. Все результаты, полученные в диссертации, являются новыми и снабжены подробными доказательствами. Результаты совместных работ получены в нераздельном соавторстве.
Основные результаты. В диссертации получены следующие основные результаты.
1. Получен алгоритмический критерий распознавания допустимых правил вывода для ^-логики порожденной классом всех конечных корневых фреймов F, удовлетворяющих условию xRy&-^(yRx)kyRz&yRu) -» 3v(zRvbuRv), где R - отношение на фрейме F.
2. Доказано, что логика © Grz и суперинтуиционистская логика, порожденная классом всех конечных корневых фреймов F, удовлетворяющих условию xRy&-i(yRx)kyRz&,yRu) -у 3v(zRvkuRv), где R - отношение на фрейме F, разрешима относительно допустимости правил вывода.
3. Получен алгоритмический критерий распознавания допустимых правил вывода для логики с оператором "завтра".
4. Получены необходимые и достаточные условия того, что 54-логика A(F) ширины 2, порожденная конечным корневым фреймом без узлов с двухэлементным первым слоем, является структурно-полной.
Теоретическая и практическая ценность. Все полученные результаты носят теоретический характер и могут быть использованы в дальнейших исследованиях допустимых правил вывода в нестандартных логиках, а также в таких областях как теория моделей, теория графов и computer science. Апробация работы. Результаты диссертации докладывались на
• XXXVII-международной научной студенческой конференции "Студент и научно-технический прогресс"(Новосибирск, 1999),
• XXXVIII-международной научной студенческой конференции "Студент и научно-технический прогресс" (Новосибирск,2000),
• XXXIX-международной научной студенческой конференции "Студент и научно-технический прогресс"(Новосибирск,2001),
• XL-международной научной студенческой конференции "Студент и научно-технический прогресс" (Новосибирск, 2002),
• международной конференции "Ломоносовские чтения" (Москва, 2000),
• международной конференции "Логика и приложения", посвященной 60-летию со дня рождения Ю.Л. Ершова (Новосибирск, 2000),
• международной конференции "Дифференциальные уравнения и симметрия" (Красноярск, 2000),
• международной научной конференции "Молодая наука - XXI веку" (Иваново, 2001),
• II Всесибирском конгрессе, посвященному Софьи Ковалевской (Красноярск, 2002),
• международной конференции "Алгебра и ее приложения", посвященной 70-летию со дня рождения В.П.Шункова и 65-летию В.М.Бусаркина(Красноярск, 2002),
• международной конференции "Мальцевские чтения" (Новосибирск, 2003),
• международной конференции "Алгебра, логика и кибернетика", посвященной 75-летию со дня рождения А.И.Кокорина (Иркутск, 2004).
Публикации. По теме диссертации опубликовано 22 работы [104]—[125]. Структура и объём работы. Диссертация состоит из введения, четырех глав, заключения и библиографического списка, включающего 103 наименования. Объём работы 103 страницы машинописного текста. Обзор содержания диссертации и полученных результатов.
ЗАКЛЮЧЕНИЕ
В главе 2 диссертационной работы рассмотрена модальная финитно-аппроксимируемая 54-логика /л2, порожденная классом всех конечных корневых фреймов F, удовлетворяющих условию (xRyk-i(yRx)kyRzkyRu) 3v(zRvkuRv), где R - отношение на фрейме F. Для логик ц2, ц2 0 Grz получен алгоритмический критерий распознавания допустимых правил вывода (леммы 2.2, 2.3, теорема 2.2). Отсюда, ввиду известной связи между модальными и суперинтуиционистскими логиками (теорема 3.2.2 [90]), следует разрешимость по допустимости правил вывода суперинтуиционистской логики порожденной классом всех конечных корневых фреймов F, удовлетворяющих условию (xRyk-^(yRx)kyRzkyRu) —> 3v(zRvkuRv), где R - отношение на фрейме F (следствие 2.1). Вышеуказанные логики не обладают свойством ветвления ниже к ни для какого к. Построение алгоритма, распознающего допустимые правила вывода логик fix, fi2, ц2 0 Grz, дает дополнительную методику решения аналогичных проблем. Кроме того решение данной задачи позволяет обосновать предположение о строгой разрешимости проективного свойства Бета над логикой /л 1, которое было выдвинуто в статье JI.JI. Максимовой [74].
В главе 3 получен алгоритмический критерий распознавания допустимых правил вывода для нетранзитивной логики С с оператором "завтра" (теоремы 3.1, 3.2, З'.З). Показано, что данная логика не является структурно-полной (теорема 3.4). Поскольку С является нетранзитивной логикой, то для исследования допустимых правил вывода в С потребовалось развитие новой техники. Представленная техника может быть использована в дальнейших исследованиях допустимых правил вывода в нетранзитивных логиках.
В главе 4 получены необходимые и достаточные условия того, что ^-логика
A(F) ширины 2, порожденная конечным корневым фреймом F без узлов с двухэлементным первым слоем, является структурно-полной (теорема 4.1). Если говорить о структурно-полных ^-логиках, порожденных конечным корневым фреймом F без узлов с одноэлементным первым слоем, то классы фреймов для указанных логик будут шире чем в предыдущем случае, и по вычислительным причинам описание для таких логик не приводятся.
Полученные в диссертации результаты могут быть использованы в дальнейших исследованиях допустимых правил вывода в нестандартных логиках. Кроме того исследования по computer science активно используют инструменты неклассических логик, поэтому полученные в диссертации результаты помимо чисто математических приложений, могут иметь применение также при разработке теории искусственного интеллекта и computer science.
1. Бабенышев С.В. Разрешимость проблемы допустимости правил вывода в модальных логиках S4.1 и 54.2 и суперинтуиционистской логике КС 1.j Алгебра и логика. — 1992. — Т. 31. — № 4. — С. 341-360.
2. Безгачева Ю.В. Допустимые правила вывода в логиках ширины 2// Международная конференция по модальной логике: Тез. сообщ. Новосибирск, ун-т. — Новосибирск, 1994. — С.19-21.
3. Григолия Р.Ш. Свободные 54.3-алгебры конечного ранга// Исследования неклассических логик и формальных теорий. — М.: Наука. — 1983. — С. 281-286.
4. Захарьящев М.В. Синтаксис и семантика суперинтуиционистских логик// Алгебра и логика. — 1989. — Т.28. — № 4. — С. 402-429.
5. Кияткин В.Р. Правила вывода с метапеременными и логические уравнения в предтабличной модальной логике РМ1// Сибирский математический журнал. — 2000. — Т.41. — Ко 1. — С. 88-97.
6. Крипке С.А. Семантический анализ модальной логики. I. Нормальные модальные исчисления высказываний// Модальная логика. — М.: Наука, 1974. — С. 254-303.
7. Крипке С.А. Семантический анализ модальной логики. II. Ненормальные модальные исчисления высказываний// Модальная логика. — М.: Наука, 1974. — С. 304-323.
8. Крипке С.А. Теорема полноты в модальной логике // Модальная логика. — М.: Наука, 1974. — С. 223-246.
9. Кузнецов А.В. О суперинтуиционистских логиках// Математические исследования. — 1975. — Т.2. — № 10. — С. 150-157.
10. Максимова JI.JI., Рыбаков В.В. О решётке нормальных модальных логик// Алгебра и логика. — 1974. — Т.13. — № 2. — С. 105-122.
11. Маслов C.IO. О поиске вывода в исчислениях общего типа// Зап. научных семинаров ЛОМИ АН СССР. — 1972. — Т.32. — С. 59-65.
12. Маслов С.Ю. Теория поиска вывода и некоторые ее применения// Кибернетика. — 1975. — № 4. — С. 134-144.
13. Маслов С.Ю. Теория дедуктивных систем и ее применения. — М.: Радио и связь — 1986.
14. Минц Г.Е. Допустимые и производные правила// Записки научного семинара ЛОМИ АН СССР. — 1968. — № 8. — С. 189-191.
15. Минц Г.Е. Производность допустимых правил// Записки научного семинара ЛОМИ АН СССР. — 1972. — № 32. — С. 85-99.
16. Новиков П.С. Конструктивная математическая логика с точки зрения классической. — М.: Наука, 1977.
17. Рыбаков В.В. Допустимые правила предтабличных модальных логик// Алгебра и логика. — 1981. — Т.20. — № 4. — С. 440-464.
18. Рыбаков В.В. Критерий допустимости правил в модальной системе SA и интуиционистской логике// Алгебра и логика. — 1984. — Т.23 — № 5. — С. 369384.
19. Рыбаков В.В. Базисы допустимых правил логик 54 и Intf/ Алгебра и логика. — 1985. — Т.24. — С. 55-68.
20. Рыбаков В.В. Базисы допустимых правил модальной системы Grz и интуиционистской логики// Математический сборник. — 1985. — Т.128 — № 3. — С. 321-338.
21. Рыбаков В.В. Универсальные теории свободных А-алгебр при А Э S4.3// Слож-ностные проблемы математической логики. — Калинин. — 1985. — С. 72-75.
22. Рыбаков В.В. Алгебраические методы в пропозициональной логике// Семиотика и информатика. — 1986. — № 28. — С. 102-121.
23. Рыбаков В.В. Уравнения в свободной топобулевой алгебре// Алгебра и логика. — 1986. — Т.25. — № 2. — С. 172-204.
24. Рыбаков В.В. Уравнения в свободной топобулевой алгебре и проблема подстановки// Доклады АН СССР. — 1986. — Т.287. — № 3. — С. 554-557.
25. Рыбаков В.В. Базисы допустимых правил модальных систем Grz и интуиционистской логики// Математический сборник. — 1987. — Т.56. — № 2. — С. 311-331.
26. Рыбаков В.В. Разрешимость по допустимости модальной системы Grz и интуиционистской логики// Известия АН СССР: Сер. математическая. — 1986; — Т.50. — № 3. — С. 598-616.
27. Рыбаков В.В. Допустимость правил вывода и логические уравнения в модальных логиках, аксиоматизирующих доказуемость// Известия АН СССР. — 1990. — Ко 3. — С. 357-377.
28. Рыбаков В.В. Критерии допустимости правил вывода с параметрами в интуиционистской пропозициональной логике// Известия АН СССР. Сер. математическая. — 1990. — Т.54. — № 6. — С. 693-703.
29. Циткин А.И. О структурной полноте суперинтуиционистских логик// Докл. АН СССР. — 1978. — Т.19. — №.4. — С. 816-819.
30. Шехтман В.Б. О неполных пропозициональных логиках// Доклады АН СССР. — 1977. — Т.235. — № 3. — С. 542-545.
31. Шехтман В.Б. Лестницы Ригера-Нишимуры// Доклады АН СССР. — 1978. — Т.241. — № 6. — С. 1288-1291.
32. Barringer Н., Fisher М., Gabbay D., Gough G. Advances in temporal logic// Kluwer Academic Publishers. Dordrecht. — December 1999. — V. 16 of Applied logic series.
33. Beeson M. Foundation of Constructive Mathematics. Mathematical Studies. — Berlin, Springer-Verlag. — 1985.
34. Bellisssima F. Finitely generated free Heyting algebras// Journal of Symbolic Logics. — 1986. — V.51. — № 1. — P. 152-165.
35. Bellisssima F. Atoms of Tense Algebras// Algebra Univarsalis. — 1991. —V.28. — P. 52-78.
36. Belnap N.D., Leblanc H., Thomason R.H. On not strengthening intuitionistic logic// Notre Dame J. of Formal Logic. — 1963. — V.4 — P. 313-320.
37. Besgacheva U.V. Admissible Rules for the Logic LinTGrz// Bulletin of Section of Logic. — 1997. — V.26. — № 2. — P. 60-67.
38. Blok W.J. On the degree of incompleteness in modal logics and the covering relation in the lattice of modal logics// Technical Reports 78-07. Department of Mathematics, University of Amsterdam. — 1978.
39. Boolos G. On systems of modal logic with provability interpretations// Theoria. — 1980. — V.46. — P. 7-18.
40. Bose S., Fisher A. Verifying pipelined hardware using symbolic logic simulation// Information and Computation. — 1992. — V.98. — № 2. — P. 378-400.
41. Burch J.R., Clarke E.M., Dill D.L.,Hwang J, McMillan K.L. Symbolic model checking: Ю20 states and beyond. Format theories of AI in knowledge and robotics// Proc. 5th IEEE Symposium on logic in Computer Science. — 1990. — P. 428-439.
42. Chagrov A., Zakharyaschev M. Modal logics. — Oxford: Oxford University Press. — 1997. — 589 p.
43. Church A. Introduction to mathematical logic. Part I. — Princeton University Press. — 1956.
44. Dummett M. Elements of Intuitionism. — Clarendon Press, Oxford. — 1977.
45. Dummett M.A., Lemmon E.J. Modal logics between 54 and 55// Z. fur Mathematical Logic und Grundl. der Mathematik. — 1959. — V.5. — P. 250264.
46. Dziobiak W. Structural Completeness of Modal Logics Containing К4// Bull. Sect. Logic Pol. Acad. Sci. — 1983. — V.12. — M> 1. — p. 32-36.
47. Emerson E.A. Temporland and Modal Logics// In Handbook of theoretical Computer Science./Ed. J. van Ieewen; — Elsevier Science Publishers, the Netherland. — 1990. — P. 996-1072.
48. Fine K. The logics containing 54.3// Z. fur Mathematical Logic und Grundl. der Mathematik. — 1971. — V.17. — P. 371-376.
49. Fine K. An incomplete logic containing 54// Theoria. — 1974. — V.40. — P. 2329.
50. Friedman II. One hundred and two problems in mathematical logic// The Journal of Symbolic Logic. — 1975. — V.40. — № 3. — P. 113-129.
51. Gabbay D.M., Guenthner F., editors. Handbook of Philosophical logic. — Reidel, Dordrecht. — 1984.
52. Gabbay D., Kurucz A., Wolter F., Zakharyaschev M. Many-dimensional modal logics: theory and applications (to appear).
53. Godel K. Eine Interpretation des Intuitionistischen Aussagenkalkiils// Ergebnisse eines mathematischen Kolloquiums. — 1933. — V.4. — P. 39-40.
54. Halpern J., Moses Y. Towards a theory of knowledge and ignorance// Logics and Models of Concurrent Systems. — Springer, Berlin. — 1985. — P. 459-476.
55. Harrop R. Concerning formulas of the types A —>• В V С, A —> 3xB(x) in intuitionistic formal systems// The Journal of Symbolic Logic. — 1960. — V.25. — № 1. — P. 27-32.
56. Heyting A. Die formalen Regeln der intuitionistischen Logik// Sitzungsberichte der preussischen Akademie von Wissenschaften. — 1930. — P. 42-56.
57. Hoek W., Woldridge M. Model Cheking knowledge and time// In SPIN 2002, Proc. of the Ninth International SPIN Workshop on Model Cheking of Software. — Genoble, France. — 2002.
58. Hughes G.E., Cresswell M.J. A new Introduction to Modal Logic. — Methuem, London. — 1996.
59. Iemhoff R. On the admissible rules of intuitionistic propositional logic// Journal of Symbolic Logic. — 2001. — V.66. — № 2. — P. 402-428.
60. Jonsson В., Tarski A. Boolean algebras with operators. Part I// American Journal of Mathematics. — 1951. — V.73. — P. 891-939.
61. Jonsson В., Tarski A. Boolean algebras with operators. Part II // American Journal of Mathematics. — 1952. — V.74. — P. 127-162.
62. Kleene S. Mathematical logic. — Jon Wiley & Sons, Inc., New York. — 1967.
63. Kripke S.A. A completeness theorem in modal logic// Journal of Symbolic Logic. — 1959. — V.24. — P. 1-14.
64. Kripke S.A. Semantic analysis of modal logic // Zeitschrift fur mathematische Logik und Grundlagen der Mathematik. — 1963. — V.9. — P. 67-96.
65. Kripke S. Semantic analysis of intuitionistic logic// Formal systems and recursive functions. — 1965. — P. 92-130.
66. Lemmon E.J. Algebraic semantics for modal logics. Part I// Journal of Symbolic Logic. — 1966. — V.31. — P. 46-64.
67. Lemmon E.J. Algebraic semantics for modal logics. Part II// Journal of Symbolic Logic. — 1966. — V.31. — P. 191-218.
68. Lemmon E.J., Scott D.S. An introduction to modal logic. — Oxford, Blackwell. — 1977.
69. Lewis C. A survey of symbolic logic. — University of California Press, Berkeley. — 1918.
70. Lewis C., Langford C. Symbolic Logic. — Appleton-Century-Crofts, New York. — 1932.
71. Lorenzen P. Einfiing in Operative Logik und Mathmatik. — Berlin Gottingen -Heidelberg. — 1955. — 412 p.
72. Makinson D. On some completeness theorem in modal logic// Zeitschrift fur mathematische Logik und Grundlagen der Mathematik. — 1966. — V.12. — P. 376-394.
73. Maksimova L.L. Intuitionistic logic and implicit definability// Annals of Pure and Applied Logic. — 2000. — V.105. — № 1-3. — P. 83-102.
74. Maksimova L.L. Strongly Decidabile Properties of Modal and Intuitionistic Calculi// Logic Journal of IGPL. — 2000. — V.8. — № 6. — P. 797-819.
75. Manna Z., Pnueli A. The temporal Logic of Reactive and Concurrent Systems. — Springer-Verlag. — 1992.
76. Manna Z., Pnueli A. Temporal Verification of Reactive Systems: Safety. — Springer-Verlag. — 1995.
77. McKinsey J. On syntactical construction of systems of modal logic// Journal of symbolic logic. — 1945. — V.10. — P. 83-94.
78. McKinsey J., Tarski A. Some theorems about the sentential calculi of Lewis and Heyting// Journal of symbolic logic. — 1948. — V.13. — P. 1-15.
79. Mendelson E. Introduction to mathematical logic. — Van Nostrand, New York. — 1984.
80. Pratt V. Time and Information in Sequental and Concurrent Computation// Intern Workshop TPPP'94. — Sendai. Japan. Lect. Not. in Сотр. Sci. 907, — Springer-Verlag. — 1994. — P. 1-24.
81. Prior A. Past, Present and Future. — Oxford University Press. — 1967.
82. Prucnal T. The Structural Completeness the Medvedev's Logic// Reports on Math. Logic. — 1976. — V.6. — P. 103-105.
83. Rosenschtein S.I. Formal theories of AI in knowledge and robotics// New General Computing. — 1985. — V.3. — P. 345-357.
84. Rybakov V.V. Logical Equations and Admissible Rules of Inference with Parameters in Modal Provability Logics// Studia Logica. — 1990. — V.49. — № 2. — P. 215-239.
85. Rybakov V.V. Problems of substitution and admissibility in the modal system Grz and intuitionistic calculus// Annals of Pure and Applied Logic. — 1990. — V.50. — P. 71-106.
86. Rybakov V.V. Rules of inference with parameters for intuitionistic logic// Journal of Symbolic Logic. — 1992. — V.57. — № 3. — P. 912-923.
87. Rybakov V.V. Criteria for admissibility of inference rules. Modal and intermediate logics with the branching property// Studia Logica. — 1994. — V.53. — № 2. — P. 203-225.
88. Rybakov V.V. Hereditarily Structurally Complete Modal Logics// J. of Symbolic Logic. — 1995. — V.60. — № 1. — P. 266-268.
89. Rybakov V.V. Admissibility of logical inference rules. — Amsterdam, New-York: Elsevier Publishers. — 1997. -— 617 p.
90. Rybakov V.V. Construction of an explicit basis for rules admissible in modal system 54// Mathematical Logic Quarterly. — 2001. — V.47. — № 4. — P. 441446.
91. Rybakov V.V. Inference in temporal next-time logic (to appear)
92. Rutskiy A.N. Decidability of Modal Logics 54 ф aN, 54 ф £N+i w.r.t. Admissible Inference Rules// Bulletin of the Section of Logic. — 2001. — V.30. — №. 4. — P.181-189.
93. Segerberg K. An essay in classical modal logic// Filosofiska Studier, Mimeograph. — 1971. — V. 1-3.
94. Takeuti G. Proof theory. — North Holland, Amsterdam. — 1975.
95. Thomason S. An incompleteness theorem in modal logic// Theoria. — 1974. — V.40. — P. 30-34.
96. Tokarz M. On Structural Completeness of Lukasiewicz logics// Selected Papers on Lukasiewicz Sentential Calculi. — Wroclow. —- 1977. — P. 171-176.
97. Troelstra A. Principles of Intuitionism. Lecture Notes in Mathematics, 95. — Springer-Verlag, Berlin. — 1969.
98. Vakarelov D. Modal Logics for Knowledge Representation Systems// Preprint № 7. — Sofia Univ. — 1988. — 29 p.
99. Wojtylak P. On Structural Completeness of Many-valued Logics// Studia Logica. — 1978. — V.37. — № 2. — P.139-147.
100. РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ
101. Голованова Е.М. Строение шкал, адекватных структурно-полным логикам ширины 2// Материалы XXXVII международной научной студенческой конференции "Студент и научно-технический прогресс". Новосибирск, 1999. -С. 28-29.
102. Голованова Е.М. Описание структурно-полных логик глубины не больше 4// Материалы XXXVIII международной научной студенческой конференции "Студент и научно-технический прогресс". Новосибирск, 2000. - С. 5-6.
103. Голованова Е.М. Структурно-полные 54-логики малой глубины// "Ломоносовские чтения-2000". Материалы по фундаментальным наукам. Изд-во МГУ, 2000. - С. 331.
104. Голованова Е.М. Об одном классе структурно-полных S'4-логик ширины 2// Материалы международной конференции "Логика и приложения". Новосибирск, 2000. - С. 35.
105. Голованова Е.М. Об одном классе структурно-полных 54-логик// Труды международной конференции "Симметрия и дифференциальные уравнения". -Красноярск, 2000. С. 76-79.
106. Голованова Е.М. О разрешимости по допустимости некоторого класса S4-логик, не обладающих свойством ветвления// Материалы XXXIX международной научной студенческой конференции "Студент и научно-технический прогресс". Новосибирск, 2001. - С. 5-6.
107. Голованова Е.М. Описание структурно-полных табличных 5"4-логик ширины 2// Материалы XXXIX международной научной студенческой конференции "Студент и научно-технический прогресс". Новосибирск, 2001. - С. 6-7.
108. Голованова Е.М. О разрешимости по допустимости некоторого класса 54-логик// Тезисы международной научной конференции "Молодая наука XXI веку". - Иваново, 2001. - С. 62.
109. Голованова Е.М. Описание корневых фреймов без узлов, порождающих структурно-полные табличные 54-логики ширины 2// Тезисы международной научной конференции "Молодая наука XXI веку". - Иваново, 2001. -С. 63.
110. Голованова Е.М. О ширине структурно-полных табличных логик// Сборник тезисов докладов "Интеллект 2001". - Красноярск, 2001. - С. 4-6.
111. Голованова Е.М. Критерий допустимости правил вывода для некоторого класса 54-логик, не обладающих свойством ветвления// Материалы XXXIV научной студенческой конференции КрасГУ: Сб. ст. Краснояр. гос. ун-т. Красноярск, 2001. - С. 43-52.
112. Голованова Е.М. Описание структурно-полных табличных 54-логик ширины 2// Труды XXXIX международной научной студенческой конференции. Новосибирск, 2001. - С. 217-222.
113. Голованова Е.М. Разрешимость по допустимости некоторого класса 54-логик, не обладающих свойством ветвления// Труды XXXIX международной научной студенческой конференции "Студент и научно-технический прогресс". -Новосибирск, 2001. С. 223-228.
114. Голованова Е.М. О структурно полноте табличных S4-логик// Материалы XL международной научной студенческой конференции "Студент и научно-технический прогресс". Новосибирск, 2002. - С. 6-7.
115. Голованова Е.М. Условие структурной полноты табличной .94-логики ширины 2 без узлов// Тезисы докладов международной конференции "Алгебра и ее приложения". Красноярск, 2002. - С. 38-39.
116. Голованова Е.М. Строение конечных корневых 54-фреймов ширины 2, порождающих структурно-полные логики// II Всесибирский конгресс женщин-математиков: Сб. ст. Краснояр. гос. ун-т. Красноярск, 2002. 201 с. - С. 23-26.
117. Голованова Е.М. Нетранзитивная временная логика дискретного времени// Материалы межрегиональной научно-практической конференции "Молодежь Сибири Науке России". - Красноярск, 2003. - С. 128-132.
118. Голованова Е.М. Критерий допустимости правил вывода для некоторого класса 5*4-логик, не обладающих свойством ветвления// Сиб. мат. журнал. — 2003 — Т.44 — № 4. — С. 726-736.
119. Golovanov M.I., Rybakov V.V., Yurasova Е.М.// A necessary condition for rules to be admissible in temporal tomorrow-logic// Bulletin of the sction of Logic. — 2003 — V.32 — № 4. — P.213-220.
120. Голованов М.И., Юрасова Е.М. Допустимость правил вывода во временной нетранзитивной логике// Материалы международной конференции "Алгебра, логика и кибернетика". Иркутск, 2004. - С. 134-136.
121. Юрасова Е.М. Условие допустимости правил вывода во временной логике с дополнительным оператором "Завтра"// Материалы международной конфегренции "Алгебра, логика и кибернетика". Иркутск, 2004. - С. 221-222.
122. Голованов М.И., Юрасова Е.М. Критерий допустимости правил вывода логики с оператором "Завтра"// Красноярск, Краен, университет, 2004, Деп. в ВИНИТИ — 22.10.04. — № 1654-В2004.
