автореферат диссертации по философии, специальность ВАК РФ 09.00.07
диссертация на тему: Современные проблемы использования табличных методов в логике

Полный текст автореферата диссертации по теме "Современные проблемы использования табличных методов в логике"

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

На правах рукописи

АНТОНОВА ОЛЬГА АРКАДЬЕВНА

СОВРЕМЕННЫЕ ПРОБЛЕМЫ ИСПОЛЬЗОВАНИЯ ТАБЛИЧНЫХ МЕТОДОВ В ЛОГИКЕ

Специальность 09.00.07 - логика

АВТОРЕФЕРАТ

диссертации на соискание ученой степени доктора философских наук

Санкт-Петербург 2004

Работа выполнена на кафедре логики философского факультета Санкт-Петербургскою государственного университета

Научный консультант: Слинин Ярослав Анатольевич

доктор философских наук, профессор

Официальные оппоненты: Ледников Евгений Евгеньевич

доктор философских наук, профессор

Джалианшили Зураб Отарович доктор философских наук, профессор

Гусев Станислав Сергеевич доктор философских наук, профессор

Ведущая организация: Санкт-Петербургский I осу дарственный

университет точной механики и оптики

Защита состоится ^2/200^ года в часов на заседании

диссертационного советаТД.212 232 (Л по защите диссертаций на соискание ученой степени доктора философских наук при Санкт-Петербур! ском государственном университете по адресу 199034, Санкт-Петербург, В.О., Менделевская линия, д. 5, философский факультет, ауд. ¿' У

С диссертацией можно ознакомиться в научной библиотеке им. М. Горького Санкт-Петербургского государственного университета

Автореферат разослан «

.-¿'■■с» и<-1 200 Нх.

<7

Ученый секретарь Диссертационного совета, Кандидат философских наук, доцент

Г.П. Любимов

твт

2

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы исследования.

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

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

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

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

помощи таблиц) дает преимущество их исполыования во многих областях логики и не только

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

Отсутствие систематическою обзора истории развития табличного метода диктует необходимость данного исследования

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

Степень разработанности темы.

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

В иностранной научной литературе ситуация сложилась существенно иная Хотя исследований, которые прямо ставили бы своей целью всестороннее рассмотрение истории развития табличного метода, не существует, имеется большое количество работ посвященных различным этапам развития данного метода доказательства. Среди фундаментальных исследований, о I метим работы Э.Бета, ДжЗемана, С Кангера, С.Клини, Р Смаллиана, МФиттиша, С Лиса, С.Крипке

Важное значение для понимания табличного метода доказательства имеют исследования посвященные проблемам его применения и использования в неклассических логиках

Исследования Я. Хинтикки, С.Крипке, П.И Быстрова, В Н Костюка, И Н Непейводы, М.Фиттинга, Э Бета, С Кангера, Р.Горе, Ф.Массачи, А Мазини, Т.Ьоргуиса, Р Голдблатта, П Уолпера посвящены проблемам применения табличного метода доказательства в различных системах модальной логики

Работы У Сакона, С Сурмы, В.Карниелли, Л А. Бочвара, В.К. Финна, М.Бааэа, Г Фермюллера, Р Хэнла рассматривают вопрос наиболее эффективного использования метода таблиц в многозначной логике

Среди работ посвященных применению метода таблиц в интуиционистской логике следует выделить работы Э.Бета, МФитгинга, М.Феррари, Р.Мильоли, Р.Дюкхоффа, С Крипке, А Авеллопе, У.Москато, М.Орнаги

Возможность использования табличного метода доказательства в релевантной логике рассматривалась в работах М Мак-Робби, Н Белнапа, П.И Быстрова.

Чрезвычайно ценными для понимания места и роли табличного метода в истории теории логического вывода являются работы, посвященные проблеме использования данного метода в области искусственного интеллекта, в частности в области теории и практики автоматического доказательства теорем Среди работ, посвященных данной проблеме, отметим работы Э.Бета, Р.Попплестона, И.Кохена, Л Триллинга, П.Венера, К Брода, И.Шенфелда, Л.Валлена, С.Ривса, А.Авеллоне, В Москато, М Орнаги, Ф.Массачи, П.Мильоли, П Бонатти, Н Бааз. Г.Фермюллер, Э.Эдера, Л. Уоллена.

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

Цель и задачи исследования.

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

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

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

Для достижения сформулированной цели автором решались следующие задачи исследования

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

2 Выявление особенностей процесса возникновения и развития табличного метода доказательства, рассматриваемого в связи с друшми традиционными методами доказательств — аксиоматическим, натуральным, секвенциальным.

3 Проведение историко-логического анализа основных направлений и тенденций развития теории логического вывода на протяжении XX века.

4 Формирование представлений о наиболее эффективном методе логически о вывода в рамках табличного метода доказательства.

5. Исследование причин усиления семантического аспекта логического вывода как теоретического базиса табличного метода доказательс1ва, осмысление роли семантики в развитии различных методов доказательства.

6. Анализ новых решений традиционных логических проблем — табличное доказательство Теоремы полноты, Теоремы компактности, интерполяционной теоремы и Основной теоремы оценка влияния табличного метода доказательства на возникновение новых методов доказательства в теории логического вывода

7 Определение места и роли табличного метода доказательства в

целом в истории теории логического вывода

Методология исследовании.

Автором использовались традиционные методы исследовательской работы, историко-логическии анализ исследовательской литературы и сравнительный анализ различных концепций логического вывода

Вместе с гем, в основу диссертационного исследования положены следующие теорешко-методологические принципы.

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

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

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

Положения и выводы, выносимые на защиту:

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

2 Табличному методу доказательства соответствуют следующие хронологические рамки:

Начальный этап развития теории табличного метода доказательства — семантический этап, который составляют семантические таблицы Бета и модели Хинтикки.

Досшжение 1ехнической простоты и эвристичности табличного метода было целью следующего — аналитического — этапа в развитии табличного метода. Так же как и на предыдущем этапе, эта цель была достигнута независимо друг от друга двумя логиками — С. Лисом и Р. Смаллианом.

Третий лап в развитии |абличного метода состоял в использовании его в различных системах неклассических логик.

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

3 Ведущая роль табличного метода доказательства в развитии

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

4. В теории табличного метода доказательства произошло объединение двух путей развития теории логического вывода — синтаксического и семантического, которое не только изменило весь дальнейший ход развития методов логического вывода в XX в., но и продолжает воздействовать на структуру последующих форм доказательства. Табличные методы Бета, Смаллиана, Финиша, Лиса и др. являкмея одним из оснований, на которых строятся новые, более эффективные теории логического вывода.

5 Наибольшим вкладом табличного метода доказательства в

развитие теории логического вывода является:

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

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

с в построении вывода с помощью табличного метода не участвуют

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

й процесс доказательства мношх базовых теорем при

использовании табличного метода упрощается

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

Теоретическое и практическое значение.

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

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

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

Апробация исследования

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

Результаты работы представлялись автором в ходе различных научных форумов, среди которых:

1 Первый Общероссийски и философский конгресс, Санкт-Петербург, июнь, 1УУ7.

2 Современная ло>ика проблемы 1еории, истории и применения в науке, 5 Общероссийская научная конференция Сапкт Петербург 1998

3 Смирновские чтения 2 Международная конференция, Москва, 1999

4 Современная логика проблемы 1еории, истории и применения в науке, б Общероссийская научная конференция Санкг-Псшрбург 2000

5 Современная логика, проблемы теории, истории и применения в науке, 7 Общероссийская научная конференция Сан к I-Петербург 2002

6 «Дни Петербургской философии», 15-16 ноября Круглый стол «Философия науки и техники»2002

7 Смирновские чтения 4 Международная конференция, Москва, 2003

8 Конференция «Рациональность и вымысел» Санкт-Петербург, 12-14 ноября. 2003

Ре^лмагы диссертационного исследования обсуждались па заседании кафедры логики философского факультета Санкт-Петербургского I осу дарственного университета Основные положения диссертации отражены в публикациях автора

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

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ Во Введении обосновывается актуальное! ь темы исследования, рассматривается состояние разраб01аннос!и проблемы, определяется общая цель, ставятся основные задачи исследования, формулируются основные методы исследования Кроме этого рассматриваются возможности теоретического и практического применения материалов работы, результаты апробации исследования

Глава I. Теория логическою вывода и табличный метод В первой главе предлагается общая картина разви I ия теории доказательств, на фоне которой определяется роль и место табличного метода среди остальных методов доказа1ельств Здесь рассмафиваются аксиоматический, натуральный и секвенциальный методы дока!а гельств

1.1. Табличный метод и его история развитии

Табличный методяв ше!ся опровергающей процедурой. 1абличный метод, рассмотренный с семашической точки ¡рения, представляет собой процедуру поиска для моделей В огом случае каждая истьь тблицы может быть рассмотрена в качестве частично1 о описания модели

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

История развития табличного метода доказательства начинается несомненно с 1 Генцена и его исследований, посвященных логическому выводу Логический вывод рассматривался Генценом только с теоретико-доказательной ючки зрения, не загра! нвая других аспектов построения вывода, например семантических. Генцен занимался анализом логических доказательств, и его исследования стали фундамснюм современной теории доказательств

Другой не менее известный I олландский математик — Э Бет рассматривал вывод уже не только с точки ¡рения теоретико-доказательной, но и с семантической точки зрения Очевидно, что введенные Бетом в качестве еще одного метода доказатсльава таблицы имели целью именно семантический анализ вывода Бет впервые указал на тесную связь, существующую между семантическими таблицами и секвенциальными исчислениями, а также между семантическими таблицами и системами натурального вывода.

Фактически семантические таблицы Бета и модели Хинтикки составляют первый, так называемый семантический эып развития табличного метода Несмотря на полезность с точки зрения семан 1 ического анализа вывода на практике оба данных метода оказались недостаточно удобными Так семантические таблицы Бета представляют собой довольно громоздкие табличные конструкции, разделенные на две части (колонки), из коюрых левая соответствует истине, а правая — лжи Хотя модель Хинтикки имеет структуру

дерева, что несомненно делаем ее намного ботсе удобной тля применения на практике, множество находящихся в точках дерева форм) т трсб}ет частого копирования, a это фактически усложняет поиск вывода

Достижение технической простил и эврисгичности табличного метода было целью следующею -- аналитически о — »rana в развитии табличного четда Гак же как и на предыдущем чане 'на цечь была достигнута независимо друг от др> та двумя дотиками— С Лисом и Р Смал тианом

И гак, когда техническая простом и элегантность таблиц с «классической» точки зрения была достигнута пришел черед рассмотреть возможнос1Ь их использования в неклассичееких системах Таким образом, следующий этап в развитии табличного метода состоял в расширении evo на различные системы неклассических логик

Хотя табличный метод быч со ¡дан лчя логики и в Л01ике, па насюящий момент область его применения значительно расширилась Традиционно правила табличных систем рассматриваются как шаги для построения контрмодели Табличные системы, основными свойствами которых являются анализ и опровержение, имеют подходящую форму для построения алгоритмов доказательства теорем

Современный этап рашития табличного метода, подразумевает под собой «автоматизацию» табличного метода, или возможность его применения в автоматическом поиске вывода Line у bei а была идея автоматического доказательства теорем при помоши таблиц, но к сожалению, она не привела к дальнейшим результатам Любопытно отметить, чю метод резолюций и метод таблиц в общераспространенной аналитической формулировке появились практически одновременно Однако еспи Робинсон, открыв метод резолюций, сразу заинтересовался его автоматическим применением, то Смаллиан и Лис совершенно не обратили внимание на «автоматическую» эффективность открытою ими метода аналитических таблиц Это во многом объясняет тот факт, что метод резолюций наиболее часто используется именно в автоматическом доказательстве теорем В настоящее время исследования в области автоматическою доказательства теорем методом таблиц являются приоритетными

1.2. Аксиоматический и табличный методы доказательства

Несмотря на значительные преиг^щества аксиоматического метода, один из коюрых состой! в шачительнои гехнической просюге описания вывода — вывод из аксиом можно построить используя один, максимум два правила, — процедура поиска доказательств в этих системах является достаточно сложной и громоздкой и, кроме юго, во многом зависит от личного опыта и шобретательносш Поиск дока^пелылва осложняется в значительной мере тем, что фактически не существует никаких предписаний о том, как вести доказательство или как опровергать формулы

Таким образом, отсутствие формализма, который был бы ближе к применяющимся в действительное)и рассуждениям при математических доказательствах, стало причиной возникновения различных вариантов на1урального исчисления, соответственно меюда нагурально1 о вывода

1.3. Натуральный вывод и табличный метод

Системы натурального вывода были открыты независимо друг от друга в начале 30-х ходов польским ломком С Яськовским и Г Генценом В отличие от выводов в рамках аксиоматическою метода, натуральные выводы, исполыуя в качестве отправной точки допущения вместо аксиом, посредством логических заключений приходят к резулыагу, не зависящему от допущений Основные правила натуральных исчислений производны в соответовующих аксиоматических исчислениях Выводы, полученные посредством такого метода, оказываются, как правило, короче, чем выводы на основе аксиоматического метода, гак как в последних одна и та же формула появляется несколько раз (в натуральных выводах >го случается гораздо реже) И главное, что значительно облегчает поиск вывода в этих системах, метод натурального вывода содержит уже некоторые предписания о том, как строить доказательство В качестве примера системы натурального вывода рассматривается с незначительными изменениями в обозначениях системы Ш (Ж) Генцена.

Можно ли преобразовать любой вывод в системе натурального вывода в «нормальный» вывод, который ведется прямым способом без окольных путей, а именно, от допущений к конечной формуле В параграфе анализируется введенное Правицем понятие максимальной формулы Вхождение формулы в

доказательство называется максимальным если око явтяегся ¡включением правила введения и посылкой правила удаления "1аким образом, вывод называется нормальным, если он не содержит максимальных вхождений формулы В параграфе формулируется Теорема о нормальной форме и несколько важных следствий из нее

Значения логических свя«ж в правилах натуральной дедукции фактически являются не классическими, а скорее конструктивными, и именно потому простые классические тавтолшии ( большим трудом доказываются в натуральном выводе, в том смысле, что их самое простое доказательство должно включать в себя гакие логические «грюки», которые далеки от естественности Так как эти правила непосредственно связаны с конструктивным значением логических связок, то когда мы используем эти правила дчя доказательства интуиционистских тавголотий, доказательство действитепыю окапывается естественным

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

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

1.4. Связь табличного и секвенциального методов дока ¡агсльсгва Секвенциальные исчисления впервые были рассмотрены 1 Генценом наряду с натуральными исчиспениями Секвеициа тьное исчисление, в отличие от системы натуральною вывода, не содержит допущений, хотя сохраняет присущее натуральным исчислениям деление способов заключения па введение и удаление логических знаков Правилам введения логических символов исчисления естественною вывода отвечают фигуры введения в сукцедент, а правилам удаления — фигуры введения в ан тецедент

Аналогично выводу в начальном исчислении, в секвенциальном исчислении используется преде ив [сние вывода в виде дерева, но здесь при движении вниз по дереву переходят не 01 формулы к формуле, а от выводимости к выводимости Таким образом, в этом исчислении происходит «вывод выводимостей»

Для любой секвенции, выводимой в Сосуществует дерево вывода, не содержащее сечений, и такое дерево вывода можно эффективно построить по произвольному дереву вывода данной секвенции Система (7? опшчается от системы 0\ исполыованием вмесю правила ссчения правило смешения

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

Для упрощения разрешающей процедуры для исчисления высказываний С Клини предлагает вариант генценовского исчисления Сп без структурных правил вывода Система О, как замечас] Юшпи, «пре тазначена дчя сокращения числа выборов посылок для данною зaкJIЮчeния, когда мы пытаемся исчерпать возможность доказательства данной конечной секвенции, особенно когда мы пытаемся доказать недоказуем осп, данной конечной секвенции»' В А Матулис предложил новые секвенциальные исчисления Ей (¿о), которые существенно отличались от исчислений Клини С\ и С'з

В этих системах 01сугпвуЮ1 структурные правила Далее, если некоторая секвенция 5] выводится из секвенции 5? (или из & и посредством применения какого-либо правила вывода исчисления Ео (Е'о), ю 51 выводима в Е0 (Е'о) только тогда, когда в этом исчислении выводима & (соо1ветсгвенно 52 и ,

Исчисления Е0 (Е'о) равнообъемиы исчислению Для вывода в исчислении £| (£'|) характерны следующие свойс1Ва

1 Клини С К Введение в метаматематику М 1957 С 425

1'(последняя обобщенная секвенция вывота не содержит отмеченных формул,

2)в каждую ветвь дерева вывопл аксиома вхоадт только один раз Важно отметить, чю анано! ично исчислениям Го (Е о) исчисления Е\ (£'1) равнообъемны О']

Аналогичным исчислением без структурных правил вывода является сис1ема <74 Клини Чта система имеет интересную семашическую ишсрпре1ацию

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

Секвенциальное дерево можно легко перестроить в семантическую табтицу, если поместить все Д-формучы н лев^ю часть таблицы, а Л-формулы ь правую часть таблицы

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

С практической точки ¡рения поиск вывода посредством метода секвенциальных деревьев является менее эффективным, чем посредством использования таблицы И связано это прежде всего с необходимости) многочисленного переписывания ней (меняемых формул Однако что касается теоретических иссиедований, в частности доказательства теоремы о полноте, метод секвенциальных деревьев оказывается просш незаменимым

Тесная свя;ь табличною и секвенциального методов доказательства отчетливо видна и в таблицах описанных И Земаном 1аблицы-доказательства являются вариантом семантических таблиц Бета

Ксли секвенция является базовой единицей Iенценовских исчислений, то базовой единицей подхода Бета является таблица Между ними существует определенное сходство В процессе вывода секвенция распадается на две носледова1ельности. соо1ветс1вующие антицеденту и сукцедетпу этой секвенции Таблица Э Ье! а разделяется па две части чевая часть соответствует антецеденту, а правая часть — с\кцеденту Таблица работает не с одной

секвенцией, а с множеством их поэтому она coorneiciuyeT, скорее, нити вывода данного цока!агельс1ва В секвенциальных исчислениях вывод строим начиная с аксиом и далее, применяя правила, потучаем последовательно более длинные и более сложные секвенции пока не получим !аключи1е 1Ьной секвенции '1 аблицы работают в обрашом направлении

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

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

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

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

В-третьих, системы без структурных правил вывода, такие как £0 (£о), (Е i) Мату лиса, (г4 Клини, еоотве1ствуюшие обратимым вариантам секвенциальных исчислений, с ючки зрения практическою поиска вывода

обладают значительными преимуществами В обратимых секвенциальных исчислениях для любою праинпа вывода секвенция-заключение выводима только в том случае, если выводимы секвенции-посылки При л ом переходя ог секвенции А, вывод которой мы хотим получить к секвснтгаям Гили секвенции), из которых А является выводимой по одному из правил, можно быть абсолютно уверенным в том, что в процессе вывода ничет не потеряно и мы не пользуемся такими секвенциями, которые в данном исчиспении не являются выводимыми Системы такого типа предполагают также интересную семантическую интерпретацию, непосредственно связанную с методом семантических таблиц Бета

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

Глава II. Табличные конструкции и их применение в классической логике

11.1. Семантический период развития табличного метода. Семантические таблицы Э. Бета и модельные множества Я. Хинтикки

Во второй главе рассматриваются два первых периода ра<вития табличного метода, один из которых — семантический — непосредственно связан с семантическими таблицами Бета и модельными множествами Хинтикки, а второй — аналитический — с таблицами Смаллиана и Фиттинга

Семантический период развития табличного метода обычно связывают с именами Э Бета и Я Хинтикки Семантические таблицы Бета представляют собой систематическую процедуру поиска контрпримера Практически одновременно с Бетом, Хинтикка предлагает модельное множество, идея которого состоит в том, что доказательс т во X — систематическая попытка построить модель, в которой -А' истинна, есчи попытка не удается, то X является истинным.

Хотя таблицы Бета и модельные множества Хинтикки оказались полезными для семантического анализа логических исчислений, с практической

ючки зрения, они оказались неудобными Ою привело к дальнейшему развитию табличного метода в сторону упрощения его формы что и было достигнуто на протяжении следующего «аналитического» периода развития табличного метода

П.2. Аналитический период раютия табличного меюда. 11.2.1. Аналитические таблицы Р. Смаплиана

Табличный метод, в частности аналитические таблицы оказался не только великолепной разрешающей (или полуразрешаюшей) процедурой, но методом, который позволил значительно упростить доказательства мно1их важных и очень важных, как например Теорема Генцена, теорем Посредством табличных исчислений, в частности аналитических таблиц, была доказана так называемая Абстрактная теорема

Табличный метод доказательства, ишестныи как аналитические таблицы, несомненно, принадлежит Р Смаллиану Однако предшественником Смаллиана в развитии именно аналитическою табличною метода был С Лис, работы которого, к сожалению, остались малойзвестными Смаллиан же во многом развил и углубил идеи Лиса

Лис делил формулы на две категории В отличие 01 Э Бета, Лис не разделял их в две колонки, а рассматривал вместе и обо ¡начат арифметическими знаками

Как и Лис, Смаллиан вводит оба вида таблиц — обозначенные и необозначенные. Там где Лис использовал для обозначения формул знаки «+» и «-», Смаллиан использует «7» и «/*'»

Табличные исследования традиционно полезны как элегантная форма для представления доказательства Поскольку роль автоматического доказательства теорем увеличивается, то справе/утиво возникает вопрос, является ли табличный метод подходящим в этой области В принципе систематическая табличная процедура может быть полезна с лой точки зрения Но систематические процедуры, даже регулярные Эрбрановы таблицы, не эффективны для широкого применения.

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

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

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

Блок-таблицы являются вариантом аналитических таблиц В отпичие от аналитических и семантических таблип блок-таблицы имеют в качестве точек дерева конечные наборы формул

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

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

Генцен доказал теорему для исчислений ЬК (классическое) и /„/(интуиционистское), Смаллиан доказал георему об устранении сечения при помощи аналитических таблиц Эта теорема включает в себя основную теорему Генцена, так как дает результаты и для таблиц, и для генценовских систем одновременно

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

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

Это показывает, что аналитические таблицы, построенные сошасно традиции без сечения, не всегда пригодны для решения проблем автомажческо! о доказательства теорем В то же время очевидно, что табличный метод наиболее естественно-расширяемая система Системы генценовско1 о типа, свободные от сечения, и соответствующие им табличные системы иногда придают доказательствам много «излишеств». Тогда можно предположить, что такие системы не во всех случаях естественны для систем классической ло1ики.

П.2.2. Таблицы Фиттинга

М. Фиттиш предлагает свой вариант аналитических таблиц, отличающийся от аналитических таблиц Смаллиана. Таблица рассматривался в терминах множества, таким образом, понятие «ветки» заменяется на понятие множества.

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

Глава 1П. Табличные методы в неклассических логиках

1П. 1. Методы логического вывода и таблицы в интуиционистской логике

Ш.1.1. Теоретический анализ методов лошческого вывода в интуиционистской логике (аксиоматический, натуральный и секвенциальный вывод)

Ш. 1.1.1. Аксиоматические системы интуиционистской логики

Первые исчисления интуиционистской логики были рассмотрены в работах В.И Гливенко, А.Н. Колмогорова, Гейтинга, Генцена Данные исчисления еще не содержали четкого конструктивною понимания математических суждений.

В параграфе отмечается что, коне ¡руктивный (интуиционистский) подход требует иного, нежели в классической логике, рассмо1рения основных логических понятий.

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

Теоремы интуиционистского пропозиционального исчисления Я1^ или минимального пропозиционального исчисления Р'х, которые не содержат отрицания, совпадают с теоремами позитивного пропозиционального исчисления, а те георемы какого-нибудь из исчислений Ру, Г $ или единственной связкой которых является о, совпадают с теоремами имшшкативного пропозиционального исчисления.

В параграфе также рассматривается более простая и «экономная» система интуиционистской (конструктивной) логики, которая была предложена П С Новиковым.

Конструктивная логика наравне с простым отрицанием путем приведения к противоречию выделяет еще одну форму отрицания — отрицание путем построения опровергающей конструкции, или сильное отрицание Ш.1.1.2. Натуральный вывод в интуиционистской лотке В 1934 году Г Генцен предложил формализацию интуиционистской логики, отличающуюся от классической логики одной схемой аксиом — именно законом исключенного третьего. Заметим, чю еще в 1929 юду В.И. Гливенко установил, что добавление закона исключенного третьего к интуиционистскому исчислению высказываний превращает его в классическое исчисление

Различие между системами Ш и ЫК состоит в допущении или недопущении закона исключенного третьего.

Нормальный вывод в интуиционистском натуральном исчислении соответствует выводу без сечения в секвенциальном исчислении

В нормальном выводе сешент не может начинаться заключением правил введения или правилом Г (для интуиционистской ло!ики) и не может заканчиваться большей посылкой правила удаления Соответственно, максимальным сегментом называется сегмент, который начинается заключением применения правила введения, или ^правилом для интуиционистской логики, и заканчивается большей посылкой применения правила удаления.

Нормальным выводом, как показал Правиц, является вывод, не содержащий максимальных сегментов и излишних применений правил удаления V или удаления 3.

Ш.1.1.3. Секвенциальные системы интуиционистской логики

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

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

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

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

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

Г точки зрения поиска вывода интуиционистское исчисление О), так же как и классическое оказались недостаточно эффективными В классической логике системы, более пригодные для алгоритмического поиска вывода Е0 (Е'о), были предложены В.А. Магулисом Необходимо было построить аналогичные

СИСТеМЫ И ДЛЯ ИНТУИЦИОНИСТСКОЙ Л01 ики.

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

Такую же роль, как в классической логике играют системы В.А Матулиса Ей и Е'о, для конструктивной играет система ./о, предложенная Р А Плтошкявичюсом

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

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

С ючки зрения эффективности поиска вывода равную позицию с обратимыми вариантами выводов занимают несократимые выводы Подробное описание алгоритма поиска данного вывода для соответствующего конструктивного исчисления было рассмофено Н Н Воробьевым В параграфе рассматривается алгоритм поиска вывода для конструктивною исчисления с сильным отрицанием.

Ш.1.2. Табличные методы в интуиционистской логике. Семантические таблицы Бета для систем интуиционис! ской логики

Первые теоретико-доказательные исследования в области интуиционистской логики А. Рейтинга, Г Генцена, АII Колмогорова затрагивали только синтаксис интуиционистской ишики, не касаясь ее семантики Семантическую модель для интуиционистской логики впервые предложил 3 В Нет Г'му же принадлежит и первая табличная система интуиционисткой логики

В параграфе рассматривается модификация табличной системы интуиционисгской логики Бета — система 1В Синтаксис системы 1,В отличается от и 1ем, что оперирует с секвенциями, у которых в сукцедсптс может быть более одной формулы

При переходе от системы Ы к 1.Я теряется крепкая связь существующая между формальной системой и семантикой интуиционистской логики.

В параграфе проводится сравнепие метода, который по сути, не является табличным, но в основе которого лежит процедура опровержения с табличным методом. Метод дерево-опровержение был предложен для системы и А Валером.

III. 1.3. Аналитические таблицы для систем интуиционистской логики

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

Классические аналитические таблицы Фиттипга имеют много обшего с интуиционистскими таблицами, однако соответствующая конструктивная семантика требует введения определенных ограничений на правила и ЬЪ, а именно множество 5 заменяется на

В параграфе рассматривается непротиворечивое множество интуиционистской логики Приводятся два основных варианта множества непротиворечивости для интуиционистской логики — множество непротиворечивости Бета и множество непротиворечивости Генцена

Далее в параграфе анализируется Теорема о существовании модели для интуиционистской логики, которая форму яируется следующим образом Пусть 5 — множество обозначенных формул 1,с Если .V принадлежит либо множеству непротиворечивое™ Бета, либо множеству непротиворечивости Ген пена, то множество 5 является интуиционистски выполнимым

Из данной теоремы непосредственно следуют полнота аксиоматических систем, полнота табличных систем, полнота систем генценовского типа. Теорема компактности, Теорема Левенгейма-Сколема, Интерполяционная теорема Крейга (для интуиционистской ло! ики)

Важно отметить спедукяций факт, который представляется несомненным и на который также указывает М Фиттинг существование «элегантной» табличной системы непосредственно связано или, скорее, эквиваленшо существованию «эффективного» понятия непротиворечивого множества дня данной системы.

Ш.1.4. Усовершенствованная табличная система Мильоли-Москато-Орнаги

Идея использования несократимых выводов в секвенциальном интуиционистском пропозициональном исчислении впервые была рассмотрена Н Н Воробьевым. В дальнейшем эта идея получила свое развитие в работах Р Дикхофа, Дж Худельмайера

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

В параграфе рассматривается система, полученная из сиетемы ЬВ добавлением новых правил и запрещением правила импликации слева для формулы -1А Данная система является полной.

Возможность использования несократимых выводов в системе Фиттинга была рассмотрена П Мильоли, У Москато и М Орнаги. Они ввели новый знак Т7,, тем самьм дублирование формул в выводе было значительно уменьшено.

111.1.5. Расширение табличного метода для интуиционистских логик на модальные системы. Системы Авсллоне-Феррари

В параграфе рассматриваются табличные исчисления для логик РЫ, и РЫ} с единственной модальностью О, предложенные А. Авеллоне, М

Феррари Логики Р1.1 и РЫ1 впервые были рассмотрены М Фэртлохом и М Мендлером

Ш.2.Табличные методы в модальной логике

Ш.2.1. Теоретический анализ методов логического вывода в системах модальной логики (аксиоматический, натуральный и секвенциальный вывод)

Ш.2.1.1. Аксиоматические варианты систем модальной логики

Существует два наиболее известных типа аксиоматических формулировок модальных исчислений — льюисовский и геделевский В отлитое от льюисовских систем, в которых аксиомы обычно модальные, в системах гсдслевского типа аксиомами являются все тавтологии, и к ним добавляются несколько модальных аксиом В параграфе рассматриваются модальные системы гильбертовского типа Т, ¿>5. Для сравнения также предлагаются исчисления Л'г", Т, £5 как в геделевской формулировке, так и в льюисовской

Ш.2.1.2. Натуральный вывод в модальной логике

Модальные системы натурального типа впервые были предложены в работах X. Карри, Д ТТравица, Ф. Фитча. В параграфе рассматриваются системы натурального типа А®5, Ш, N54, которые немного отличаются от систем натурального вывода, предложенных Д. Правицем.

Ш.2.1.3. Секвенциальные системы модальной логики

Большинство модальных систем появилось спачала в аксиоматических формулировках, и только потом, после открытия Г Генценом секвенциального исчисления, были предложены эквивалентные секвенциальные исчисления для модальных систем. Различные варианты модальных секвенциальных исчислений были рассмотрены в работах X. Карри, М Ониси и К Матсумото, С. Кант-ера. Многие первые секвенциальные модальные системы включали в себя элиминационную теорему.

В параграфе рассматриваются секвенциальные системы ОТ, С&|, О^ Во всех данных системах правило сечения устранимо, из чего следует, что приведенные выше геделевские системы дедуктивно эквиваленты соответствующим секвенциальным системам И кроме того, устранимость сечения дает разрешающие процедуры для поиска вывода в этих системах

Ш.2.2. Семантический анализ модальной логики методом таблиц. Семантические таблицы Кринке и модельные множества Хинтикки

Семан гический «путь» исследования модальной логики берет начало в работах Э. Бета, но затем прерывается до работ С. Кринке.

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

Семан гическая таблица для модальных систем имеет 1-у же функцию, что и семангаческие таблицы. Семантическая таблица — это специальная схема, предназначенная для проверки того, следует ли семан гически некоторая данная формула из некоторых других данных формул. Необходимым и достаточным условием, чтобы В пе следовала из А\, , А„ является существование модели, в которой А), ..., А„ были бы общезначимы, а В не была бы обще*начимой Для этого А\, ., А„ помещаем в левый столбец таблицы, а В — в правый столбец таблицы.

Ш.2.3. Табличные методы Фиттинга для модальной Л01 ики

Фиттинг предложил префиксные табличные системы, главная идея которых — обозначить возможные миры таким же образом, как синтаксические правила определяют достижимость. Префиксы можно рассматривать в качестве аналогов диаграмм К. Хьюга и С Крессвела. Префиксная система может быть рассмотрена также как прямой потомок секвенциальной системы Кангера Кангер предложил секвенциальные формулировки для некоторых модальных логик. Его система .V; представляет интерес, так как пропозициональные формулы в ней индексируются положительными числами. Эти числа могут быть рассмотрены как соответствующие возможным мирам в моделях Крипке Префиксы также рассматриваются в табличной системе, предложенной Фштиш ом, как названия для возможных миров.

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

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

Табличные исчисления, которые во многом являются схожими с префиксными табличными исчислениями и индексированными секвенциальными исчислениями Кангера, предложил П,И. Быстрое

III.3. Применение табличных методов в многозначной логике

IIU.1. Теоретический анализ методов логического вывода в многозначной логике (аксиоматический, секвенциальный)

Ш.3.1.1. Системы гильбсртовского типа в многозначной логике

Впервые трехзначная логика Лукасевича /.з была аксиоматизирована М Вайсбергом Позже он же предложил общий метод аксиоматизации для широкого класса конечнозначных логик, в который входят также все и-зпачпые логики Лукасевича Метод Вайсберга показывает, что конечная нормальная матрица аксиоматизируема.

Еще один метод аксиоматизации был предложен Дж. Россером и А Тюркеттом В качестве необходимых условий данный метод указывает па общезначимость импликативных формул В, С и К, а также обязательное наличие ./„-операторов.

Этот метод применим для конечнозначных логик Лукасевича, а также для предикатных многозначных логик Однако оба данных метода с практической точки зрения оказались крайне неудобными и громоздкими К тому же они накладывают значительные ограничения на класс аксиоматизируемых п-значных Jioi ик.

Метод аксиоматизации, применимый к более широкому классу л-значных логик, был предложен В М Поповым Единственным необходимым условием является существование одноместных функций 4(х), определяемых на множестве {1,. , п} (п>2), с единственным выделенным значением j

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

Ш.3.1.2. Секвенциальные системы миогозначной логики

После открытия Генценым секвенциальных исчислений появились севенциальные исчисления многозначной логики В параграфе рассматривается секвенциальное исчисление /.„( >.

В параграфе также рассматривается секвенциальное исчисление с мета-связками.

111.3.2. Табличные методы в миогозначной логике. Аналитические таблицы для систем многозначной логики.

В параграфе рассматриваются аналитические таблицы для системы Ви предложенные Д.А. Бочваром и В.К Финном.

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

В параграфе рассматриваются аналитические таблицы для систем многозначной логики. При этом конечную последовательность конфигураций (К\, ..., Кт) назовем ¿„ц-таблицей, если 1(,+\ получается из К, (г-1, ., т-1) применением некоторого правила редукции Ьудем также считать !.„, |-таблицей и последовательность (К), состоящую из одной конфигурации

В параграфе рассматриваются табличные конструктивные варианты для трехзначной логики Ъочвара В}.

Множество отмеченных формул (-) называется замкнутым, если существует формула Л, такая что ТА, е© или ТА, е© или /■/!, Х4е(=)

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

Ш.3.3. Табличный метод Карниелли. Систематизация конечнозначных логик через метод таблиц

Обозначенные таблицы для многозначных жмик были впервые рассмотрены У. Саконом, который предложил обозначенные таблицы для множества конечнозначных логик Лукасевича Общие обозначенные табличные системы, которые соответствуют дуальным секвенциальным системам впервые были описаны С. Сурмой, У. Карниелли; Н Забелем. Карниелли фактически только обобщает исследования Сурмы для копечпозначной первопорядковой логики с кванторами, Забель расширяет этот метод на бесконечнозпачныс логики.

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

Карниелли систематизировал практически все конечнозначные ло!ики посредством метода таблиц. Некоторые определения были заимствованы Карниелли у Сурма, однако существенным отличием подхода Карниелли является возможность использовать данный метод во всех мноюзначных первопорядковых логиках с любым количеством выделенных (с11ч^1пци'1чЪес1) истинностных значений.

Табличный метод является во многих случаях удобной заменой генценовских (секвенциальных) исчислений Но иногда эффективнее работать именно с секвенциальными исчислениями, на что указывает и Карниелли Лег ко заметить, что данные системы взаимопревращаемы и двойственны

Ш.3.4. Оптимизация табличного метода Карниелли. Таблицы для множеств-знаков Хэнла

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

ТП.3.5. Расширение таблично! о метода для конечнозначных логик на системы интуиционистской логики. Система Баса-Фермюллера

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

Попытка объединить табличное исчисление, основанное на интуиционистской логике, с табличным исчислением для всех конечнозначных пропозициональных логик была предпринята М Басом, Г Фермюллером В результате обобщения моделей Крипке для интуиционистской логики на класс конечнозначных логик образовалась так называемая комбинированная система, в данном случае интуиционистский «дубликат» конечнозначных систем

Ш.4. Методы логического вывода и таблицы в релевантной логике Ш.4.1. Теоретический анализ методов логическою вывода в релевантной логике (аксиоматический, натуральный и секвенциальный вывод)

Ш.4.1.1 Аксиоматические системы релевантной логики

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

Ш.4.1.2. Системы натурального вывода в релевантной логике Детальное рассмотрение натуральных систем релевантной логики было впервые проведено А. Андерсоном и Н. Белнапом. Их натуральные системы построены в стиле Фитча и пекоторыми существенными деталями отличаются от изложения натурального вывода, который приведен в параграфе

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

Ш.4.1.3. Генценовские логистические исчисления для релевантных систем

В параграфе рассматриваются генценовские логистические исчисления для релевантных систем Генценовское исчисление I.Rотличается от секвенциального исчисления следующими чер!ами. Исчисление LR-, содержи! только правила для —далее можно ограничиться секвенциями, имеющими единственную формулу в консеквенге. В исчислении LR^ отсутствует структурное правило утончения

Исчисление /.£-,_» аналогично исчислению LRтолько в правиле |—> В должно быть пустым и А должна содержать только формулы, в коюрых главная связка —>.

Также в параграфе рассматривается секвенциальный вариант исчисления R без отрицания — исчисление Lit,

Ш.4.1. Таблицы для систем релевантной логики

Ш.4.1.1. Таблицы для систем А'-, J?-,-*,

Первые табличные системы для релевантной логики были построены М Мак Робби и Н. Белнапом.

Генценовская система, соответствующая (->,-i) фрагменту релевантной системы R, получается простым ограничением логических правил — правилами для и -1, а также удалением правила утончения, которое ответственно за введение «иррелевантности» в классическое (и интуиционистское) мышление, поскольку появляется формула, которая не используется в выводе заключения.

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

Релевантная таблица для (->,-i) фрагмента системы R есть не что иное, как классическая таблица, выполняющая вышеприведенное требование Эквивалентность между такой табличной системой и генценовской системой относительно одного и того же фрагмента очевидна, формальное доказательство можно найти у Мак Робби и Белнапа. Необходимо сделать еще одно замечание относительно формулировки табличных правил. Важно отме!И1ь, что в

кон1ексге релевантных таблиц необходимо придерживаться версии а-правила с двумя заключениями и нельзя избегать повторения формулы

Ш.4.1.2. Таблицы для релевантных систем с мультипликативными связками

В параграфе рассматриваются релевантные системы, коюрые включают в себя мультипликативные связки о и +, а также л и v Табличный метод для релевантных систем, которые включают в себя эти связки, был впервые сформулировал М. МакРобби и Н. Белнапом.

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

Ш.4.1.3. Таблицы с индексированными формулами для релевантных систем

В параграфе рассматриваются табличные исчисления с индексированными формулами для релевантных систем R, RM.

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

По теме диссертации опубликованы следующие работы:

1. Табличные методы в логике. СПб, 2003. (14,5 п л )

2. Логика Биобиблиографический справочник. СПб. 2002. (в соавт. с Сохор Т.Е., Молославов A.C.)

3 Табличный метод как модель описания процесса аргументации //Современная логика: проблемы теории, истории и применения в науке Материалы 8 Общероссийской научной конференции. СПб., 2004. С.147-149. (0,8пл)

4. Перспективы преподавания математической логики// Проблемы преподавания логики и дисциплин логического цикла. Материалы Международной научно-практической конференции Киев. 2004 С 6-8 (1,2 п.л.)

РОС. НАЦИОНАЛЬНАЯ I БИБЛИОТЕКА I

СПстсИт I ов т w !

5 Философские аспекты возникновепия интуиционистской логики // Логико-философские штудии-2 СПб. 2003 21-36 (2 п.л.)

6 Философский анализ оснований интуиционистской логики //Смирновские чтения. 4-я Международная конференция. М., 2003. С. 190-191 (0,4 п.л )

7 Интуиция и логика в концепции Брауэра //Рационализм и воображение СПб., 2003. С. 114-116. (0,5 ц.л.)

8. Философский анализ брауэровской теории континуума как «среды свободного становления» //Вестпик Санкт-Петербургского государственного университета. Серия 6(3), №22. 2002. С. 28-33 (1 п л)

9 Философский взгляд на интуиционистскую логику //Философия объект и субъект научного исследования Санкт-Петербург 2002 С 23-37 (1,7 п л)

10. Об истории развития табличного метода в интуиционистской логике //Современная логика: проблемы теории, истории и применения в науке: Материалы 7 Общероссийской научной конференции СПб , 2002 С 294297 (0,7 п.л.)

11. Сравнительный анализ методов логического вывода //Рабочие тетради но компаративистике: Сравнительные исследования в гуманитарных и психологических науках. Выпуск 3. СПб. 2001. С 11-16. (0,8 п л )

12 Логический практикум (совм. с Милославовым A.C.. Наволоцкой ТА.. Любимовым Г.П., и др.). СПб., 2001. (2 п.л)

13. Алгоритм систематизации конечнозначных логик методом таблиц// Вестник Санкт-Петербургского университета, №2(14). СПб., 2000. С. 67-69. (0,9 п.л)

14 Сборник задач и упражнений по символической логике СПб , 2000 (1, 8 п.л.)

15. Чисто сукцедентная система S //Философия XX века школы и концепции СПб., 2000. С.404. (0,2 п.л.)

16 Проблема выводимости в конструктивных исчислениях с сильным отрицанием //Современная логика, проблемы теории, истории и применения в пауке: Материалы 6 Общероссийской научной конференции СПб., 2000 С 413-416. (0,7 п.л.)

17. Таблицы Земана //Материалы и i езисы Второго Российского философского конгресса. Т.2. Свердловск. С.ЗЗ. (0,3 п л.)

18 Возникновение и развише табличного метода доказательства// Смирновские чтения 2-я Международная конференция М, 1999 С 31 33 (0,8 п л )

19 Табличные построения для конечно шачных логик //Современная логика проблемы теории, истории и применения в науке. Ма1ериалы 5 Общероссийской научной конференции СПб., 1998 С.9-10 (0,7пл)

20 Метод семантических таблиц Э В Бета // Человек - Философия -Гуманизм. Тезисы докладов и выступлений Первого Российского философского конгресса (4-7 июня 1997 т ) т.З, Санкт- Петербург 1997т. С 152. (0,4 п.л.)

21 Логико-риторичсские вопросы у софистов //Современная логика' проблемы теории, истории и применения в науке. Санкт-Петербург. 1996 С 100 (0,3 п.л.)

Подписано в печать 05.10.2004

Формат 60x84 1/16 Усл. печ. л. 2,0. Тираж 100 экз. Заказ №124

Отпечатано в ООО «Издательство "ЛЕМА"»

199034, Россия, Санкт-Петербург, В О., Средний пр., д.24, тел./факс: 323-67-74

^ -10 0 4

РЫБ Русский фонд

2006-4 3186

Оглавление научной работы автор диссертации — доктора философских наук Антонова, Ольга Аркадьевна

Введение.

Глава I. Теория логического вывода и табличный метод

1.1. Табличный метод и его история развития.

1.2. Аксиоматический и табличный методы доказательства.

1.3. Натуральный вывод и табличный метод.

1.4. Связь табличного и секвенциального методов доказательства.

Глава II. Табличные конструкции и их применение в классической логике

II.1. Семантический период развития табличного метода. Семантические таблицы Э. Бета и модельные множества

Я. Хинтикки.

II.2. Аналитический период развития табличного метода.

П.2.1. Аналитические таблицы Р. Смаллиана.

II.2.2. Таблицы Фитгинга.

Глава III. Табличные методы в неклассических логиках

III. I. Методы логического вывода и таблицы в интуиционистской логике

Ш.1.1. Теоретический анализ методов логического вывода в интуиционистской логике (аксиоматический, натуральный и секвенциальный вывод) ГОЛ. 1.1. Аксиоматические системы интуиционистской логики.

Ш.1.1.2. Натуральный вывод в интуиционистской логике.

Ш. 1.1.3. Секвенциальные системы интуиционистской логики.

III. 1.2. Табличные методы в интуиционистской логике. Семантические таблицы Бета для систем интуиционистской логики.

П1.1.3. Аналитические таблицы для систем интуиционистской логики.

П1.1.4. Усовершенствованная табличная система Мильоли

Москато-Орнаги.

1П.1.5. Расширение табличного метода для интуиционистских логик на модальные системы. Системы Авеллоне-Феррари.

Ш.2.Табличные методы в модальной логике

III.2.1. Теоретический анализ методов логического вывода в системах модальной логики (аксиоматический, натуральный и секвенциальный вывод)

Ш.2.1.1. Аксиоматические варианты систем модальной логики.

Ш.2.1.2. Натуральный вывод в модальной логике.

Ш.2.1.3. Секвенциальные системы модальной логики.

1П.2.2. Семантический анализ модальной логики методом таблиц. Семантические таблицы Крипке и модельные множества Хинтикки.

1П.2.3. Табличные методы Фитгинга для модальной логики.

III.3. Применение табличных методов в многозначной логике

Ш.3.1. Теоретический анализ методов логического вывода в многозначной логике (аксиоматический, секвенциальный)

Ш.3.1.1. Системы гильбертовского типа в многозначной логике.

Ш.3.1.2. Секвенциальные системы многозначной логики.

III.3.2. Табличные методы в многозначной логике. Аналитические таблицы для систем многозначной логики.

Ш.3.3. Табличный метод Карниелли. Систематизация конечнозначных логик через метод таблиц.

Ш.3.4. Оптимизация табличного метода Карниелли.

Таблицы для множеств-знаков Хэнла.

III.3.5. Расширение табличного метода для конечнозначных логик на системы интуиционистской логики. Система Баса-Фермюллера.

Ш.4. Методы логического вывода и таблицы в релевантной логике.

Ш.4.1. Теоретический анализ методов логического вывода в релевантной логике (аксиоматический, натуральный и секвенциальный вывод) Ш.4.1.1 Аксиоматические системы релевантной логики.

Ш.4.1.2. Системы натурального вывода в релевантной логике.

Ш.4.1.3. Генценовские логистические исчисления для релевантных систем.

Ш.4.1. Таблицы для систем релевантной логики

Ш.4.1.1. Таблицы для систем RM.

Ш.4.1.2. Таблицы для релевантных систем с мультипликативными связками.

Ш.4.1.3. Таблицы с индексированными формулами для релевантных систем.

Введение диссертации2005 год, автореферат по философии, Антонова, Ольга Аркадьевна

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

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

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

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

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

Отсутствие систематического обзора истории развития табличного метода диктует необходимость данного исследования.

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

Степень разработанности темы.

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

В иностранной научной литературе ситуация сложилась существенно иная. Хотя исследований, которые прямо ставили бы своей целью всестороннее рассмотрение истории развития табличного метода, не существует, имеется большое количество работ посвященных различным этапам развития данного метода доказательства. Среди фундаментальных исследований, отметим работы Э.Бета, Дж.Земана, С.Кангера, С.Клини, Р.Смаллиана, М.Фиттинга, С. Лиса, С.Крипке.

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

Исследования Я. Хинтикки, С.Крипке, П.И.Быстрова, В.Н.Костюка, Н.Н.Непейводы, М.Фиттинга, Э.Бета, С.Кангера, Р.Горе, Ф.Массачи, А.Мазини, Т.Боргуиса, Р.Голдблатга, П.Уолпера посвящены проблемам применения табличного метода доказательства в различных системах модальной логики.

Работы У. Сакона, С.Сурмы, В.Карниелли, Д.А. Бочвара, В.К. Финна, М.Бааза, Г.Фермюллера, Р.Хэнла рассматривают вопрос наиболее эффективного использования метода таблиц в многозначной логике.

Среди работ посвященных применению метода таблиц в интуиционистской логике следует выделить работы Э.Бета, М.Фиттинга, М.Феррари, Р.Мильоли, Р.Дюкхоффа, С.Крипке,

A.Авеллоне, У.Москато, М.Орнаги.

Возможность использования табличного метода доказательства в релевантной логике рассматривалась в работах М. Мак-Робби, Н.Белнапа, П.И. Быстрова.

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

Среди работ, посвященных данной проблеме, отметим работы Э.Бета, Р.Попплестона, И.Кохена, Л.Триллинга, П.Венера, К.Брода, И.Шенфелда, Л.Валлена, С.Ривса, А.Авеллоне,

B.Москато, М.Орнаги, Ф.Массачи, П.Мильоли, П.Бонатги, Н.Бааз, Г.Фермюллер, Э.Эдера, JI. Уоллена.

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

Цель и задачи исследования.

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

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

Для достижения сформулированной цели автором решались следующие задачи исследования:

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

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

3. Проведение историко-логического анализа основных направлений и тенденций развития теории логического вывода на протяжении XX века.

4. Формирование представлений о наиболее эффективном методе логического вывода в рамках табличного метода доказательства.

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

6. Анализ новых решений традиционных логических проблем — табличное доказательство Теоремы полноты, Теоремы компактности, интерполяционной теоремы и Основной теоремы: оценка влияния табличного метода доказательства на возникновение новых методов доказательства в теории логического вывода.

7. Определение места и роли табличного метода доказательства в целом в истории теории логического вывода.

Методология исследования.

Автором использовались традиционные методы исследовательской работы: историко-логический анализ исследовательской литературы и сравнительный анализ различных концепций логического вывода.

Вместе с тем, в основу диссертационного исследования положены следующие теоретико-методологические принципы:

1. Исследование табличного метода доказательства как самостоятельного явления в теории логического вывода при одновременном рассмотрении его в контексте преобразования логической традиции (переходе от логик неклассического типа к логикам искусственного интеллекта).

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

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

Положения и выводы, выносимые на защиту:

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

2. Табличному методу доказательства соответствуют следующие хронологические рамки:

Начальный этап развития теории табличного метода доказательства — семантический этап, который составляют семантические таблицы Бета и модели Хинтикки.

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

Третий этап в развитии табличного метода состоял в использовании его в различных системах неклассических логик.

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

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

4. В теории табличного метода доказательства произошло объединение двух путей развития теории логического вывода — синтаксического и семантического, которое не только изменило весь дальнейший ход развития методов логического вывода в XX в., но и продолжает воздействовать на структуру последующих форм доказательства. Табличные методы Бета, Смаллиана, Фиттинга, Лиса и др. являются одним из оснований, на которых строятся новые, более эффективные теории логического вывода.

5. Наибольшим вкладом табличного . метода доказательства в развитие теории логического вывода является: а. одно из главных преимуществ табличного вывода состоит в том, что в нем наиболее ярко выражается связь, существующая между семантикой и синтаксисом логического исчисления. Таким образом, именно табличный метод показывает нам те семантические связи, которые лежат в основании логической (синтаксической) структуры рассматриваемой логики. b. правила построения табличного вывода соответствуют способу обычных содержательных рассуждений, таким образом, выводы, полученные методом таблиц, оказываются более естественными, чем, выводы в рамках аксиоматического, натурального и секвенциального методов доказательства. c. в построении вывода с помощью табличного метода не участвуют более сложные формулы, чем исходная (доказываемая), и каждый шаг построения вывода детерминирован конечным числом альтернатив дальнейших логических шагов. d. процесс доказательства многих базовых теорем при использовании табличного метода упрощается.

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

Теоретическое и практическое значение.

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

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

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

Апробация исследования

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

Результаты работы представлялись автором в ходе различных научных форумов, среди которых:

1. Первый Общероссийский философский конгресс, Санкт-Петербург, июнь, 1997.

2. Современная логика: проблемы теории, истории и применения в науке, 5 Общероссийская научная конференция. Санкт-Петербург. 1998

3. Смирновские чтения: 2 Международная конференция, Москва, 1999

4. Современная логика: проблемы теории, истории и применения в науке, 6 Общероссийская научная конференция. Санкт-Петербург. 2000

5. Современная логика: проблемы теории, истории и применения в науке, 7 Общероссийская научная конференция. Санкт-Петербург. 2002

6. «Дни Петербургской философии», 15-16 ноября. Круглый стол «Философия науки и техники»2002.

7. Смирновские чтения: 4 Международная конференция, Москва, 2003

8. Конференция «Рациональность и вымысел». Санкт-Петербург, 12-14 ноября. 2003.

Основные положения диссертации отражены в публикациях автора.

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

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

Заключение

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

Не вдаваясь в детали, мы дали только общий обзор того, как таблицы зарождались, как развивались и где они находятся сейчас. История таблиц, начиная свое существование с работ Г. Генцена, затем продолжает интенсивно развиваться в семантических исследованиях Э. Бета и Я. Хинтикки. С. Лис и Р. Смаллиан придают таблицам такую форму, что они становятся самым эвристичным методом доказательства. Таблицам становится тесно в рамках классической логики, и они распространяются на многие неклассические логики, параллельно развивая отношение с другими техниками доказательства и раскрывая тем самым возможности своей «автоматизации».

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

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

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

Мы ограничились только модальной, многозначной, релевантной, интуиционистской логиками. Однако существует еще много логических областей, в которых табличный метод эффективно применяется, но которые мы не затронули. Например, табличный метод успешно применяется в логиках программирования, на что указывают работы М. Фиттинга1; таблицы для логики с равенством были исследованы Б.

Л ч

Бекертом; С. Толедо предложил табличные системы для арифметики, которая использует со-правило; П. Эндрюс4 развил таблицы для теории типов; табличные построения для систем немонотонной логики были рассмотрены Н. Оливетги5.

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

1 Fitting М. Tableaux for logic programming // Journal of Automated Reasoning 13, 1994. P. 175—188.

2 Beckert B. Equality and other theories //Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht-Boston-London, 1999. P.197—254.

3 Toledo S. Tableau Systems for First Order Number Theory and Certain Higher Order Theories //Lecture Notes in Mathematics. V.447. Berlin, 1975.

4 Andrews P.B. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. 1986.

5 Olivetti N. Tableaux for nonmonotonic logics // Handbook of tableau methods. P.469—528.

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

Список научной литературыАнтонова, Ольга Аркадьевна, диссертация по теме "Логика"

1. Aczel Р.Н. Some results on intuitionistie predicate logic // Journal of Symbolic Logic. Vol. 32. 1967. P. 113—115.

2. Anderson A.R., Belnap N.D. Entailment: The logic of relevance and necessity. Princeton, 1975.

3. Avelone A., Ferrari M. Almost Dublication-Free Tableau Calculi for Propositional Lax Logics // Theorem Proving with Analytic Tableaux and Related Methods. 5-th International Workshop, Tableaux 96. P. 75—89.

4. Avelone AMoscato V., Miglioli P., Ornaghi V. Generalized tableaux Systems for Intermediate propositional logics // Automated Reasoning with Analytic Tableaux and Related Methods. International Conference. Tableaux 97. P. 139—147.

5. Avron A. Natural 3-valued logics — characterization and proof theory // Journal of Symbolic Logic. Vol. 56 (1). 1991. P. 276—294.

6. Avron A. The method of hypersequents in proof theory of propositional non-classical logics. Tel Aviv University, 1994.

7. Baaz M., Fermuller C.G. Non-elementary Speedups between41.

8. Different Versions of Tableaux // Proceedings of Tableaux 95, 4 Workshop on Theorem Proving with Analytic Tableaux and Related Methods. 1995. P. 217—230.

9. Baaz M., Fermuller G. Combining Many-Valued and Intuitionistie Tableaux // Theorem Proving with Analytic Tableaux and Related Methods. 5-th International Workshop, Tableaux' 96. Italy, May 1996. P. 23—35.

10. Baaz M, Fermuller G. Combining many-valued and intuitionistic tableaux // Theorem proving with analytic tableaux and related methods. 5-th Intern. Workshop, 1996. P. 65—79.

11. Barth E. On natural deduction in modal logic with two primitives //Logiqueet Analyse. 12, 1969. P. 157—166.

12. Beckert В., Hahnle R. Analytic tableaux // Automated Deduction — A Basis for Applications. Vol.I/Ed. W.Bibel., P.H.Schmitt. 1998.

13. Beckert В., Hahnle R, Schmitt P. The even more liberalized 5-rule in free variable semantic tableaux // Computational Logic and Proof Theory, Proceedings of the 3rd Kurt Godel Colloquium, 1993. P. 108—119.

14. Beckert В., Rape C. Incremental theory reasoning methods for semantic tableaux // Proceedings of Tableaux 96, 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods. Palermo, 1996. P. 93—109.

15. Beckert В., Posegga J. LeanTAP: Lean tableau-based deduction // Journal of Automated Reasoning. Vol. 15 (3). 1995. P. 339—358.

16. Belnap N.DJr., Gupta A., Dunn J.M. A consecution calculus for positive relevant implication with necessity // Journal of Philosophical Logic. Vol. 9. 1980. P. 343—362.

17. Benthem J.F.A.K. The Logic of Time: a model-theoretic investigation into the varieties of temporal ontology and temporal discourse. Synthese library. Vol. 156. Dordrecht, 1983.

18. Beth E. W. Vexistence en mathematique. Paris, 1956.

19. Beth E.W. On machines which prove theorems // Simon Stevin Wissen-Natur-Kundig Tijdschrift 32,1958. P. 49—60.

20. Beth E.W. Semantic construction of intuitionistic logic // Mededelingen der Kon. Ned. Akad. Vol. Wet 19, 11. Amsterdam, 1956.

21. Beth E. W. Semantic entailment and formal derivability // Mededelingen der Kon. Ned. Akad. Vol. Wet. 18, 13. Amsterdam, 1955.

22. Beth E. W. The foundations of mathematics. Amsterdam, 1959. ll.Bibel W. Automated Theorem Proving. Vieweg, 1982.

23. Borghuis T. Interpreting modal natural deduction in type theory I I Diamonds and Defaults. 1993. P. 67—102.

24. BozicM., Dosen K. Models for normal intuitionistic modal logics // Studia Logica. Vol. 43. 1984. P. 217—245.

25. Broda K. The application of semantic tableaux with unification to automated deduction // Technical report, Department of Computing, Imperial College, 1992.

26. Broda K. The application of semantic tableaux with unification to automated deduction // Technical report, Department of Computing, Imperial College, 1992.

27. Broda K. The relation between semantic tableaux and resolution theorem proves // Tech. Rep. DOC 80/20, Imperial College of Science and Technology. London, Oct. 1980.

28. Burgess J. Basic tense logic // Handbook of Philosophical Logic. Vol. П: Extensions of Classical Logic /Ed. D.Gabbay, F.Guenthner. Dordrecht, 1984. P. 1—88.

29. Carnielli W.A. An algorithm for axiomatizing and theorem proving in finite many-valued prepositional logic // Logique et analyse. Vol. 28. № 112. Louvain, 1985. P. 363—368.

30. Carnielli W.A. Systematization of finite many-valued logics through the method of tableaux // Journal of Symbolic Logic. Vol. 52 (2). 1987. P. 473-493.

31. Catach L. TABLEAUX: A general theorem prover for modal logics // Journal of Automated Reasoning. Vol. 7.1991. P. 489—510.

32. Cerrito S., Mayer M. Hintikka Multiplicities in Matrix Decision Methods for Some Propositional Modal logics // Automated Reasoning with Analytic Tableaux and Related Methods. International Conference. Tableaux'97. P. 25—35.

33. Cook S.A. The complexity of theorem proving procedures // Proceedings of the 3rd Annual Symposium on the Theory of Computing, 1971.

34. D 'Agostino M. Tableaux methods for classical prepositional logic // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 45—123.

35. D Agostino M., Gabbay D, Broda K. Tableaux methods for substructural logics // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 397—467.

36. D 'Agostino M., Gabbay D. A generalization of analytic deduction via labeled deductive systems. Part 1: basic substructural logics // Journal of Automated Reasoning. Vol. 13. P. 243—281. 1994

37. Davis M. The prehistory and early history of automated deduction // Automation of Reasoning, /Ed. J. Siekman, G. Wrightson. New York, 1983. P. 1—28.

38. Davis M., Putnam H. A computing procedure for quantification theory // Automation of Reasoning /Ed. J. Siekman, G. Wrightson. New York, 1983. P. 125—139.

39. Dosen K. Sequent-systems for modal logic // Journal of symbolic logic. Vol. 50 (1). 1985. P. 149—168.

40. Dunn J.M. A «Gentzen system» for positive relevant implication // Journal of Symbolic Logic. Vol. 38. 1973. P. 356—357.

41. Dyckhoff R. Contraction—free segment calculi for intuitionistic logic // Journal of Symbolic Logic 57 (3). 1992. P. 111—118.

42. Eder E. An Implementation of a Theorem Prover based on the Connection Method // Artificial Intelligence Methodology Systems Applications. /Ed. W.Bibel, B.Petkoff. North Holland, 1985. P. 121—128.

43. Emerson E.A., Halpern J.Y. Decision procedures and expressiveness in the temporal logic of branching time // Journal of Computer and System Sciences. Vol. 30. 1985. P. 1—24.

44. Ferrari M, Miglioli P. Counting the maximal intermediate constructive logic // Journal of Symbolic Logic. Vol. 8 (4). 1993. P. 21—33.

45. Fisher M. A resolution method for temporal logic // Proceedings of 12th International Joint Conference on Artificial Intelligence 1991. Morgan-Kaufmann, 1991. P. 99—104.

46. Fitting M. An embedding of classical logic in S4 II Journal of Symbolic logic. Vol. 35. 1970. P. 529—534.

47. Fitting M. Intuitionistic Logic, Model theory and forcing. New York, 1969.

48. Fitting M. Model existence theorems for modal and intuitionistic logic // Journal of Symbolic Logic. Vol. 38. 1973 P. 213—218.

49. Fitting M. С. First-order modal tableaux I I Journal of Automated Reasoning 4. 1988. P. 191—213.

50. Fitting M.C. Intuitionistic Logic, Model Theory and Forcing. Amsterdam, 1997.

51. Fitting M.C. Tableau methods of proof for modal logics I I Notre Dame Journal of Formal Logic 13. 1972. P. 237—247.

52. Fitting M.C. Tableaux for logic programming // Journal of Automated Reasoning 13. 1994. P. 175—188.

53. Gale M. The philosophy of Time. New York. 1967.

54. Giambrone S. Gentzen systems and decision procedures for relevant logics // Bulletin of the section of logic. Warszawa; Lodz, 1982 (1983). Vol. 11 (3/4). P. 169—175.

55. Ginsberg M.L. Multi-valued logics // Computational Intelligence. Vol. 4 (3). 1988.

56. Goldblatt R.I. Logics of Time and Computation // Lecture Notes 7, Center for the Study of Language and Information. Stanford, 1987.

57. Gore R. Tableaux methods for modal and temporal logic // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 297—396.

58. Gough G. Decision procedures for temporal logics. Manchester, 1984.

59. Hahnle I. Automated Deduction in Multiple-Valued logics. New York. 1993.

60. Hahnle R. Tableaux for many-valued logics // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 529—580.

61. Hahnle R. Uniform notation of tableaux rules for multiple-valued logics // Proceedings International Symposium on Multiple-Valued Logic. Victoria, IEEE. 1991. P. 238—245.

62. Hintikka JForm and content in quantification theory // Acta Philosophica Fennica Two Papers on Symbolic Logic 8. 1955. P. 8—55.

63. Kawai H. Sequential calculus for a first-order infinitary temporal logic // Mathematical Logic Quarterly. Vol. 33. 1987. P. 423—432.

64. Kirin KG. Gentzen's method of the many-valued prepositional calculi // Zeitschrift fur mathematische logic und Grundlagen der Mathematik. Bd. 12. Leipzig, 1966. P. 317—332.

65. Komori Y. Some results on the super-intuitionistic predicate logics // Reports on mathematic logic. Warszawa; Cracow, 1983. №15. P. 13—33.

66. Letz R. First-order tableau methods // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 126—196.

67. Loveland D.W. Automated Theorem Proving: A Logical Basis. North Holland, 1978.

68. MasiniA. 2-sequent calculus: Intuitionism and natural deduction // Journal of Logic and Computation. Vol. 3 (5). 1993. P. 533—562.

69. McRobbie M., Belnap N.D. Proof-tableau formulations of some first-order relevant ortho-logics // Bulletin of the section of logic. Warszawa; Lodz, Vol. 13 (4). 1984. P. 233—240.

70. Meyer R.K., McRobbie M.A., Belnap N.D. Linear analytic tableaux I I Proceedings of Tableaux'95. 4 th Workshop on Theorem Proving with Analytic Tableaux and Related Methods. Vol. LNAI 918. 1995. P. 278—293.

71. Miglioli P., Moscato U., Ornaghi M. An improved refutation system for intuitionistic predicate logic // Journal of Automated Reasoning, 13 (3). 1994. P. 361—373.

72. Miglioli P., Moscato U., Ornaghi M. Refutation systems for pro positional modal logics // Proceedings of the 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods. Vol. LNAI 918. 1995. P. 95—105.

73. Mints G. Gentzen-type systems and resolution rule. Part I: Propositional logic // Proceedings International Conference on Computer Logic, COLOG'88. Tallinn, USSR. Vol. 417 of Lecture Notes in Computer Science. Berlin, 1990. P. 198—231.

74. Mints G. Gentzen-type systems and resolution rule. Part П: Predicate logic // Proceedings ASL Summer Meeting, Logic Colloquium'90. Helsinki, Finland. Vol. 2 of Lecture Notes in Logic. Berlin, 1993. P. 163—190.

75. Mints G. Proof theory in the USSR, 1925—1970 // Journal of Symbolic Logic, 56 (2). 1991. C. 385-423.

76. Mundici D. A constructive proof of McNaughton's Theorem in infinite-valued logic // Journal of Symbolic Logic. Vol. 59 (2). 1994. P. 596—602.

77. Murray N.V., Rosenthal E. Resolution and path-dissolution in multiple-valued logics // Proceedings International Symposium on Methodologies for Intelligent Systems. Charlotte, 1991.

78. Ohnishi M, Matsumoto К. Gentzen method in modal calculi I // Osaka Mathematical Journal. Vol. 9. 1957. P. 113—130.

79. Ohnishi M, Matsumoto K. Gentzen method in modal calculi II // Osaka Mathematical Journal. Vol. 11. 1959. P. 115—120.

80. Ono H., Komori Y. Logics without the contraction rule // Journal of Symbolic Logic. Vol. 50. 1985. P. 16£—201.

81. Oppacher F., Suen E. HARP: A tableau-based theorem prover // Journal of Automated Reasoning, 4. 1988. P. 69—100.

82. Paech B. Gentzen-systems for propositional temporal logics // Proceedings of 2nd Workshop on Computer Science Logics, LNCS. 1988. P. 240—253.

83. Poplestone R.J. Beth-tree methods in automatic theorem-proving // Machine Intelligence /Ed. N.L.Collins, D.Michie. Vol. 1. New York, 1967. P. 31—46.

84. Pottinger G. Uniform, cut-free formulatins of T, S4 and S5 II Journal of Symbolic Logic. Vol. 48. 1983. P. 900—901.

85. Prior A. Past, present and future. Oxford, 1967.

86. Reeves S. Semantic tableaux as a framework for automated theorem-proving I I Advances in Artificial Intelligence (Proceedings of AISB-87). /Ed. C.S.Mellish, J.Hallam. Wiley, 1987. P. 125—139.

87. Reeves S.V. Adding equality to semantic tableaux // Journal of Automated Reasoning, 3. 1987. P. 225—246.

88. Rosser J.В., Turquette A.R Many-valued Logics. Amsterdam, 1952.

89. Rousseau G. Sequents in many valued logic I // Fundamenta Mathematica, LX. 1967. P. 23—33.

90. Rousseau G. Sequents in many valued logic ПУ/ Fundamenta Mathematics LXVII. 1970. P. 125—131.

91. Sambin G., Valentini S. A modal sequent calculus for a fragment of arithmetic // Studia Logica. Vol. 34. 1980. P. 245—256.

92. Schmitt S.f Kreitz C. Converting non-classical matrix proofs into sequent-style systems // Proceedings of 13th International Conference on Automated Deduction. Vol. 1104 of Lecture Notes in Artificial Intelligence. Berlin, 1996. P. 418—432.

93. Schroder J. Korner's criterion of relevance and analytic tableaux // Journal of Philosophical Logic. Vol. 21 (2). 1992. P. 183—192.

94. Shankar N. Proof search in the intuitionistic sequent calculus // Proceedings of 11th International Conference on Automated Deduction. Vol. 607 of Lecture Notes in Artificial Intelligence. Berlin, 1992. P. 522—536.

95. Smullyan R.M. Analytic natural deduction // Journal of Symbolic Logic, 30. 1965. P. 123—139.

96. Smyllyan R.M. First-order logic. New York, 1964.

97. Suchon W. La methode de Smullyan de construire le calcul n-valent des propositions de Lukasiewicz avec implication et negation // Reports on Mathematical Logic. Universities of Cracow and Katowice, 2. 1974. P. 37—42.

98. Sundholm G. Systems of deduction // Handbook of Philosophical Logic. Vol. I, chapter 1.2. /Ed. D.Gabbay, F.Guenther. Dordrecht, 1983. P. 133—188.

99. Surma S.I. An algorithm for axiomatizing every finite logic // Computer science and multiple-valued logic: theory and applications. Amsterdam, 1977. P. 143—149.

100. TakahashiM. Many-valued logics of extended Gentzen style П // Journal of Symbolic Logic. Vol. 35 (4). 1970. P. 493—528.

101. Thistlewaite P.В., Meyer R.K., McRobbie M.A. Advanced theorem-proving techniques for relevant logics // Logique et analyse. Vol. 28 (110/111). Louvain, 1985. P. 233—256.

102. Thomason R.H. On the strong semantical completness of the intuitionistic predicate calculus // Journal of Symbolic Logic. Vol. 33. 1968. P. 12—25.

103. Toledo S. Tableau Systems for First Order Number Theory and Certain Higher Order Theories // Lecture Notes in Mathematics. Vol. 447. Berlin, 1975.

104. Trzesicki K. Gentzen-style axiomatization of tense logic I I Bulletin of the section of logic. Warszawa; Lodz, 1984. Vol. 13 (2). P. 75—84.

105. Tuziak R. An axiomatization of the finite-valued Lukasiewicz calculus // Studia Logica. Vol. 47 (1). 1988. P. 49—55.

106. Urquhart A. Semantic for relevant logic // Journal of Symbolic Logic. Vol. 37. 1972. P. 11—17.

107. Urquhart A. The complexity of propositional proofs // The Bulletin of Symbolic Logic. Vol. 1. 1995. P. 425—467.

108. Urquhart A. The undecidability of entailment and relevant implication I I Journal of symbolic logic. Vol. 49 (4). 1984. P. 1059—1073.

109. Valentini S. The modal logic of provability: cut-elimination // Journal of Philosophical Logic. Vol. 12. 1983. P. 471—476.

110. Vellino A. The Complexity of Automated Reasoning. PhD thesis, University of Toronto, 1989.

111. Waaler A., Wallen L. Tableaux for intuitionistic logics // Handbook of tableau methods /Ed. M.D'Agostino, Dov M.Gabbay, R.Hahnle, J.Posegga. Dordrecht; Boston; London, 1999. P. 255—296.

112. Wallen L.A. Automated Deduction in Nonclassical Logics. 1990.

113. Warning H. Sequent calculi for normal modal propositional logics // Journal of Logic and Computation. Vol. 4. 1994.

114. Wolper P. The tableau method for temporal logic: an overview I I Logique et Analyse, 110—111. 1985. P. 119—136.

115. Woodruff P.W. A modal interpretation of three-valued logic I I Journal of Philosophical Logic. Vol. 3. 1974. P. 433—440.

116. Woolhouse R. Tensed modalities // Journal of Philosophical Logic. Vol. 2. 1973. P. 393—415.

117. Wrightson G. Non-classical theorem proving using links and unification in semantic tableaux // Tech. Rep. CSD-ANZARP-84-003. Wellington, 1984.

118. Zabel N. Nouvelles Techniques de Deduction Automatique en Logiques Polyvalentes Finies et Infinies du Premier Ordre. PhD thesis. Institut National Polytechnique de Grenoble. 1993.

119. Zach R. Proof theory of finite-valued logics. Master's thesis, Institut fur Algebra und Diskrete Mathematik. Wien, 1993.

120. Zeman I. Modal logic. Oxford, 1973.

121. Аншаков О.М.у Рынков С.В. О многозначных логических исчислениях // Семиотика и информатика. Вып. 19. М., 1982. С. 90—117.

122. Аншаков О.М., Рынков С.В. Об одном способе формализации и классификации многозначных логик // Семиотика и информатика. Вып. 23. М., 1984. С. 78—106.

123. Бочвар Д.А. К вопросу о непротиворечивости одного трехзначного исчисления // Математический сборник. Т. 12. № 3. 1943. С. 287—308.

124. Бочвар ДА., Финн В.К. О многозначных логиках, допускающих формализацию анализа антиномий // Исследования по математической лингвистике, математической логике и информационным языкам. М., 1972. С. 238—295.

125. Бродский И.Н. Индексация формул и поиск вывода // Вестник СПбГУ. Сер. 6. Вып. 4. СПб., 1992.

126. Быстрое П.И. Взаимное преобразование секвенциальных и натуральных выводов в модальной логике // Логические исследования. Вып. 6. М., 1999. С. 61—68.

127. Быстрое П.И. Нестандартный метод табличных конструкций для модальных и релевантных логик // Логические исследования. Вып. 1. М., 1993. С. 156—171.

128. Быстрое П.И. Погружение релевантной системы Е в табличное исчисление индексированных формул // Многозначные, релевантные и паранепротиворечивые логики. М., 1984. С. 20—26.

129. Войшвгишо Е.К. Философско-методологические аспекты релевантной логики. М., 1988.

130. Воробьев Н.Н. Конструктивное исчисление высказываний с сильным отрицанием // Доклады Академии Наук СССР. Т. 85. № 3 (1952). С. 465—468.

131. Воробьев Н.Н. Конструктивное исчисление высказываний с сильным отрицанием // Труды Математического института АН СССР. Т. LXXII (1964). С. 195—227.

132. ГейтингА. Интуиционизм. М., 1965.

133. Генцен Г. Исследования логических выводов // Математическая теория логического вывода. М., 1967. С. 9—49.

134. Катер С. Упрощенный метод доказательства для элементарной логики // Математическая теория логического вывода. М., 1967. С. 200—206.

135. Карпенко А.С. Многозначные логики // Логика и компьютер. Вып. 4. М., 1997.

136. Клини С.К Введение в метаматематику. М., 1957.

137. Клини С.К. Математическая логика. М., 1973.

138. Клини С.К. Перестановочность применений правил в генценовских исчислениях LK и ZJ // Математическая теория логического вывода. М., 1967. С. 208—236.

139. Крайзелъ Г. Основания интуиционистской логики // Математическая логика и ее применения. М., 1965. С. 229—244.

140. Крайзелъ Г. Исследования по теории доказательств. М., 1981.

141. Крипке С. Семантический анализ модальной логики. I. Нормальные модальные исчисления высказываний // Фейс Р. Модальная логика. М., 1974. С. 254—304.

142. Крипке С. Семантический анализ модальной логики. П. Ненормальные модальные исчисления высказываний // Фейс Р. Модальная логика. М., 1974. С. 304—324.

143. Максимова JI.JI. Предгабличные суперинтуиционистские логики // Алгебра и логика. 1972. № 11. С. 13—17.

144. Мардаев С.И. Две иерархии локально-табличных суперинтуиционистских логик. Новосибирск, 1987.

145. Марков А.А. Конструктивная логика // Успехи математических наук. Т. 5 № 3 (1950). С. 187—188.

146. Марков А.А. О конструктивной математике // Труды математического института им. В.А. Стеклова. Т. 67. 1962. С. Sr—14.

147. Маслов С.Ю. Возможности применения теории дедуктивных систем // Теория логического вывода. Ч. 1. М., 1974.

148. Маслов С.Ю. Обратимый вариант конструктивного исчисления предикатов // Записки научных семинаров ЛОМИ АН СССР. 1967. Т. 4. С. 96—110.

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

150. Маслов С.Ю., Минц Г.Е., Оревков В.П. Неразрешимость в конструктивном исчислении предикатов некоторых классов формул, содержащих только одноместные предикатные переменные // Доклады Академии наук. 1965. Т. 163 (2). С. 295—297.

151. Матулис В.А. Два варианта классического исчисления предикатов без структурных правил вывода // Доклады Ан СССР, 1962. Т. 147. №5. С. 1029-1031.

152. Минц Г.Е. Нормализация натуральных выводов и эффективность классического существования // Логический вывод. М., 1979. С. 246—266.

153. Минц Г.Е. Системы Льюиса и система Г(1965—1973) // Фейс Р. Модальная логика. М., 1974. С. 422—509.

154. Минц Г.Е. Теорема об устранимости сечения для релевантных логик // Записки ЛОМИ. Т. 32. 1972. С. 90—97.

155. Непейвода Н.Н. Префиксные семантические таблицы для модальных логик // Многозначные, релевантные и паранепротиворечивые. М., 1984. С. 60—68.

156. Новиков П.С. Конструктивная математическая логика с точки зрения классической. М., 1977.

157. Оревков В.П. Неразрешимость в конструктивном исчислении предикатов класса формул типа —,-i\/3 // Доклады Академии наук. 1965. Т. 163 (3). С. 581—583.

158. Плюшкевичус Р.А. Об одном варианте конструктивного исчисления предикатов без структурных правил вывода // Доклады АН СССР. 1965. Т. 161. №2.

159. Попов В.М. Логический анализ релевантных систем. М., 1979.

160. ПравицД. Натуральный вывод. М., 1997.

161. Серебрянников О.Ф. Эвристические принципы и логические исчисления. М., 1970.

162. Сидоренко Е.А. Релевантность и импликация // Модальные и интенсиональные логики и их применение к проблемам методологии науки. М., 1984. С. А—18.

163. Смирнов В. А. Поиск доказательств в натуральном интуиционистском исчислении предикатов // Логика, методология, философия науки. М., 1995. С. 176—180.

164. Смирнов В А. Представление логических систем с сильной релевантной импликацией в секвенциальной форме // Теория логического вывода. М., 1974. С. 149—159.

165. Смирнов В А. Формальный вывод и логические исчисления М., 1972.

166. Такеути Т. Теория доказательств. М., 1978.

167. Уусталу Т., Ленту с М. Секвенциальные системы модальных исчислений. М., 1989.

168. Шанин Н.А. О конструктивном понимании математических суждений // Труды математического института АН СССР. 1958. Т. 52. С.

169. Шанин Н.А. Об иерархии способов понимания суждений в конструктивной математике // Труды математического института им. В.А. Стеклова. Т. 129. 1973. С. 203—266.

170. Яблонский С.В. Функциональные построения в лг-значной логике // Труды математического института им. В.А. Стеклова. Т. 51. С. 5—142.