Исследование допустимых правил вывода в нестандартных суперинтуиционистских и модальных транзитивных логиках тема диссертации и автореферата по ВАК РФ 01.01.06, кандидат физико-математических наук Руцкий, Алексей Николаевич

• Руцкий, Алексей Николаевич
• кандидат физико-математических наук
• 2002

Оглавление диссертации кандидат физико-математических наук Руцкий, Алексей Николаевич

ВВЕДЕНИЕ

1 СЕМАНТИЧЕСКИЕ МЕТОДЫ В ИССЛЕДОВАНИЯХ ДОПУСТИМЫХ ПРАВИЛ ВЫВОДА

1.1 Синтаксис модальных и суперинтуиционистских: логик.

1.2 Строение моделей Крипке.

1.3 Алгебраическая семантика для модальных и суперинтуиционистских логик

1.4 Применение п-характеристических моделей Крипке в исследованиях допустимых правил вывода.

1.5 Связь между суперинтуиционистскими и модальными логиками.

2 РАЗРЕШИМОСТЬ ПО ДОПУСТИМОСТИ

МОДАЛЬНЫХ ЛОГИК 54®«* и

2.1 Предварительные сведения.

2.2 Алгоритм распознавания допустимых правил вывода модальных логик 54 ф и 54©

2.3 Сохранение допустимости правил вывода при Т-переводе в модельно равномерных по допустимости логиках.

3 НАСЛЕДОВАНИЕ ДОПУСТИМЫХ ПРАВИЛ ВЫВОДА В ТРАНЗИТИВНЫХ МОДАЛЬНЫХ

И СУПЕРИНТУИЦИОНИСТСКИХ ЛОГИКАХ

3.1 Предварительные сведения.

3.2 Критерий наследования допустимых правил вывода модальной логики К

3.3 Наследование допустимых правил вывода логики КА и табличные модальные логики.

3.4 Признаки наследования допустимых правил вывода для финитно аппроксимируемых транзитивных модальных и суперинтуиционистских логик, мо-дельно равномерных по допустимости.

4 ПОСТРОЕНИЕ ЯВНОГО БАЗИСА ДЛЯ

ДОПУСТИМЫХ ПРАВИЛ ВЫВОДА

МОДАЛЬНОЙ ЛОГИКИ КА

4.1 Предварительные сведения.

4.2 Построение явного базиса для правил вывода, допустимых в модальной логике К

Введение диссертации (часть автореферата) на тему «Исследование допустимых правил вывода в нестандартных суперинтуиционистских и модальных транзитивных логиках»

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

При изучении свойств формальных систем наряду с теоретическими решаются и чисто прикладные задачи. Так, с использованием различных аксиоматических систем, главным образом временных и модальных логик, ведутся исследования по проблемам искусственного интеллекта и Computer Science. Среди направлений, где в последние годы плодотворно ведутся подобные исследования, можно отметить разработку баз данных, сетевые технологии, тестирование процессоров и компьютерных схем, создание самообучающихся систем и исследование различных аспектов программирования [48, 49, 52, 83, 105].

Любая формальная система определяется тремя составляющими: языком этой системы, ее аксиомами и правилами вывода. Задавая аксиоматическую систему, можно формулировать точные и корректные математические утверждения и проводить построение доказательств или опровержений теорем. Аксиоматическая система соответствует единственной пропозициональной логике, формируя с помощью правил вывода этой системы из ее аксиом множество теорем. Однако конкретная пропозициональная логика может соответствовать многим аксиоматическим системам, обладающим различной дедуктивной мощностью. Предпочтение как правило отдается системе, более эффективной для построения доказательств и проверки теорем заданной логики. Уже по своему определению, правила вывода обладают большей, чем аксиомы, дедуктивной мощностью. Поэтому при построении формализации для некоторого логического исчисления, мы можем сначала выбрать среди его теорем некоторое множество аксиом, а затем дополнить его удобными с дедуктивной точки зрения правилами вывода. В качестве таких правил вывода, очевидно, можно использовать только правила, применение которых не расширяет множество теорем этой логики. Такой класс правил, получивших название допустимых правил вывода, был введен П.Лоренценом [75] в 1955 году. Было указано, что каждая логика, вне зависимости от способа своего формального описания, должна обладать уникальным классом всех до пустимых правил вывода. Этот класс правил вывода является инвариантом логического исчисления и представляется наиболее удобным инструментом в теории доказательств.

Основная проблема теории допустимых правил вывода состоит в распознавании допустимости в заданном логическом исчислении произвольного правила вывода г := а\, . ,<*т//?. Если для классического исчисления высказываний проблема решалась элементарной проверкой теоремы b А • • • А ат -» ¡3, то в неклассических логиках ее решение потребовало развития сложной и разнообразной семантической техники. Первоначально эта проблема была сформулирована A.B. Кузнецовым для случая интуиционистской логики [10]. Позднее она была включена Х.Фридманом [60] в обзор современных проблем математической логики.

Исследования допустимых правил вывода первоначально проводились именно для интуиционистских логик как имеющих большое значение в основаниях математики. Еще в 40-х годах П.С.Новиков отмечал в своих лекциях, что класс всех допустимых правил интуиционистского исчисления IPC необходимо отличать от класса всех производных правил вывода IPC. К началу 60-х годов сформировалась развитая алгебраическая семантика для интуиционистских, модальных и временных логик, основа для которой была заложена в работах А.Тарского, Дж.МакКинси, В.Джонсона, Е.Леммона и других [54, 69, 70, 73, 74, 78, 79]. Десятилетие спустя в работах С.Крипке, К.Хинтикка, К.Шютте [6, 7, 8, 9, 43, 72, 96] была разработана семантика моделей Крипке. Этот мощный семантический аппарат быстро нашел свое применение во многих областях математической логики и стал основным инструментом в исследованиях допустимых правил вывода.

Примеры допустимых, но не производных правил вывода для интуиционистской логики и модальной логики Льюиса 54 были получены Р.Харропом [67] в 1960 году и Г.Е.Минцем [16, 17] в 1972 году. Тогда же Г.Е.Минц привел ряд достаточных условий допустимости и производности правил вывода, а также провел исследование структурно полных логик, то есть логик, для которых все допустимые правила являются производными. А.И.Циткин [41] построил в 1977 году базис для допустимых квазихарактеристических правил вывода 1РС. В 1978 году он также привел описание [42] всех структурно предполных интуиционистских логик, то есть логик, каждое расширение которых является структурно полным. В 1981 году Дж.Порт провел исследования допустимых и производных правил вывода модальной логики Льюиса 55 [81]. Используя методы алгебраической семантики, В.В.Рыбаков в 1981 году доказал разрешимость проблемы допустимости для табличных и предтабличных модальных логик [24]. Параллельно с этими исследованиями проводится изучение возможностей характеризации всего отношения выводимости I-. Начиная с 80-х годов исследования допустимых правил вывода ведутся по многим направлениям [55, 71, 89, 106].

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

В 80-90 годы разрешимость по допустимости была доказана для многих известных суперинтуиционистских и модальных логик, в том числе для модальных логик Соловая 5 (см. [104]), Гёделя-Лёба ОЬ, Гжегорчика Огг, Льюиса 5*4 и для модальной транзитивной логики К4 [25, 26, 27, 32, 33, 36, 37, 88, 93, 96]. Исследования разрешимости по допустимости для правил вывода с метапеременными проводились В.В.Рыбаковым, С В, Бабеньгаевым и В.Р.Кияткиным [5, 86, 87, 91]. Для этого обычно использовалась схема, разработанная в 1984 году В.В.Рыбаковым для решения проблемы Кузнецова-Фридмана [26]. Эта схема оказалась достаточно гибкой и применимой для практически всех финитно аппроксимируемых логик, обладающих свойством ветвления. Вместе с тем, многие логики, представляющие достаточно большой интерес для исследователей, этим свойством не обладают. К ним можно отнести, например, модальные логики $4.2, 54.3, К4.2, К4.3 и суперинтуиционистские логики КС, ЬС (см. определение 2.2). Другая проблема состоит в требовании финитной аппроксимируемости исследуемых логик. Известно, что существуют разрешимые логики, не обладающие свойством финитной аппроксимируемости (и даже не компактные по Крипке) [22]. Эта проблемы инициировали проведение исследований для получения других схем доказательства разрешимости по допустимости, которые были проведены С.В.Бабенышевым, Ю.В.Безгачевой и др. (см. например [1, 3, 46, 63]).

В 2000 году Л.Л.Максимова предложила рассмотреть проблему разрешимости по допустимости для модальных логик 8А@а& и 54 ф. Эти логики реализуют два подхода к обобщению идеи ограничения возможности достижения максимальных миров, которая была введена с единичными ограничениями еще в известных логиках .54.2 и 54.1. Так, логика 54 ф характеризуется классом 54-фреймов, имеющих не больше N максимальных сгустков, а логика 54" классом фреймов, максимальные сгустки которых имеют не более N элементов [96]. Интерес здесь представляет главным образом логика 54 ф ая, не обладающая свойством ветвления. Построение алгоритма, распознающего допустимые правила вывода этой логики, дает нам еще одну методику решения аналогичных проблем. Решение этой задачи также позволит обосновать предположение о строгой разрешимости интерполяционного свойства над логикой 54, которое было выдвинуто в статье Л.Л.Максимовой [77].

Задача 1. Проверить, являются ли модальные логики 54 ф и 54 ф разрешимыми по допустимости.

Между суперинтуиционистскими и модальными логиками существует взаимосвязь. Впервые ее заметил К.Гёдель [64], указавший на возможность определения интуиционистской истинности в модальных терминах. Реальное воплощение эта идея получила спустя десятилетие в работе А.Тарского и Дж.МакКинси [79], в которой был введен Т-перевод интуиционистских пропозициональных формул в язык модальных исчислений. Такой подход, обобщенный для произвольных пропозициональных суперинтуиционистских логик, был развит в работах М.Думмета и Е.Леммона [54], Л.Л.Максимовой и В.В.Рыбакова [14]. После опубликования этих работ аналогии между модальными логиками, расширяющими логику Льюиса 54, и суперинтуиционистскими логиками стали очевидными. Были установлены связи и возможные переводы между соответствующими булевыми и псевдобулевыми алгебрами. В итоге были введены модальные напарники - классы нормальных модальных пропозициональных логик {г}}, сохраняющих Т -переводы всех теорем конкретных суперинтуиционистских логик. Множество всех модальных напарников заданной суперинтуиционистской логики образует решетку, ограниченную максимальным и минимальным модальными напарниками: т(А) С ц С <т(А). Так, для интуиционистской логики Гейтинга Н модальными напарниками являются все логики {т]} решетки: 54 С ?? С Огг.

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

Аналогичные исследования проводились и в отношении Т-перевода правил вывода. Было доказано [96], что истинность и производность правил вывода также сохраняются при Т -переводе на любой модальный напарник. Вместе с тем, проблема сохранения свойства допустимости правил вывода при Г-переводе оставалась не решенной в полном объеме. В.В.Рыбаков показал [23], что допустимость правил вывода сохраняется при Т-переводе для максимальных модальных напарников суперинтуиционистских логик. Однако допустимые правила часто не обладают общими фундаментальными свойствами формальных систем, такими, как разрешимость, конечная базируемость, финитная аппроксимируемость. Возможность сохранения свойства допустимости правил вывода при Т -переводе на всей решетке модальных напарников представлялась вероятной, но не столь очевидной [96], и В.В.Рыбаков предложил проверить это предположение для ряда известных логик.

Задача 2. Проверить сохранение допустимости правил вывода при Т-переводе из суперинтуиционистской логики в ее произвольный модальный напарник для ряда известных финитно аппроксимируемых логик.

В последние годы исследование допустимых правил вывода проводится также и в связи с изучением проблемы наследования. Известно, что для произвольных логик г] и Л, 1) С Л, правила вывода, допустимые в логике г}, могут не быть допустимыми в логике Л [92, 94, 95, 96, 99]. Вместе с тем, наследование (или сохранение) всех допустимых в логике 1} правил вывода логикой Л позволяет применять многие результаты исследований допустимых правил 1} в логике Л и наоборот. Проблема наследования для правил вывода состоит в получении описания классов логик, наследующих все допустимые правила вывода заданной логики Л, либо в получении признаков, распознающих эти логики.

Исторически вопрос о наследовании допустимых правил впервые был поставлен при исследовании суперинтуиционистских логик, не сохраняющих допустимые правила интуиционистской логики Гейтинга Н [92]. В дальнейшем было указано, что свойством наследования допустимых правил вывода должны обладать и структурно полные логики [95]. Только в 90-е годы были получены критерии наследования допустимых правил вывода для ряда известных логик. Сначала в работах В.В.Рыбакова был приведен критерий наследования для интуиционистской логики [92, 96]. Вскоре в статье, написанной В.В.Рыбаковым в соавторстве с Г.Генсером и Т. Онером, был доказан критерий наследования правил вывода, допустимых в модальной логике Льюиса 54 [99]. С помощью этого критерия были указаны все такие модальные логики среди табличных логик, расширяющих логику 54. Также В.В.Рыбаковым и В.В.Римацким получен критерий наследования допустимых правил вывода модальной логики ¿>4.2 [39].

Для изучения проблемы наследования большое значение имеет семантическое свойство ко-накрытия. Впервые это свойство также было введено для исследования свойства наследования в суперинтуиционистских логиках. Позже было предложено применить его и для исследования модальных логик. Так, в упомянутой статье [99] показано, что свойство ко-накрытия является необходимым и достаточным для наследования правил вывода, допустимых в логике 54. Современное изучение проблемы наследования допустимых правил вывода потребовало конкретизировать определение этого свойства и ввести новые определения ко-последователя и свойства ко-накрытия относительно произвольной финитно аппроксимируемой логики А. В статье [99] был поставлен ряд вопросов для дальнейшего изучения свойств наследования допустимых правил вывода. По мнению авторов статьи, наиболее существенной задачей стало нахождение критерия наследования правил вывода, допустимых в модальной логике К4, так как эта логика является базовой, как наименьшая транзитивная нормальная модальная логика.

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

Несмотря на достаточно общие подходы и требования к логикам для получения алгоритма распознавания допустимости, этот способ не универсален [96,63]. Поэтому в настоящее время исследуются принципиальные возможности и другого пути решения проблемы допустимости, а именно использования базисов этих правил. Задача построения базиса для допустимых правил вывода логики Л состоит в полном описании множества правил, из которых выводятся все правила, допустимые в Л. Впервые успешно эта задача была решена А.И.Циткиным для получения базиса допустимых квазихарактеристических правил вывода в интуиционистской логике [41]. Позже В.В.Рыбаковым было установлено, что большинство суперинтуиционистских и модальных логик не могут иметь базис для допустимых правил вывода от конечного числа переменных [96]. Вместе с тем, В.В.Римацким был получен класс модальных логик, имеющих конечный базис для допустимых правил вывода [20, 84]. В ходе дальнейших исследований [2, 19, 28, 29, 35, 38], проведенных В.В.Рыбаковым, С. В, Бабеяыигевым, В.В.Римацким, В.Р.Кияткиным и другими, были получены базисы для многих известных логик. Однако эти логики разрешимы по допустимости, поэтому в них интерес представляли явные базисы, то есть точно описываемые и легко используемые при проведении доказательств. Использование таких базисов позволяет избежать многих сложностей при создании и программировании реальных алгоритмов построения доказательств. Явные базисы были найдены Р.Иемхофф для интуиционистской логики Гейтинга Я [68] и В.В.Рыбаковым для модальной логики Льюиса 54

97]. В.В.Рыбаков, В.Р.Кияткин и М.Терзилер построили явные независимые базисы дяя модальных и суперинтуиционистских предтабличных логик [98].

Непосредственным алгебраическим аналогом допустимых правил являются квазитождества на свободных алгебрах многообразий, порожденных соответствующими логиками [15]. Известно [85, 96], что каждому правилу вывода г можно сопоставить квазитождество д(г), истинное на свободной алгебре ^(А) счетного ранга из многообразия 'оаг(Х), порожденного логикой А, тогда и только тогда, когда правило г допустимо в логике А. Это обусловило как возможность применения алгебраической семантики для исследования допустимых правил вывода, так и возможность использования результатов этих исследований при решении некоторых проблем алгебры [44, 45, 47]. Так, разрешимость по допустимости логики А равносильна разрешимости квазиэквациональной теории А)) свободных алгебр многообразия, порожденного этой логикой. В.В.Рыбаковым была доказана разрешимость универсальных теорий свободной псевдобулевой алгебры, свободной алгебры замыканий и свободных алгебр для многообразий логик, расширяющих логику 54.3, а С.В.Еабенышев доказал разрешимость квазиэквациональных теорий свободных алгебр из многообразий, порожденных логиками £>4.2 и S4.2Grz [1, 24, 30, 31, 34]. Аналогично, переводя базис для правил вывода, допустимых в логике А, в форму квазитождеств, мы можем получить базис для квазитождеств Тк<1(Т(Х)) [96, 103]. Таким образом Р.Иемхофф и В.В.Рыбаковым были построены явные базисы для квазитождеств Т^(.Г(Я)) и ТА, (^(54)). В 2001 году В.В.Рыбаков предложил, применяя технику редуцирования правил вывода, построить явные базисы для правил вывода, допустимых в модальных логиках А'4 и СЬ. В целом, построение явных базисов допустимых правил вывода для различных модальных и суперинтуиционистских логик, а также базисов для квазитождеств истинных на свободных алгебрах многообразий, порожденных этими логиками, является достаточно актуальной и во многом не решенной проблемой.

Задача 4. Построить явный базис для допустимых правил вывода минимальной транзитивной модальной логики К4.

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

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

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

Основные результаты. В диссертации получены следующие основные результаты.

1. Доказана разрешимость по допустимости для модальных логик ¿>4©а^ и .

2. Доказано сохранение допустимости правил вывода при Т -переводе из финитно аппроксимируемой суперинтуиционистской логики, модельно равномерной по допустимости, в каждый модальный напарник этой логики.

3. Получен критерий наследования всех правил вывода, допустимых в модальной логике К4 для финитно аппроксимируемых логик, и отрицательно решен вопрос о наследовании допустимых правил вывода логики КА табличными логиками. Получены признаки наследования всех правил вывода, допустимых в некоторой транзитивной модальной или суперинтуиционистской логике 7), финитно аппроксимируемой и модельно равномерной по допустимости.

4. Построен явный базис для правил вывода, допустимых в модальной логике К А.

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

Апробация работы. Результаты диссертации докладывались на следующих конференциях:

• XXXIX Международной научной студенческой конференции (Новосибирск, 2001),

• II Всесибирский конгресс женщин-математиков (Красноярск, 2002),

• ХХХХ Международной научной студенческой конференции (Новосибирск, 2002),

• Краевой межвузовской научной конференции "Интеллект 2002" (Красноярск, 2002),

• IV Международной конференции "Алгебра и приложения", посвященной 70-летию профессора В.П.Шункова и 65-летию профессора В.М.Буеаркина (Красноярск, 2002).

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

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

Заключение диссертации по теме «Математическая логика, алгебра и теория чисел», Руцкий, Алексей Николаевич

ЗАКЛЮЧЕНИЕ

В теоремах 2.2 и 2.3 проведено доказательство разрешимости по допустимости модальных логик 54 ф схн и 54 ф , не обладающих свойством ветвления, что является обоснованием предположения о строгой разрешимости интерполяционного свойства над логикой 54 [77]. В теореме 3.1 приведен критерий наследования допустимых правил вывода модальной логики К4. С помощью этого критерия доказано, что большинство известных модальных логик, в том числе табличные модальные логики (см. следствие 3.1), не могут наследовать допустимые правила вывода логики К А. В разделе 4.2 приведено построение множества правил вывода , которое, как показано в теореме 4.5, образует явный базис для правил вывода, допустимых в логике К А. Полученные результаты могут быть использованы в дальнейших исследованиях различных аспектов неклассических логик.

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

Список литературы диссертационного исследования кандидат физико-математических наук Руцкий, Алексей Николаевич, 2002 год

1. Бабенышев C.B. Разрешимость проблемы допустимости правил вывода в модальных логиках 54.2 и S4.2Grz // Алгебра и логика. 1992. -Т.31. -№4. - С.341-359.

2. Бабенышев C.B. Базисы допустимых правил вывода модальных логик 54.2 и S4.2Grz {{ Алгебра и логика. 1993. - Т.32. - №2. - С. 117-130.

3. Безгачева Ю.В. Допустимые правила вывода в логиках ширины 2 // Международная конференция по модальной логике: Тез. сообщ. Новосибирск, ун-т. Новосибирск, 1994. - С.19-21.

4. Захарьящев М.В. Синтаксис и семантика суперинтуиционистских логик // Алгебра и логика. 1989. - Т.28. - №4. - С.402-429.

5. Кияткин В.Р. Правила вывода с метапеременными и логические уравнения в пред-табличной модальной логике РМ1 // Сибирский математический журнал. 2000. -Т.41. - № 1. - С.88-97.

6. Крипке С.А. Неразрешимость одноместного модального исчисления предикатов // Модальная логика. М.: Наука, 1974. - С.247-253.

7. Крипке С.А. Семантический анализ модальной логики. I. Нормальные модальные исчисления высказываний // Модальная логика. М.: Наука, 1974. - С.254-303.

8. Крипке С.А. Семантический анализ модальной логики. И. Ненормальные модальные исчисления высказываний // Модальная логика. М.: Наука, 1974. - С.304-323.

9. Крипке С.А. Теорема полноты в модальной логике // Модальная логика. М.: Наука, 1974. - С.223-246.

10. Кузнецов A.B. О суперинтуиционистских логиках //Математические исследования.- 1975. Т.2. -№10. - С.150-157.

11. Максимова Л.Л. Предтабличные суперинтуиционистские логики // Алгебра и логика.- 1972. Т.14. - №2. - С.558-570.

12. Максимова Л.Л. Предтабличные расширения логики 54 Льюиса // Алгебра и логика.- 1975. Т.14. - Ш, - С.28-56.

13. Максимова Л.Л. Модальные логики конечных слоев // Алгебра и логика. 1975. -Т.14. - №3. - С.304-319.

14. Максимова Л.Л., Рыбаков В.В. О решетке нормальных модальных логик // Алгебра и логика. 1974. - Т.13. - №2. - С. 105-122.

15. Мальцев А.И. Алгебраические системы. М.: Наука, 1970. - 392 с.

16. Минц Г.Е. Допустимые и производные правила // Записки научного семинара ЛОМИ АН СССР. 1968. - №8. - С.189-191.

17. Минц Г.Е. Производность допустимых правил // Записки научного семинара ЛОМИ АН СССР. 1972. -№32. - С.85-99.

18. Расева Е., Сикорский Р. Математика математики. М.: Наука, 1972. - 592с.

19. Римацкий В.В, Базисы допустимых правил вывода табличных модальных логик ширины 2 // Алгебра и логика. 1996. - Т.35. - №5. - С.612-623.

20. Римацкий В.В. О конечной базируемости допустимых правил вывода модальных логик ширины 2 // Алгебра и логика. 1999. - Т.38. - №4. - С.436-455.

21. Рыбаков В.В. Модальные логики с LM -аксиомами // Алгебра и логика. 1978. -Т. 17. -Ко4. - С.455-467.

22. Рыбаков B.B. Разрешимые некомпактные расширения логики 54 // Алгебра и логика. 1978. - Т. 17. - № 2. - С.210-219.

23. Рыбаков В.В. Допустимые правила предтабличных модальных логик // Алгебра и логика. 1981. - Т.20. - №4. - С.440-464.

24. Рыбаков В.В. Элементарные теории свободных алгебр замыканий // XXVI Всесоюзная алгебраическая конференция: Тезисы докладов. Л., 1981. - С.116.

25. Рыбаков В.В. Допустимые правила логик, содержащих 54.3 // Сибирский математический журнал. 1984, - ТЖ - №5. - С.141-145.

26. Рыбаков В.В. Критерий допустимости правил в модальной системе 54 и интуиционистской логике // Алгебра и логика. 1984. - Т.23. - №5. - С.546-572.

27. Рыбаков В.В. Разрешимость проблемы допустимости в конечнослойных модальных логиках Ц Алгебра и логика, 1984. - Т.23. - № 1. - С.100-116.

28. Рыбаков В.В. Базисы допустимых правил логик 54 и Int // Алгебра и логика. -1985. Т.24. - №1. - С.87-107.

29. Рыбаков В.В. Базисы допустимых правил модальной системы Grz и интуиционистской логики // Математический сборник. 1985. - Т.128(170). - №3. - С.321-338.

30. Рыбаков В.В. Универсальные теории свободных Л-алгебр при Л Э 54.3 // Слож-ностные проблемы математической логики. Калинин. 1985. - С.72-75.

31. Рыбаков В.В. Алгебраические методы в пропозициональной логике // Семиотика и информатика. 1986. - №28. - С. 102-121.

32. Рыбаков В.В. Разрешимость по допустимости модальной системы (Угг и интуиционистской логики // Известия АН СССР: Сер. математическая. 1986. - Т.50. - № 3. - С.598-616.

33. Рыбаков В.В. Уравнения в свободной топобулевой алгебре // Алгебра и логика. -1986. Т.25. - №2. - С.172-204.

34. Рыбаков В.В. Уравнения в свободной топобулевой алгебре и проблема подстановки // Доклады АН СССР. 1986. - Т.287. - №3. - С.554-557.

35. Рыбаков В.В, Базисы допустимых правил модальной системы Стг и интуиционистской логики // Математический сборник. 1987. - Т.56. - №2. - С.311-331.

36. Рыбаков В.В. Допустимость правил вывода и логические уравнения в модальных логиках, аксиоматизирующих доказуемость // Известия АН СССР: Сер. математическая. 1990. - Т.54. - №3. - С.357-377.

37. Рыбаков В.В. Критерии допустимости правил вывода с параметрами в интуиционистской пропозициональной логике // Известия АН СССР: Сер. математическая. -1990. Т.54. - Мб. - С.693-703.

38. Рыбаков В.В., Кияткин В.Р., Терзилер М. Независимый базис для правил, допустимых в предтабличных логиках // Деп. ВИНИТИ 06.11.98, №3220-В98.

39. Рыбаков В.В., Римацкий В.В. Сохранение допустимости правил вывода в логиках, родственных Б4.2 // Сибирский математический журнал. 2002. - Т.43 - №2. -С.446-453.

40. Фейс Р. Модальная логика // Модальная логика. М.: Наука, 1974. - С. 13-220.

41. Циткин А.И. О допустимых правилах интуиционистской логики высказываний // Математический сборник. 1977. -Т.102. - №2. - С.314-323.

42. Циткин А.И. О структурально полных суперинтуиционистских логиках // Доклады АН СССР. 1978. - Т.241. - С.40-43.

43. Шютте К. Полные системы модальной и интуиционистской логики // Модальная логика. М.: Наука, 1974. - С.324-421.

44. Baker К. Finite equational basis for finite algebras a congruence-distributive equational class // Advanced Mathematics. 1977. - Y.24. - №3. - P.207 243.

45. Bellisssima F. Finitely generated free Heyting algebras // Journal of Symbolic Logics. -1986. V.51. - Ml. - P.152-165.

46. Bezgacheva J. V Admissible rules of temporal logic LinTGrz // Bulletin of the Section of Logic. 1997. - V.26. - № 2. - P.60-69.

47. Blok W.J, Pigozzi D. A finite basis theorem for quasivarieties // Algebra Universalies. -1986. V.22. - P.l-13.

48. Bose S., Fisher A. Verifying pipelined hardware using symbolic logic simulation // IEEE international Conference on Computer Design. 1989. // Information and Computation -1992. V.98. -M2. - P.378-400.

49. 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.

50. Chagrov A., Z&kh&ryaschev M. On independent axiomatizability of modal and supermtuitionistie logics // Journal of Logic and Computation. -1995. V.5. - P.287-302.

51. Chagrov A., Zakharyaschev M. Modal logics. London: Cambridge Press, 1997. - 589 p.

52. Clarice E.M., Grümberg O., Brown M. Reasoning about networks with many finite state processes // Proc. 5th ACM symp. on Principles of Distributed Computing. 1986. -P.240-248.

53. De Joung D., Troelstra S. On the connection of partially ordered sets with some pseudoboolean algebras // Indagationes mathematical. 1966. - Y.28. - P.317-329.

54. Dummet M.A., Lemmon E.J. Modal logics between 54 and S5 // Zeitschrift für mathematische Logik and Grundlagen der Mathematik. 1959. - V.5. - P.260-264.

55. Fagin R., Halpern J.Y., Vardi M.Y. What is an inference rule ff Journal of Symbolic Logics. 1992. - V.57. - № 3. - P.1018-1045.

56. Fine K. Logics containing 54.3 // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. 1971. - V.17. - P.371-376.

57. Fine K. An ascending chain of S4 logics // Theoria. 1974. - ¥.40. - P.110-116.

58. Fine K. The logics containing K4. Part I // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. 1974. - V.39. - P.229-237.

59. Fine K. The logics containing K4. Part II // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. 1975. - V.50. - P.619-651.

60. Fridman H. One hundred and two problems in mathematical logic ff Journal of Symbolic Logics. 1975. - V.40. - №3. - P.l 13-129.

61. Gabbay D.M. A general filtration method for modal logics // Journal of Philosophical Logic. 1972. - V.l. - P.29-34.

62. Gabbay D.M., De Jongh D.H.J. A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property // Journal of Symbolic Logic. 1974. -V.39. - № 1. - P.67-78.

63. Ghilardi S. Unification and projectivity in propositional logic //Preprint №58 \ 1996. -Milano University Italy. 1996. - 45 p.

64. Gödel K. Eine Interpretation in der Intuitionistisher Aussagenkaleulus // Ergebnisse mathematics Kolloquiumus. 1933. - V.4. - P.34-40.

65. Goldblatt R.I. Metainathematics of modal logics. Part I // Reports on Mathematical Logic. 1976. - №6. - P.41-78.

66. Goldblatt R.I. Metamathematics of modal logics. Part II // Reports on Mathematical Logic. 1976. - №7. - P.21-52.

67. Harrop R. Concerning formulas of the types A -f B A C, A —> 3xB(x) in intuitionistic formal systems // Journal of Symbolic Logic. 1960. - V.25. - № 1. - P.27-32.

68. IemhofF R. On the admissible rules of intuitionistic propositional logic // Journal of Symbolic Logic. 2001. - V.66. - №2. - P.402-428.

69. Jonsson B.3 Tarski A. Boolean algebras with operators. Part I // American Journal of Mathematics. 1951. - V.73. - P.891-939.

70. Jonsson B., Tarski A. Boolean algebras with operators. Part II // American Journal of Mathematics. 1952. - V.74. - P.127-162.

71. Kracht M. Internal definability and completeness in modal logics. // Ph. D. Free University of Berlin, 1991.-110 p.

72. Kripke S.A. Semantic analysis of modal logic // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. 1963. - V.9. - P.67-96,

73. Lemmon E.J. Algebraic semantics for modal logics. Part I // Journal of Symbolic Logic. 1966. - V.31. - P.46-64.

74. Lemmon E.J. Algebraic semantics for modal logics. Part II // Journal of Symbolic Logic. -1966.-V.31.-P.191-218.

75. Lorenzen P. Einfung in Operative Logik und Mathrnatik. Berlin - Göttingen - Heidelberg, 1955. - 412 p.

76. Makinson D. On some completeness theorem in modal logic // Zeitschrift für mathematische Logik und Grundlagen der Mathematik. 1966. - V.12. - P.376-394.

77. Maksimova L.L. Strongly decidable properties of modal and intuitionistic calculi // Logic Journal of IGPL. 2000. - V.8. - №6. - P.797-819.

78. McKinsey J.C.C. On syntactical construction of system of modal logic // Journal of Symbolic Logic. 1945. - V.10. - P.83-94.

79. McKinsey J.C.C., Tarski A. Some theorems about the sentential calculi of Lewis and Heyting // Journal of Symbolic Logic. 1948. - Y.13. - P.l-15.

80. Pigozzi D. Finite basis theorem for relatively congruence- distributive quasivarieties // Transactions of American Mathematical Society. 1988. - V.31Ö. - P.499-533.

81. Port J. The deducibilities of 55 // Journal of Philosophical Logic. 1981. - V.10. -P.409-422.

82. Port J. Axiomatization and independence in 54 and 55 // Report on Mathematical Logic. 1983. - V.16. - P.23-33.

83. Rosenschtein S.I. Formal theories of AI in knowledge and robotics // New General Computing. 1985. - V.3. - P.345-357.

84. Rimatskiy V.V. Finite bases of admissible inference rules for modal logics of width 2 // Bulletin of the Section of Logic. 1997. - V.26. - №3. - P.126-134.

85. 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.

86. Rybakov V.V. Metatheories of first-order theories // Proc. of the IV Asian Logic Conference. CSK Educational Center. Tokyo. Japan, 1990. - P.16-17.

87. 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.

88. Rybakov V.V. Poly-modal logic as metatheory of pure predicate calculus // Abstracts of the 9-th Intern. Congress of Log. Meth. and Phil, of Sci., Section 1-5. Uppsala. Sweden, 1991. - P. 158.

89. Rybakov V.V. A modal analog for Glivenko's theorem and its applications // Notre Dame Journal of Formal Logic. 1992. - V.33. - №2. - P.244-248.

90. Rybakov V.V. Rules of inference with parameters for intuitionistic logic // Journal of Symbolic Logic. 1992. - V.57. - №3. - P.912-923.

91. Rybakov V.V. Intermediate logics preserving admissible inference rules of Heyting calculus // Mathematical Logic Quarterly. 1993. - V.39. - P.403-415.

92. 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.

93. Rybakov V.V. Preserving of admissibility of inference rules in modal logic // Logical foundations of computer science; Lecture notes in computer science/Eds.: Nerude A., Matiyasevich Yu.V. Springer-Verlag, 1994. - V.813 - P.304-316.

94. Rybakov V.V. Hereditary structurally complete modal logics // Journal of Symbolic logic. 1995. - V.60. - Ml. - P.266-288.

95. Rybakov V.V. Admissibility of logical inference rules. Studies in Logic and Foundations of Mathematics. V.136. - Elseiver Sci.Publ., North-Holland - New-York - Amsterdam, 1997. - 617 p.

96. Rybakov V.V. Construction of an explicit basis for rules admissible in modal system S4 // Mathematical Logic Quarterly. 2001. - V.47. - M4.- P.441-446.

97. Rybakov V.V., Kiyatkin V.R, Terziler M. Independent bases for rules admissible in pretabular logics // Logic Journal of IGPL. 1999. - V.7. - M2. - P.118-139.

98. Rybakov V.V., Gencer G., Oner T. Description of modal logics inheriting admissible rules for 54 // Logic Journal of IGPL. 1999. - V.7. - №5. - P.635-663.

99. Rybakov V.V., Terziler M., Remazki V. A Basis in Semi-Reduced Form for the Admissible Rules of the Intuitionistic Logic IPC // Mathematical Logic Quarterly. 2000. - V.46. -№5. - P.207-218.

100. Segerberg K. Decidability of 54.1 // Theoria. 1968. - V.34. - P.7-20.102

101. Segerberg K. An essay in classical modal logic // Filosofska Studier. University of Uppsala. Uppsala, 1971. - V.l-3. - №13

102. S elm an A. Completeness of calculi for axiomatically defined classes of algebras // Algebra Universaiies. 1972. - V.2. - №2. - P.20-32.

103. Solovay R. Provability interpretations of modal logic // Israel Journal of Math. 1976. - V.25. - P.287-3G4.

104. Vardi M.Y. Querying logical databases // Journal of Computer and System Sciences. -1986. V.33. - P.142-160.

105. Williamson T. Some admissible rules in nonnormal modal systems // Notre Dame Journal of Formal Logic. 1993. - V.34. - №3. - P.378-400.

106. Wooldridge M,, Lomuscio A. A computationally grounded logic of visibility, perception and knowledge // Journal of IGPL. 2001. - V.9. - №2. - P.273-288.

107. РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ

108. РуцкийА.Н. Разрешимость по допустимости модальных логик S4®aN и 54ф£лг+1 // Материалы XXXIV научной студенческой конференции: Сб. ст. Краенояр. гос. ун-т. -Красноярск, 2001. С.102-112.

109. Rutskiy A.N. Decidability of Modal Logics 54 ф aN, 54 ф w.r.t. Admissible Inference Rules // Bulletin of the Section of Logic. 2001. - V.30. - M4. - P.181-189.

110. Руцкий A.H. Необходимый признак наследования допустимых правил вывода К4 // II Всесибирский конгресс женщин-математиков: Сб. ст. Краенояр. гос. ун-т. Красноярск, 2002. 201 с. - С. 117-122.

111. Руцкий А.Н. Сохранение допустимости правил вывода в финитно аппроксимируемых логиках при Т-переводе // Материалы IV международной конференции "Алгебра и ее приложения": Тез. докл. Красноярск, 2002. - С.102.

112. Руцкий А.Н. Признак наследования допустимых правил вывода для некоторых классов транзитивных модальных и суперинтуиционистских логик // Материалы IV международной конференции "Алгебра и ее приложения" : Тез. докл. Красноярск, 2002. - С.103-105.

113. Руцкий А.Н., Федоришин Б.Р. Критерий наследования допустимых правил вывода модальной логики К4 // Деп. ВИНИТИ. 11.11.2002, № 1938-В2002.

114. Руцкий А.Н. Явный базис для правил вывода, допустимых в модальной системе К4 и Деп. ВИНИТИ. 11.11.2002, Ne 1939-В2002.