Введение к работе
Актуальность темы исследования.
В 50-е гг. наряду с такими известными методами доказательства как аксиоматический, натуральный, секвенциальный получил широкое распространение и применение метод таблиц. Табличный метод имеет фундаментальное значение для теории доказательств, являющейся одной из интенсивно развивающихся областей современной логики. Не меньшее значение имеет табличный метод и для развития исследований по искусственному интеллекту, в частности в такой его области как теория и практика автоматического доказательства теорем.
Однако область применения табличного метода не ограничивается математической логикой и искусственным интеллектом. Метод таблиц широко используется в исследованиях по философии и методологии науки. Табличный метод, в частности, является хорошим средством описания и анализа научной дискуссии. Научная дискуссия, по сути, есть систематический способ отыскания контр-примеров, который приводит либо к опровержению, либо к доказательству некоторого утверждения.
За последнее время появилось большое количество работ, посвященных применению таблиц в различных логических системах. Однако отсутствие систематического обзора истории развития табличного метода диктует необходимость данного исследования.
Степень разработанности темы.
Имеется большое количество работ, посвященных табличному методу, хотя большинство из них принадлежит зарубежным авторам и не переведено на русский язык. Среди фундаментальных исследований, посвященных табличному методу, отметим работы Э.Бета, Дж.Земана, С.Кангера, С.Клини, Р.Смаллиана, М.Фиттинга, С.Крипке.
Применению табличных методов в неклассических логиках посвятили свои работы:
в модальных логиках - С.Крипке, П.И.Быстров, В.Н.Костюк, Н.Н.Непейвода, М.Фиттинг, Э.Бет, С.Кангер, Р.Горе, Ф.Массачи.
в многозначных логиках - С.Сурма, В.Карниелли, Д.Бочвар, В.Фшш, М.Бааз, Г.Фермюллер.
в релевантной логике имеются только работы П.И.Быстрова.
в интуиционистской логике - Э.Бет, М.Фиттинг, М.Феррари, Р.Мильоли, Р.Дюкхофф, С.Крипке, А.Авеллоне, У.Москато, М.Орнаги.
Важным для понимания развития табличных методов и возможностей их применения является вопрос об использовании метода таблиц в области искусственного интеллекта, в частности в области теории и практики автоматического доказательства теорем.
Среди работ, посвященных данной проблеме, отметим работы Э.Бета, Р.Попплестона, И.Кохена, Л.Триллинга, П.Венера, К.Брода, И.Шенфелда, Л.Валлена, С.Ривса, А.Авеллоне, В.Москато, М.Орнаги, Ф.Массачи, П.Мильоли, П.Бонатти, Н.Бааз, Г.Фермюллер.
Однако все вышеперечисленные работы посвящены отдельным проблемам развития табличных методов, поэтому возникла необходимость систематического обзора истории разчития табличного метода и применения его в различных логических системах.
Цель и задачи исследования.
Цель данной диссертации заключается в том, чтобы дать систематический обзор истории развития табличного метода, указать достоинства и недостатки данного метода по сравнению с другими, рассмотреть основные логические системы, к которым применяется данный метод.
В соответствии с этой целью ставятся следующие задачи:
-рассмотреть исторические, философские и логические предпосылки возникновения табличных исчислений;
-произвести сравнительный анализ различных вариантов табличных исчислений;
-определить роль и место табличных исчислений для развития теории доказательств и математической логики;
Методология исследования.
Специфика темы и многообразие, связанных с ней проблем, предопределили выбор метода данного исследования. Методологическим основанием диссертации является метод историко-логической реконструкции и
метод сравнительного анализа, взаимосвязь которых позволит выявить весь спектр проблем.
Для формирования общей концепции исследования плодотворным оказалось обращение к работам отечественных и зарубежных логиков, математиков, историков и философов науки.
Научная новизна диссертации состоит в следующем:
воссоздана целостная история развития табличного метода;
проанализированы и систематизированы различные варианты табличных исчислений;
проанализировано доказательство Основной теоремы с помощью таблиц и указаны основные преимущества данного доказательства по сравнению с доказательством, предложенного Генценом;
указаны философские и логические приоритеты развития и усовершенствования метода таблиц.
На зашиту выносятся следующие положения:
-возникновение табличного метода было обусловлено, во-первых, трудностями в основаниях математики и, во-вторых, развитием теории доказательств;
-табличный метод является наиболее простой и эффективной процедурой поиска доказательства;
-Абстрактная теорема, доказанная Смаллианом, представляет собой обобщенный вариант Основной теоремы Генцена.
Теоретическое и практическое значение диссертации заключается в следующем:
во-первых, работа, посвященная развитию табличных исчислений, восполняет определенный пробел в написании истории современной логики;
во-вторых, материалы диссертации можно использовать в преподавании курсов «История современной логики» и «Теория логического вывода».
Апробация работы: Диссертация обсуждалась на заседании кафедры логики философского факультета Санкт-Петербургского государственного университета. Основные положения диссертации отражены в публикациях автора.
Структура и объем работы определяются ее целями и задачами. Диссертация состоит из введения, двух глав, заключения и списка литературы. Содержание работы изложено на 128 страницах машинописного текста. Список литературы состоит из 131 наименований.