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

Полный текст автореферата диссертации по теме "Алгоритм поиска вывода для систем негативной силлогистики"

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

КРАСНЕНКОВА АНАСТАСИЯ ВЛАДИМИРОВНА

АЛГОРИТМ ПОИСКА ВЫВОДА ДЛЯ СИСТЕМ НЕГАТИВНОЙ СИЛЛОГИСТИКИ

Автореферат

диссертации на соискание ученой степени кандидата философских наук Специальность 09.00.07 — Логика

Москва 2009

003471199

Диссертация выполнена на кафедре логики философского факультета Московского государственного университета им. М.В. Ломоносова

Научный руководитель: Доктор философских наук, профессор

В.А. Бочаров

Официальные оппоненты:

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

К.И. Бахтияров

Кандидат философских наук

А.В. Смирнов

Ведущая организация:

Институт философии РАН, сектор логики

Защита диссертации состоится « 9 » июня 2009 года в 16:00 на заседании диссертационного совета Д 501.001.48 по философским наукам при Московском государственном университете им. М.В. Ломоносова по адресу:

119991, г. Москва, Ломоносовский проспект, д. 27, корп. 4, учебный корпус № 1, философский факультет, ауд. А-518.

С диссертацией можно ознакомиться в читальном зале Отдела диссертаций в Фундаментальной библиотеке МГУ по адресу: Ломоносовский проспект, д. 27, сектор «А», 8 этаж, к. 812.

Автореферат разослан « » ¿"J-Q & 2009 года.

Ученый секретарь Диссертационного совета:

Кандидат философских наук Д.В. Зайцев

Общая характеристика работы

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

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

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

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

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

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

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

Подробный отчет об исследованиях в области автоматического поиска логического вывода (доказательства) проделан В.О. Шангиным1; в частности, В.О. Шангин выделяет следующие этапы в развитии указанной проблематики: средневековый период, где следует отметить такого ученого, как Р. Луллий, впервые реализовавшего идею перебора вариантов; исследования XIX в., начавшиеся с создания первых вычислительных машин и программ для них (Ч. Бэббидж, А. Лавлейс, У. Джевонс и др.) и закончившиеся в 1939 г. созданием первого электронного цифрового компьютера (К. Берри, Дж. Атанасов). Поэтому, начиная примерно с 1945 г., ведется активная работа над написанием программ, реализующих автоматический поиск доказательства. В.О. Шангин отмечает, что именно здесь зародилось два основных направления данных исследований: математическое, позднее вылившееся в метод резолюций, и направление, симулирующее основные интеллектуальные приемы, используемые при построении логического вывода.

Первое направление представляют такие ученые, как М. Дэвис, Дж. Робинсон, Л. Уос, Б. Мелтцер, П. Андреус, В. Бибель и др. Ко второму направлению относятся А. Невел, Дж. К. Шоу, Г. Саймон, М. Минский, Л.М. Нортон и др. На сегодняшний день программы, базирующиеся на методе резолюций, являются самыми эффективными и способными решать очень сложные и объемные задачи (например, программа OTTER), однако за разработками, моделирующими собственно человеческие рассуждения, также стоит большое будущее, в силу важности исследований по робототехнике, нейрофизиологии и т.п.

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

На кафедре логики философского факультета МГУ с начала 90-х гг. прошлого столетия предпринимались успешные попытки построения алгоритмов второго типа (т.е. алгоритмов, моделирующих человеческие рассуждения) для автоматического доказательства теорем в различных исчислениях. Одним из первых был создан алгоритм для натурального исчисления классической логики высказываний (А.Е. Болотов, В.А. Бочаров,

1 Шангин В.О. Автоматический поиск натурального вывода в классической логике предикатов. Дис. ... каия филос. наук : 09.00.07. М„ 2004.

A.Е. Горчаков)2, который получил свою компьютерную реализацию на языке С++. Позже с участием В.О. Шангина и других был сконструирован алгоритм поиска вывода для классической логики предикатов (натуральное исчисление)3. Затем А.Е. Горчаков,

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

В этой связи необходимо упомянуть интерактивный редактор доказательств Deductio5, сконструированный A.B. Смирновым н А.Е. Новодворским, позволяющий работать со многими логическими системами, в том числе и с традиционной силлогистикой.

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

Поисково-дедуктивная система «ЭКСПО», работающая по сходным принципам, что и интерактивный редактор доказательств Deductio7, была разработана А.П. Кулаичевым8 в 80-х гг. XX в. Группа исследователей, участвовавшая в разработке и тестировании данной системы, активно работала с силлогистическим знанием, в частности, с соритами Кэрролла, в состав которых входили сложные термы. Эта система с помощью специальной базы данных могла даже формализовать сориты, введенные в нее на естественном языке, записывая полный набор посылок в виде цепочки конъюнкций, а отдельные посылки — как логическое умножение субъекта и предиката. Программа могла работать как пошагово (пользователь последовательно вводил в нее посылки), так и сразу получать заключение из формализованного сорита. Но силлогистические заключения, как итоговые, так и промежуточные, получались сугубо алгебраическим методом (путем вычеркивания одинаковых термов, вне зависимости от их качества) и, таким образом, механизмы действия

2 Болото« А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода в классической пропозициональной логике // Труды научно-исследовательского семинара логического центра института философии РАН. М: ИФРАН, 1996.

3 Логика и компьютер. Выпуск 5. Пусть докажет компьютер. М.: Наука, 2004.

4 Гэрчаков А.Е., Макаров ВВ., Спирин C.B. О некоторых особенностях построения компьютерной реализации алгоритма

автоматического доказательства теорем в натуральном исчислении, http://www.logic.ru (Логические исследования). M., 1998.

1 Логика и компьютер. Выпуск 3, Доказательство и его поиск (курс логики и компьютерный практикум). М: Наука, 1996. ' См. 5.

' См. 5.

1 Кулаичев А.П., Рамендик Д.М., Славуцкая Л/.В. Диалоговая система подготовки и предъявления зрительной информации // Вопросы психологии. М., 1984, № 4. С. 118—120.

программы не моделировали понятие логического вывода, в отличие от системы Deductio.

Здесь следует также упомянуть К.И. Бахтиярова9, чьим основным направлением исследования является работа над методом арифметизации логики, успешно разрешающего проблему Лейбница — представления умозаключений в виде арифметических вычислений. К.И. Бахтияров ввел логические векторы для представления булевых конституент, записав их компоненты в троичной системе счисления (что соответствует семантической интерпретации силлогистических теорий, по К.И. Бахтиярову). На основе данного метода были построены компьютерные программы, особый интерес из которых для данного исследования представляют программа КЭРРОЛЛ — для решения аристотелевских силлогизмов и программа СОРИТ — для решения соритов со многими терминами. Данные программы реализуют идею так называемого «логического калькулятора». Однако принципы работы данных программ основаны на математических методах и потому не моделируют эвристические приемы, характерные для «естественных» рассуждений.

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

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

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

Сам алгоритм поиска вывода основывается на алгоритме, предложенном В.А. Бочаровым, А.Е. Болотовым, А.Е. Горчаковым для классического исчисления высказываний и на идеях, сформулированных A.B. Смирновым и А.Е. Новодворским10, в силу чего алгоритм позволяет пользователю самостоятельно задавать правила вывода некоторой натуральной силлогистической системы (с использованием специального формализованного языка). Однако после задания правил вывода и корректной постановки задачи алгоритм работает как автоматический генератор доказательств.

9 Бахтияров КИ. Умозаключения на персональных компьютерах. М: Наука, 1989. Бахтияров К.И. Компьютеризация логики // ФИ, М., 1990. Бахтияров КИ. Логические основы компьютеризации умозаключений. М: МИИСП, 1986.

10 См. 5.

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

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

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

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

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

Научная новизна исследования

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

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

идеи доказательства теорем о конечности и адекватности самого алгоритма.

Методологическое основы н источники исследования

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

В диссертационном исследовании использовались формулировки систем натурального вывода, предложенные В.А. Бочаровым, В.И. Маркиным" и др.

В диссертационном исследовании использовались формулировки аксиоматических систем, предложенные A.A. Ильиным12.

В основе представленного в диссертационной работе алгоритма лежит алгоритм, построенный В.А. Бочаровым, А.Е. Болотовым, А.Е. Горчаковым для классического исчисления высказываний, и идеи, сформулированные A.B. Смирновым и А.Е. Новодворским Данные источники оказали существенное влияние на формулировку предложенного в исследовании алгоритма.

Тезисы, выносимые иа защиту:

1. Утверждается, что построенные в диссертационном исследовании силлогистические натуральные исчисления для традиционной негативной силлогистики, фундаментальной негативной силлогистики, негативных силлогистик Больцано, Кэрролла и Аристотеля являются семантически непротиворечивыми и семантически полными.

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

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

" Бочаров В.А, Маркин В.И. Основы логики. Учебник. М: ИНФРА-М, 2002.

12 Ильин A.A. Негативная силлогистика аристотелевского типа. Логика и B.E.K.: Сборник научных трудов: К 90-летию со дня рождения проф. Войшвилло Евгения Казимировича. М: Современные тетради, 2003. Ильин A.A. Силлогистика Б. Больцано. М.: Современные тетради, 2003.

Ильин A.A. Негативная силлогистика Л. Кэрролла // Современная логика: проблемы теории, истории и применения в науке: Материалы VII Общероссийской научной конференции. М, 2002.

Ильин A.A. Системы негативной силлогистики // Современная логика: проблемы теории, истории и применения в науке: Материалы IX Общероссийской научной конференции. СПб., 2006.

Ильин A.A. Негативная фундаментальная силлогистика // Смирновские чтения. 3-я Международная конференция. М., 2001.

Практическая значимость

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

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

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

Основные положения и результаты диссертационного исследования были представлены в виде тезисов доклада на IX Международной научной конференции «Современная логика: проблемы теории, истории и применения в науке» (Санкт-Петербург, 2006 г.).

Также автором были опубликованы две статьи — в «Вестнике Московского Университета» («Алгоритмы вывода для негативных силлогистик». Серия 7. Философия. № 2, 2008 г.) и в Сборнике научных исследований по лотке ИФ РАН («Поиск натурального вывода в системе негативных силлогистик». Выпуск 14, 2007 г.).

Структура диссертации

Диссертация состоит из Введения, трех глав: «Алгоритмизация силлогистики: история вопроса», «Натуральные системы негативной силлогистики», «Алгоритм поиска вывода в натуральных системах негативной силлогистики», — Заключения, Приложений и Литературы.

Основное содержание работы

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

В Первой главе — Алгоритмизация силлогистики: история вопроса — дается исторический обзор исследований по алгоритмизации систем негативных силлогистик. Особенное внимание уделяется современному состоянию дел в области автоматизации силлогистики. Глава состоит из 5 параграфов.

В параграфе 1.1 — Проблема моделирования «естественных» рассуждений — рассматриваются базовые составляющие данного моделирования. Согласно проф. Е.Г. Драгалиной-Черной13, это:

1. Введение новых знаний в базу данных;

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

3. Пополнение знаний на основе эвристических процедур;

4. Систематизация знаний;

5. Приобретение знаний на метауровне;

6. Приобретение знаний в диалоге.

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

1. Пополняется база данных как самих натуральных силлогистических исчислений, «рассмотренных» алгоритмом, так и база данных доказанных и обоснованных в той или иной системе утверждений;

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

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

13 Драгалина-Черная КГ. Логика: от трнвия к инженерии знаний // Научный журнал Московского гуманитарного университета «Знание. Понимание. Умение», № 4, 2006.

вероятностных методов.

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

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

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

В параграфе 1.2 — Восточные школы: силлогистика джайное — подробно исследуется одна из древнейших силлогистических систем с негативными терминами — силлогистика джайнов14 — и отмечаются ее ключевые моменты: наличие трех типов терминов (положительные, отрицательные, а также т.н. «неописуемое», т.е. неопределенный термин) и присутствие вероятностного оператора «некоторым образом».

В параграфе 1.3 — Античная мысль — последовательно анализируются все этапы античной мысли, связанные с развитием негативной силлогистики, начиная с Аристотеля15, который первым различил отрицательный предикат и отрицательный термин, заканчивая перипатетиками и римскими стоиками16, которые ввели операцию превращения, а также исследовали довольно сложные силлогизмы с отрицательными терминами, в частности, такие, где квантифицировался предикат суждения.

В параграфе 1.4 — Средневековая силлогистика — исследуются труды средневековых логиков в области негативной силлогистики.

Отмечается, что на основе исследований ученых Средневековья (У. Оккам и др.) современными логиками (В.И. Маркин) были построены интересные системы негативной силлогистики — к примеру, система сингулярной негативной силлогистики т.н. «оккамовского» типа", где операция терминного отрицания применяется и к субъекту, и к предикату, в том числе, и тогда, когда они представляют собой сингулярные (или

14 Изложение материала ведется по книге: Стяжкин И.И. Формирование математической логики. М.: Наука, 1967.

" Аристотель. «Первая Аналитика». Первая книга, гл. 46. М.: Мысль, 1978.

16 См. 14.

17 Маркин В.И. Силлогистические теории в современной логике. М.: Издательство Московского университета, 1991.

единичные) термины.

Исследователи Средневековья, в частности, П. Испанский, Р. Луллий, У.Оккам и др. продолжали разрабатывать операцию обращения предиката, ввели операцию внешнего отрицания силлогистических высказываний, а также применяли совместное сочетание данных операций, например, при работе с переходом вида -,(Sa~P) О SiP.

В параграфе 1.5 — Силлогистические исследования Нового Времени — подробным образом рассматриваются труды ученых этого периода. Особенно большое внимание уделяется Г. Лейбницу, так как именно он первым предпринял попытку алгоритмизации силлогистики18. Алгоритмизация осуществлялась им за счет арифметизации — ученый провел соответствие между рядом целых чисел и простыми силлогистическими терминами. Но, в силу того что Лейбниц не обнаружил эффективной стратегии поиска опровергающих некорректные силлогистические выводимости пар, он не смог осуществить до конца алгоритмизацию силлогистики. Современные логики (К.И. Бахтияров) успешно построили алгоритм на базе этой идеи и реализовали его в виде компьютерных программ КЭРРОЛЛ, БУЛЬ и СОРИТ, активно опирающихся на векторную семантику трехзначной логики19.

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

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

Знаменитые сориты Кэрролла, содержащие до 20 посылок, имеют в своем составе не только негативные, но и расширенные за счет операций пересечения и объединения термины и способны весьма «озадачить» современный компьютер.

В параграфе 1.6 — Современные исследования в области негативной силлогистики — рассматриваются современные исследования в данной сфере. В.А. Бочаровым, В.И. Маркиным22, A.A. Ильиным были аксиоматизированы интересные силлогистические системы — традиционная, фундаментальная, аристотелевская, силлогистика Больцано и Кэрролла; сингулярные негативные силлогистики оккамовского и

11 Лейбниц Г.В. Сочинения в четырех томах. Том 3. «Правила, по которым с помощью чисел можно судить о правильности выводов, о формах и модусах категорических силлогизмов». М: Мысль, 1984.

19 См. 9.

20 См. 14.

21 Кэрролл Л. История с узелками. М.: Мир, 2000.

22 Маркин В.И. Силлогистические теории в современной логике. М: Издательство Московского университета, 1991.

аристотелевского типа — и с помощью метода В.М. Попова (использование специальных аналитических таблиц) доказана их разрешимость23. Были получены также результаты об их непротиворечивости п полноте. A.A. Ильиным24 (с использованием критерия В.А. Смирнова) была доказана погружаемость традиционной негативной силлогистики, силлогистик Больцано, Кэрролла и Аристотеля в НФС. Также A.A. Ильин25 доказал погружаемость НФС в ОФС. Поэтому, в силу данных результатов, а также результатов В.И. Маркина о погружаемости ОФС в логику предикатов26, базовые метатеоретические свойства данных систем могут обосновываться через логику предикатов.

В параграфе 1.7 — История алгоритмизации систем негативной силлогистики — приводятся краткий обзор алгоритмов в области негативной силлогистики.

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

Даже такое обширное исследование по моделированию поиска вывода в различных областях современной логики, как27, (на базе которого была построена программа Deductio) рассматривает силлогистику либо в ракурсе других теорий: исчисления предикатов (в т.ч. и прикладного), исчисления высказываний, булевой алгебры, — либо формулирует силлогистику вообще без использования исчисления высказываний (без логических связок) и поэтому с очень сложной формулировкой правила сведения к абсурду.

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

23 Бочаров В.А Аристотель и традиционная логика. М.: Издательство Московского университета, 1984.

24 Ильин A.A. Негативная силлогистика аристотелевского типа. Логика и В.Е.К.: Сборник научных трудов: К 90-летию со дня рождения проф. Войшвилло Евгения Казимировича. М.: Современные тетради, 2003. Ильин A.A. Силлогистика Б. Больцано. М: Современные тетради, 2003.

Ильин А.А Негативная силлогистика Л. Кэрролла // Современная логика: проблемы теории, истории и применения в науке: Материалы VII Общероссийской научной конференции. М , 2002.

Ильин A.A. Системы негативной силлогистики // Современная логика: проблемы теории, истории и применения в науке: Материалы IX Общероссийской научной конференции. СПб., 2006.

Ильин A.A. Негативная фундаментальная силлогистика // Тр. науч.-исслед. семинара Логич. центра Ин-та философии РАН. Вып. 15. М., 2000.

Маркин В.И. Обобщенная позитивная силлогистика //Логические исследования. Вып. 6. М.: РОССПЭН, 1999. Логика и компьютер. Выпуск 3. Доказательство и его поиск (курс логики и компьютерный практикум). М.: Наука, 1996. " См. 8.

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

Следует еще раз упомянуть о разработках К.И. Бахтиярова, основанных на троичном векторном счислении; на основе данных разработок были построены не только специальные программы по решению силлогизмов и соритов, но и интерактивная обучающая игра КЭРРОЛЛ.

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

Во Второй главе — Анализ систем негативной силлогистики — дается подробный анализ натуральных субординатных систем негативной силлогистики, базирующихся на системе НВ, предложенной В.А. Бочаровым и В.И. Маркиным29. Показывается, что все рассматриваемые в работе системы НВ обладают свойством семантической непротиворечивости и полноты. Глава состоит из 6 параграфов.

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

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

н Бочаров В.А. Маркин В.И. Основы логики. Учебник. М.: ИНФРА-М, 2002.

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

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

Б, Р, М, О, БР[, Мь (¿1, ... — список силлогистических переменных.

а, е, о — логические (силлогистические) операторы.

-1 — логические (пропозициональные) константы.

--логическая (силлогистическая) константа.

(,) — технические символы;

Будем использовать в качестве метапеременных, пробегающих по множеству индивидных силлогистических переменных, бесконечный список вида X, У, Ъ, Хь У[, '/.¡, Х2...

Будем использовать в качестве метапеременных, пробегающих по множеству силлогистических формул, бесконечный список вида А, В, С, А|, В\, Сь Аг...

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

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

1. Любая силлогистическая переменная есть силлогистический терм.

2. Если X — силлогистический терм, то ~Х — силлогистический терм.

3. Ничто иное не есть силлогистический терм.

4. Понятие силлогистической формулы.

5. Если X и У—■ термы, то ХаУ, ХеУ, Х1У, ХоУ — силлогистические формулы.

6. Если А — силлогистическая формула, то (—>А) — силлогистическая формула.

7. Если А, В — силлогистические формулы, то (А&В), (АуВ), (АэВ) — силлогистические формулы.

8. Ничто иное не является силлогистической формулой.

Внешние формульные скобки договоримся опускать.

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

Формулировка правил вывода всех рассматриваемых систем ориентирована на

15

программную реализацию алгоритма, и поэтому критерий независимости правил опускается (большее количество правил позволяет сократить алгоритмический перебор).

В параграфе 2.2 — Натуральная система негативной традиционной силлогистики (нТС) —■ задаются правила вывода в данной силлогистической системе.

1.ВНСЭВ 2.А/-А V В З.ВНАУВ 4. А&ВНА 5. А&ВНВ 6 .А.ВНА&В 7. АУВ, -•В НА 8.АЭВ, АНВ 9.-\АУВ) Н-А &-В 10. —А НА 11. Н ХаХ 12. -ХаУ Н ХоУ 13. -ХоУ Н ХаУ

14. -Х1У Н ХеУ 15. -ХеУ Н Х1У 16. ХоУ н -ХаУ 17. ХеУ н -ОйУ 18. Хе-У Н ХаУ 19. Ха~У Н ХеУ 20. Хо~У Н ХГУ 21.Х|~УнХоУ 22. ХаУ Н Х1У 23. ХеУ Н УеХ 24. Х1У н У1Х 25. ХаУ Н Хе~У 26. —ХаУ Н ХаУ 27. —ХоУ Н ХоУ 28. -В, В Н -С 29. Хаг, гаУ Н ХаУ 30. Хэ1, 2еУ Н ХеУ

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

Выводом формулы А из множества формул Г в системе нТС называется непустая последовательность формул, отвечающая следующим условиям:

1. каждая формула данной последовательности есть либо одна из формул множества Г (посылка), либо допущение (самостоятельно введенная нами посылка), либо получена по одному из правил вывода системы нТС; м. если в выводе применялись правила № 1 и № 28, то все формулы вывода, начиная с последнего допущения и вплоть до результата применения одного из данных правил, исключаются из дальнейшего процесса построения вывода; ш. последняя формула данной последовательности графически равна А; ¡V. все допущения в уже построенном выводе должны быть исключены. Доказательством в нТС будем называть вывод формулы А из пустого множества формул Г.

Теоремой называется формула, для которой имеется доказательство. Далее приводится аксиоматическая формулировка указанной системы негативной силлогистики30. Назовем ее кратко ТС.

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

30 Здесь и далее формулировки аксиоматических систем принадлежат Ильину А. А.

Ильин А.А. Системы негативной силлогистики // Современная логика: проблемы теории, истории и применения в науке: Материалы IX Общероссийской научной конференции. СПб., 2006.

семантическая полнота и непротиворечивость31, то данные свойства будут справедливы и относительно пТС.

Доказывается сначала Лемма 2.2.1: vA(r тсн А => Г „тснА). Для доказательства Леммы 2.2.1 необходимо и достаточно показать, что все аксиомы ТС являются теоремами нТС, а также, что правило modus ponens сохраняется в иТС. Доказательство данной Леммы приведено в Приложении I диссертационного исследования.

Затем доказывается Лемма 2.2.2: v А(Г Н|С |- А => Г ТС|-Л). Лемма 2.2.2 доказывается методом возвратной математической индукции. Доказательство данной Леммы приведено во Второй главе диссертационного исследования, а также в Приложении 2 диссертационной работы.

Из Лемм 2.2.1 и 2.2.2. автоматически следует Метатеорема 2.2.1:

V А(Г „тс ЬАоГ нтс!=А).

В параграфе 2.3 — Натуральная система негативной силлогистики Больцано (нБС) — задаются правила вывода в данной силлогистической системе.

l.BhCDB l.AhAvB l.BhAvB 4. А & В Ь А 5.А&ВНВ

6 ,A,BhA&B 7. AvB,-Bl-A 8. АЭВ, А I-В 9.-(AVB) I--А &-В

10. -"А 1- А 11. XiY I- ХаХ 12. XaY I- XiY 13. XiY I- YiX

14. Xe~Y I- XaY 15. Xa~Y h XeY 16. Xo~Y h XiY 17. Xi~Y H XoY

18. —XoY I- XoY 19. —XaY I- XaY 20. —XeY H XeY 21. —XeY I- -XeY

22. —XaY t- -XaY 23. —XiY н -XiY 24. —XoY H -XoY 25. XaY н Xe~Y

26. XoY I- Xi~Y 27. XeY I- Xa~Y 28. XeY, YiY I- YeX

29. XaZ, ZaY h XaY 30. XaZ, ZeY h XeY 31. -Д В h -C 32. XeY h- XiX

33. XoY t- XiX 34. -XiX h ~Xi~X 35. -~Xi~X I- XiX

36. -XeY, XiX I- XiY 37. -XiY, XiX н XeY 38. -XaY, XiX h- XoY

3 9. -XoY, XiX h XaY 40. XeY Ь -XiY 41. XoY I- -XaY

Содержание и ход доказательств параграфа 2.3 совершенно аналогичны структуре и доказательствам параграфа 2.2, с той лишь разницей, что идет опора на аксиоматику системы БС32, которая так же, как и при работе с системой ТС, постулируется явным образом.

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

" См. 24.

32 Ильин A.A. Силлогистика Б. Больцано. М.: Современные тетради, 2003.

семантическая полнота и непротиворечивость33, то данные свойства будут справедливы и относительно нБС.

Так же, как и для систем ТС и нТС, доказывается Лемма 2.3.1 и 2.3.2 (соответствующие выкладки приведены в Приложениях 3 и 4 диссертационного исследования), а затем утверждается, что доказанной является Метатеорема 2.3.1:

УАСГивсНА» Г нбс (=А).

В параграфе 2.4 — Натуральная система негативной силлогистики Кэрролла (нКС) — задаются правила вывода в данной силлогистической системе.

1 .ВНСЭВ г.АнАУВ г.ВНАУВ 4. А&ВЬА 5. А&ВНВ 6. А, В Н А & В 7. АУВ,-ВНА 8. АЭВ.АЬВ 9.-(АУВ) Н-А&-В 10. -"А НА 11. Х1У Н ХаХ 12. ХеУ н УеХ 13. Х1У I- У1Х 14. ХаУ н Х1У 15. Ха~У I- ХеУ 16. Хг~У н ХоУ 17. Хо~У И Х1У 18. Хе~У, XIX н ХаУ 19. -XIX I—Х1~Х 20. —~Х1~Х ь XIX 21. ХоУ н XIX 22. ~*В, В Н~*С 23. —ХаУ I- ХаУ 24. —ХеУ Н ХеУ 25. —ХоУ Н ХоУ 26 .-—ХаУ Н -ХаУ 27. —ХоУ Н -■ХоУ 28. ХаУ Н Хе~У 29. ХоУ I- Х1~У 30. ХеУ, XIXI- Ха-У 31. Х<а, гаУ I- ХаУ 32. Хаг, геУ У- ХеУ 33. -ХеУ н Х1У 34. -Х1У Ь ХеУ 35. -ХаУ, XIX (- ХоУ 36. -ХоУ, XIX Н ХаУ 37. ХеУ н -Х1У 38. ХоУ I- -ХаУ

Содержание и ход доказательств параграфа 2.4 совершенно аналогичны структуре и доказательствам параграфа 2.2, с той лишь разницей, что идет опора на аксиоматику системы КС34, которая так же, как и при работе с системой ТС, постулируется явным образом.

Для доказательства семантической непротиворечивости и полноты системы нКС доказывается дедуктивная эквивалентность систем КС и нКС. Их дедуктивная эквивалентность означает тот факт, что они описывают одно и то же. Так как относительно системы КС посредством ее погружения в логику предикатов доказана семантическая полнота и непротиворечивость35, то данные свойства будут справедливы и относительно нКС.

Так же, как и для систем ТС и нТС, доказывается Лемма 2.4.1 и 2.4.2 (соответствующие выкладки приведены в Приложениях 5 и 6 диссертационного исследования), а затем утверждается, что доказанной является Метатеорема 2.4.1:

V А(Г яке I- А <=> Г «кс^ А).

" См. 24

34 Ильин А.А Негативная силлогистика Л. Кэрролла // Современная логика: проблемы теории, истории и применения в науке:

Материалы VII Общероссийской научной конференции. М, 2002. " См. 24.

В параграфе 2.5 — Натуральная система негативной силлогистики Аристотеля (нАС) — задаются правила вывода в данной силлогистической системе.

\BhCDB 2 АНАУВ Ъ. В Н А V В 4. А & В Н А 5. А&ВнВ

6. А, В Н А & В 7. А V В, -В I- А 8. А Э В, А Н В 9. -(А V В) I- -А & -В 10.—АН А 11.Х1УНУ1Х 12. ХеУнУеХ 13. ХаУ Н Х1У 14. ХГУ Н ХаХ 15. ХаУ I- Хе~У 16. Ха~У Н ХеУ 17. Х1~У н ХоУ 18. Хе~У, XIX н ХаУ 19. Хо~У, Х\Х Н Х1У 20. Хе—У I- ХеУ 21. Хо—У Н ХоУ 22. —ХоУ I- ХоУ 23. —ХаУ Н ХаУ 24. ХоУ, XIX I- Х1~У 25. ХеУ, XIX Н Ха~У

26 -»X I- ~Х(~Х 27. —М-Х н XIX 28. -В, В И -С 29. Хаг, Н ХаУ 30. ХгИ, 2еУ н ХеУ 31. -ХеУ н Х1У 32. -ХаУ н ХоУ 33. -Х1УI- ХеУ

34. -ХоУ I- ХаУ 35. ХеУ Н -Х1У 36. ХоУ I- -ХаУ

Содержание и ход доказательств параграфа 2.5 совершенно аналогичны структуре и доказательствам параграфа 2.2, с той лишь разницей, что идет опора на аксиоматику системы АС36, которая так же, как и при работе с системой ТС, постулируется явным образом.

Для доказательства семантической непротиворечивости и полноты системы нАС доказывается дедуктивная эквивалентность систем АС и нАС. Их дедуктивная эквивалентность будет означать тот факт, что они описывают одно и то же. Так как относительно системы АС посредством ее погружения в логику предикатов доказана семантическая полнота и непротиворечивость37, то данные свойства будут справедливы и относительно нАС.

Так же, как и для систем ТС и нТС, доказывается Лемма 2.5.1 и 2.5.2 (соответствующие выкладки приведены в Приложениях 7 и 8 диссертационного исследования), а затем утверждается, что доказанной является Метатеорема 2.5.1:

V А(Г„ас Н А о Г „АС*=А).

В параграфе 2.6 — Натуральная система фундаментальной негативной силлогистики (нФС) — задаются правила вывода в данной силлогистической системе.

1 .В ¡-СЭВ 2.АНАУВ г.ВЬ-АУВ 4. А&ВНА 5. А&ВНВ б.А.ВНА&В 7. А V В,-В НА 8.АЭВ,АНВ 9.-(А V В) Н-А &-В 10. —А НА 11. Н ХаХ 12. Х1У Н У1Х 13.ХеУ Н УеХ 14.Х1У Н XIX 15. Хе~У Н ХаУ 16. Ха~У Н ХеУ 17. Х1~У Н ХоУ 18. Хо~У Н Х1У 19. —ХаУ Н ХаУ 20. —ХоУ Н ХоУ 21. ХаУ Н Хе~У 22. ХоУ Н Х1~У 23. Хаг, 1аУ Н ХаУ 24. ХаЪ, 2еУ Н ХеУ 25. -XIX Н ~Х1~Х

26. —Х1~Х Н XIX 27. -Д В Н -С 28. -ХеУ Н Х1У 29. -ХоУ Н ХаУ

36 Ильин АЛ. Негативная силлогистика аристотелевского типа. Логика и В.Е.К.: Сборник научных трудов: К 90-летию со дня рождения проф. Войшвилло Евгения Казимировича. М: Современные тетради, 2003.

37 См. 24.

30.-Х^нХеУ 31. -\ХаУ I- ХоУ 32. ХеУ Н-Х1У 33. ХоУ 1- -ХаУ

Содержание и ход доказательств параграфа 2.6 совершенно аналогичны структуре и доказательствам параграфа 2.2, с той лишь разницей, что идет опора на аксиоматику системы ФС38, которая так же, как и при работе с системой ТС, постулируется явным образом.

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

Так же, как и для систем ТС и вТС, доказываем Леммы 2.6.1 и 2.6.2 (соответствующие выкладки приведены в Приложениях 9 и 10 диссертационного исследования), а затем утверждаем, что доказанной является Метатеорема 2.6.1:

V А(Гнфс Н А <=> Г „ФС1=А).

В Третьей главе — Описание алгоритма для натуральных систем негативных силлогистик — детально описывается указанный алгоритм поиска вывода, разъясняются главные принципы его работы, описываются методы, использованные при его программной реализации, приводится пример работы алгоритма, выполненный построенным программным модулем. Глава состоит из 6 параграфов.

В параграфе ЗА — Сущность алгоритма — описываются фундаментальные принципы, лежащие в основе его работы.

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

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

31 Ильин А.А. Негативная фундаментальная силлогистика // Смирновские чтения. 3-я Международная конференция. М., 2001.

39 См. 25.

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

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

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

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

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

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

(тогда он будет семантически полным).

Далее показывается, каким образом алгоритм осуществляет обработку введенных в него правил вывода.

Обработка правил вывода системы, введенных пользователем в текстовый редактор— Блокнот или MS Word, — происходит с опорой на идеи В.А. Смирнова40. Это означает, что правила вывода той или иной системы делятся на аналитические и синтетические.

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

Затем разъясняется понятие пропозициональной и терминной сложности формулы.

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

1. ф(А) = <p(_L) = 0, где А — произвольная простая формула любой степени

терминной сложности, а ± — обозначение для противоречия (необходимо для работы

с правилом введения отрицания).

2. ф(-,А) = ф(А) + 0,5;

3. ф(А=> В) = ф(А & В) = ф(А) + ф(В) + 1;

4. ф(А v В) = ф(А) + ф(В) + 1,5

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

Определяется с помощью рекурсии (п.п. 1 — 3) и индукции (п.п. 4 — 5):

I. y(XoY) = 0, где X, У — простые силлогистические термы, а о — одна из допустимых силлогистических констант;

40 Смирнов В.А. Теория логического вывода. М.: РОССПЭН, 2000.

2. ц/(ос°~Р) = у(а°Р) + 1. где а, р — произвольные силлогистические термы;

3. ф(~аор) = \|/(а°Р) + 1;

4. = ч»(А), где А — произвольная формула;

5. у(А & В) = у(А п В) = у(А V В) = (|/(А) + у(В), где А и В — произвольные формулы.

На множестве всех формул определяется отношение частичного порядка, в силу чего алгоритм успешно сортирует правила и начинает свою работу.

Дополнительно отмечается, что синтетические правила вывода делятся алгоритмом на прямые и непрямые. Прямые синтетические правила вывода — это те п.в., которые не используются для построения дополнительного подвывода и не содержат метатерма С. Непрямые правила — это те, которые, наоборот, используются для построения дополнительных подвыводов и содержат метатерм С (например, правила №№ 1 и 28 в системе нТС).

Все синтетические правила вывода, не имеющие подформулы С, автоматически классифицируются как прямые синтетические правила вывода (например, правило № 3 в системе нТС).

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

Аналитические правила вывода, в свою очередь, делятся на правила вывода с посылками (правило № 8 в системе нТС) и «беспосылочные» правила вывода («беспосылочным», к примеру, является правило вывода ХаХ).

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

Стек вывода (далее — СВ) представляет собой натуральный вывод в той или иной исследуемой силлогистической системе.

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

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

Затем описываются алгоритмические процедуры.

Процедура 1, или процедура достижимости

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

Процедура 2, или процедура унификации

Работает с текущей целью, содержащей метапеременные. Процедура 2 пытается найти кортеж формул, являющийся результатом правильной подстановки в выражение, содержащее метапеременные. Например, когда текущей целью является противоречие, записываемое у нас как <-"В, В>, процедура 2 ищет в СВ пары неисключенных формул, являющиеся результатом правильной подстановки в с-В, В>, например «c-SaP, SaP>. В случае неудачи процедура 2 выдает пустой кортеж.

Процедура 3, или процедура применения беспосылочных аналитических правил вывода

Процедура 3 применяет беспосылочные правила вывода, последовательно подставляя все простые термы обосновываемой выводимости или теоремы в беспосылочные правила и добавляя полученные формулы в СВ.

Процедура 4, или процедура применения аналитических правил с посылками

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

Здесь также действуют описанные выше эвристики допустимого уровня сложности формулы.

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

Процедура S, или процедура порождении новых целей с помощью синтетических

правил вывода

Данная процедура строит новые цели меньшей степени пропозициональной сложности, чем формулы-цели, предшествующие ей. Процедура 5 начинает свою работу, когда главная цель — теорема или формула, которую необходимо вывести из посылок, — не достижима непосредственно, при помощи процедур 3 и 4. Процедура 5 меняет местами посылки и заключение в синтетических п.в. и затем пытается последовательно применить данные правила к текущей цели. Если некоторое синтетическое п.в. оказалось применимо к текущей цели, то результат его применения, являющийся либо формулой, либо противоречием (например, в случае применения правила № 28 в системе вТС), добавляется в СЦ.

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

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

Процедура 6, или процедура построении новых целей по формулам св

Процедура 6 формирует новые вспомогательные цели на базе формул СВ и аналитических правил вывода с количеством посылок, превосходящим или равным 2 (обычно это правила исключения импликации и дизъюнкции). Процедура 6 включается в работу, когда процедура 5 естественным образом остановилась. Процедура 6 просматривает аналитические правила вывода и отбирает те из них, где число посылок больше или равно 2; затем она производит последовательную подстановку в выбранные правила, используя формулы СВ. При помощи функции <р данная процедура выбирает посылку наименьшей пропозициональной сложности и делает ее новой текущей целью (например, при работе с результатом подстановки в правило исключения дизъюнкции А V В, -А н В — БаР V БоР, -.ЭаР I- БоР — такой целью становится формула -.БаР).

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

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

Процедура 7, или процедура работы с достигнутыми целями

Процедура 7 оперирует с достигнутыми целями СЦ. Она применяет синтетические п. в. и таким образом осуществляет построение вывода.

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

Если алгоритм добавил в СВ главную цель и СЦ представляет собой пустой список, то теорема объявляется доказанной (выводимость обоснованной), и программа переходит к построению результирующего вывода.

Процедура 8, или процедура работы с недостигнутыми целями

Процедура 8 начинает свою работу, когда текущая цель недостижима

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

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

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

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

Итак, процедура 8 тестирует все возможные варианты получения некоторой цели, конструируя таким образом древовидную структуру целей. Тупиковые ветви удаляются из СЦ и СВ.

Если алгоритм удалил главную цель, то формула объявляется опровергнутой. Происходит выход из алгоритма.

Процедура 9, или процедура построения результирующего вывода

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

Для этого она активно использует указанную выше строку Static, куда были записаны номера всех добавленных в СВ формул. Она «просеивает» лишние формулы и оставляет только те формулы, которые действительно использовались при построении вывода.

В параграфе 3.3 — Общее описание алгоритма — описывается целостная работа алгоритма.

I. Сначала применяется процедура 1, или процедура достижимости (т.е. алгоритм проверяет, есть ли у нас тривиальная выводимость). Если она дала положительный результат, то переход к VIII. В случае отрицательного результата происходит либо переход к процедуре 3 (при начальной конфигурации работы алгоритма), либо происходит возврат в ту процедуру, откуда процедура 1 была вызвана (на более «поздних» этапах работы алгоритма).

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

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

IV. В действие вступает процедура 5. После каждого ее применения осуществляется переход к I, а в случае, когда она добавляет в СВ посылку нового подвывода по непрямому п.в., алгоритм переходит к III. В случае недостижимости текущей цели процедура 5 работает до тех пор, пока текущей целью не станет противоречие. Тогда алгоритм переходит к V.

V. Применяется процедура 2. Если процедура 2 обнаружила в СВ противоречие, то переход к VIII. В противном случае переход к VI.

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

VII. В действие включается процедура 8. Если к цели, имеющей вид формулы, были применены не все допустимые правила, то алгоритм переходит к IV. В противном случае она работает до тех пор, пока либо не найдет конструктивную ветвь построения вывода (доказательства), либо пока не опровергнет главную цель из СЦ. Тогда процедура 8 прекращает свою работу, а алгоритм объявляет теорему не доказуемой или выводимость необоснованной.

VIII. В данном пункте описывается действие процедуры 7.

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

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

Когда цель является конъюнкцией (в нашей интерпретации — кортежем формул), то новой целью (если достигнута первая его компонента) становится его второй элемент и осуществляется переход к I.

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

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

IX.

IX. Применяется процедура 9 так, как описано выше.

В параграфе 3.4 — Пример работы алгоритма — подробным образом анализируется теорема н ((SaM v —.SiS) & (МаР v -,MiM)) э (Se~P v —.SiS) системы нБС при эвристике нулевого уровня сложности.

В параграфе 3.5 — О программной реализации — говорится о том, что программа написана на языке Object Pascal (система программирования Delphi). Данная система обладает богатыми программистскими возможностями и обширными динамическими библиотеками программных средств.

Программная реализация активно опирается на генетический алгоритм.

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

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

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

доступной даже неискушенному пользователю.

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

На Рисунке приводится пример работы программы. Программный модуль доказывает теорему н((Ма-Ру-8а8)&(5е~Му-РаР))э(5а---Ру-БаЭ) в системе нТС (см. стр. 21).

В параграфе 3.6 — Перспективы развития алгоритма — говорится о возможных направлениях модификации и усовершенствования как самого алгоритма, так и программного модуля, построенного на его основе.

маг«

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

Конечность алгоритма доказывается через доказательство конечности СВ, конечности СЦ и конечности ветвления СЦ.

Кратко изложены размышления о конечности алгоритма.

Показана конечность СВ.

Число посылок у нас конечно по определению.

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

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

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

Доказывается конечность СЦ.

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

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

пропозициональной сложности предыдущей. Анализ любой цели, в случае ее недостижимости, с необходимостью заканчивается целью-противоречием, пропозициональная сложность которой равна 0: данная цель есть не что иное, как логическая константа 1, а <р(±). Следовательно, применительно к порождению новых целей на базе предыдущих у нас не может возникнуть ситуации, когда алгоритм порождает потенциально бесконечный список целей, приводящий к тому, что алгоритм не может закончить свою работу (бесконечные циклы).

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

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

Таким образом, мы расписали случай для достижимой (доказуемой) формулы.

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

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

Данный алгоритм построен таким образом, что в случае недостижимости той или иной текущей цели, он пытается получить их альтернативным путем, т.е. посредством еще не применявшихся к ним синтетических правил. Если такие правила нашлись, то повторяется описанный выше конечный цикл. Отмечено, что алгоритм ведет строгий контроль над применением данных правил — они применяются последовательно и по порядку, поэтому абсолютно исключена ситуация, когда алгоритм «зацикливается», постоянно применяя одно и то же правило к одной и той же текущей цели. Здесь же отмечено, что все формулы СВ, относящиеся к тупиковой ветви доказательства (вывода), удаляются из СВ. Если же все

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

Таким образом, показана конечность СЦ.

Доказывается конечность ветвления СЦ. Здесь под ветвлением понимается набор всех возможных путей получения той или иной цели. Корнем полученной древовидной структуры считается главная цель, а листьями — последние минимальные цели для каждой альтернативы.

В силу того, что число правил вывода конечно, и число всех целей в СЦ конечно, и анализ каждой цели с необходимостью порождает конечную последовательность подцелей, и количество вспомогательных целей, полученных по аналитическим п.в. и сопоставляемых каждой «синтетической» ветви, тоже конечно, то число всех возможных ветвей доказательства также с необходимостью будет конечным —■ у нас никогда не возникнет бесконечного цикла в ширину. Также не возникнет бесконечного цикла в глубину при работе с каждой из ветвей: строя нити доказательства (вывода) вглубь с помощью целей, полученных по аналитическим п.в., в итоге мы все равно получаем нити конечной длины. Действительно, так как число таких вспомогательных целей конечно и из каждой выходит только конечное множество ветвей-подцелей, то число всех возможных вариантов поиска вывода в данном случае тоже будет конечным.

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

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

Доказана конечность ветвления СЦ.

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

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

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

Похожий метод доказательства такого рода утверждений использовался Е.Д. Смирновой41.

Семантическая полнота алгоритма доказана построением множества Хинтикки для рассматриваемых в работе силлогистических систем.

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

о обобщение предложенного алгоритма и метода доказательства метатеоремы об адекватности на натуральные системы: расширенной силлогистики, на сингулярные негативные силлогистики оккамовского и аристотелевского типа, а также на обобщенные и интенсиональные силлогистики;

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

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

41 См.: Смирнова Е.Д. Логика и философия. Серия «Научная философия». М: РОССПЭН, 1996. С. 97, 99.

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

Красненкова A.B. Алгоритмы вывода для негативных силлогистик // Вестник Московского Университета. Серия 7. Философия. № 2. М.: Издательство МГУ, 2008. — 0,3 п.л.

Красненкова A.B. Поиск натурального вывода в системе негативных силлогистик // Логические исследования. Вып. 14. М.: Наука, 2007. — 1 п.л.

Подписано в печать 06.05.09 Формат 60x88 1/16. Объем 1 пл. Тираж 50 экз. Заказ № 873 Отпечатано в ООО «Соцветие красок» 119991 г.Москва, Ленинские горы, д.1 Главное здание МГУ, к. А-102

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

ВВЕДЕНИЕ.4

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

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

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

Научная новизна исследования.

Тезисы, выносимые на защиту.

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

Практическая значимость.

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

Глава 1. АЛГОРИТМИЗАЦИЯ СИЛЛОГИСТИКИ: ИСТОРИЯ ВОПРОСА.11

§1. Проблема моделирования (симуляции) «естественных» рассуждений.11

§2. Восточные школы: силлогистика джайнов.13

§3. Античная мысль.14

Силлогистические исследования Аристотеля.14

Перипатетики.

Римский стоицизм.

§4. Средневековая силлогистика.17

§5. Силлогистические исследования Нового времени.18

Труды по силлогистике Г. Лейбница.18

Система Г. Холланда.21

Работы С. Маймона, Ф. Кастильона, Ж. Жергонна.22

Логические идеи А. де Моргана.

Силлогистические исследования Л. Кэрролла.24

§6. Современные исследования в области негативной силлогистики.26

§7. История алгоритмизации систем негативной силлогистики.27

Глава 2. АНАЛИЗ СИСТЕМ НЕГАТИВНОЙ СИЛЛОГИСТИКИ.29

§1. Обобщенная формулировка исследуемых систем негативной силлогистики.29

§2. Натуральная система негативной традиционной силлогистики (нТС).32

§3. Натуральная система негативной силлогистики Больцано (нБС).39

§4. Натуральная система негативной силлогистики Кэрролла (нКС).40

§5 Натуральная система негативной силлогистики Аристотеля (нАС).42

§6. Натуральная система негативной фундаментальной силлогистики (нФС).44

Глава 3. ОПИСАНИЕ АЛГОРИТМА ДЛЯ НАТУРАЛЬНЫХ СИСТЕМ НЕГАТИВНЫХ СИЛЛОГИСТИК 46

§1. Сущность алгоритма.

§2. Общая характеристика алгоритма.47

Формализованный язык, используемый алгоритмом.47

Эвристики алгоритма.48

Алгоритмические процедуры.54

§3. Общее описание алгоритма.61

§4. Пример работы алгоритма.63

§5. О программной реализации.68

§6. Перспективы развития алгоритма.70

Введение диссертации2009 год, автореферат по философии, Красненкова, Анастасия Владимировна

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

Вопросы, связанные с поиском логического вывода, составляют ядро многих логических исследований. Как отмечает В. О. Шангин1, «бурное развитие данной проблематики в XX веке стимулировали, с одной стороны, фундаментальные работы Г. Генцена и Ж. Эрбрана и, с другой, появление ЭВМ. Возможность использования ЭВМ в процессе поиска логического вывода привела к появлению проблематики автоматического (машинного) поиска логического вывода».

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

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

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

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

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

1 Шангин В.О. Автоматических поиск натурального вывода в классической логике предикатов. Диссертация на соискание ученой степени кандидата философских наук. Специальность 09.00.07 - Логика. Москва, 2004. Стр. 3.

2 Подробнее см. Нильсон Н. Искусственный интеллект. Методы поиска решений. Москва, «Мир», 1973.

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

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

Подробный отчет об исследованиях в области автоматического поиска логичел ского вывода проделан В. О. Шангиным, в частности В. О. Шангин выделяет следующие главные этапы в развитии указанной проблематики: средневековый период, где следует отметить такого ученого, как Р. Луллий, впервые реализовавшего идею перебора вариантов; исследования XIX века, начавшиеся с создания первых вычислительных машин и программ для них (Ч. Бэббидж, А. Лавлейс, У. Джевонс и др.) и закончившиеся в 1939 г. созданием первого электронного цифрового компьютера (К. Берри, Дж. Атанасов). Поэтому, начиная с середины XX века, ведется активная работа над написанием программ, реализующих автоматический поиск доказательства. В. О. Шангин отмечает, что именно здесь зародилось два основных направления данного поиска: математический, позднее вылившийся в метод резолюций, и метод, симулирующий основные интеллектуальные приемы, используемые при построении логического вывода.

Первое направление представляют такие ученые, как: М. Дэвис, Дж. Робинсон, Л. Уос, Б. Мелтцер, П. Андреус, В. Бибель и др.

Ко второму направлению относятся А. Невел, Дж. К. Шоу, Г. Саймон, М. Минский, Л. М. Нортон и др. На сегодняшний день программы, базирующиеся на методе резолюций, являются самыми эффективными и способными решать очень сложные и объемные задачи (например, программа OTTER), однако за разработками, моделирующими собственно человеческие рассуждения, также стоит большое будущее, в силу важности исследований по робототехнике, нейрофизиологии и т.п.

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

На кафедре логики философского факультета МГУ с начала 90-х г. прошлого столетия предпринимались успешные попытки построения алгоритмов второго типа (т.е. ал

3 Шангин В.О. Автоматических поиск натурального вывода в классической логике предикатов. Диссертация на соискание ученой степени кандидата философских наук. Специальность 09.00.07 - Логика. Москва, 2004. Стр.16-22. горитмов, моделирующих человеческие рассуждения) для автоматического доказательства теорем в различных исчислениях. Одним из первых был создан алгоритм для натурального исчисления классической логики высказываний (Болотов А. Е., Бочаров В. А., Горчаков А. Е.4), который получил свою компьютерную реализацию на языке С++5. Позже с участием Шангина В. О. и др. была сконструирована процедура поиска вывода для классической логики предикатов (натуральное исчисление)6. Затем Горчаков А.Е., Макаров В. В., Спирин С.В.7 на основе предыдущих работ создали алгоритм, действующий в натуральном интуиционистском исчислении высказываний, построенном на базе соответствующего секвенциального исчисления. В настоящее время ждут своего решения компьютерные реализации поисковых процедур для классической логики предикатов и интуиционистской логики высказываний.

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

В этой связи необходимо упомянуть интерактивный редактор доказательств De-ductio9, сконструированный Смирновым А. В. и Новодворским А. Е., позволяющий работать со многими логическими системами, в том числе и с традиционной силлогистикой.

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

4 Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода в классической пропозициональной логике// Труды научно-исследовательского семинара логического центра института философии РАН. Москва, ИФРАН, 199 б.

5 Горчаков А.Е., Макаров В.В., Спирин С.В. О некоторых особенностях построения компьютерной реализации алгоритма автоматического доказательства теорем в натуральном исчислении. http://www.lodc.ru (Логические исследования). Москва, 1998.

6 Логика и компьютер. Выпуск 5. Пусть докажет компьютер. Москва, «Наука», 2004.

7 См.5.

8 Подробнее об этом см. Горчаков А.Е., Макаров В.В., Спирин С.В. О некоторых особенностях построения компьютерной реализации алгоритма автоматического доказательства теорем в натуральном исчислении. http://www.logic.ru (Логические исследования). Москва, 1998.

9 Логика и компьютер. Выпуск 3. Доказательство и его поиск (курс логики и компьютерный практикум). Москва, «Наука», 1996.

10 Логика и компьютер. Выпуск 3. Доказательство и его поиск (курс логики и компьютерный практикум). Москва, «Наука», 1996. пользования исчисления высказываний (исчисления предикатов) и поэтому с очень сложной формулировкой некоторых важных правил вывода.1'

Поисково-дедуктивная система «ЭКСПО», работающая по сходным принципам,

1 9 что и интерактивный редактор доказательств Deductio , была разработана А. П. Кулаиче

1Ч вым в 80-х гг. XX века. Группа исследователей, участвующая в разработке и тестировании данной системы, активно работала с силлогистическим знанием, в частности, с соритами Кэрролла, решая сориты с 20 посылками, в состав которых входили сложные термы (до трех пересечений позитивных и негативных термов)14. Эта система с помощью специальной базы данных могла даже формализовать сориты, введенные в нее на естественном языке, записывая полный набор посылок в виде цепочки конъюнкций, а отдельные посылки - как логическое умножение субъекта и предиката. Программа могла работать как пошагово (пользователь последовательно вводил в нее посылки), так и сразу получать заключение из формализованного сорита. Но силлогистические заключения, как итоговые, так и промежуточные, получались алгебраическим методом (путем вычеркивания одинаковых термов, вне зависимости от их качества) и, таким образом, механизмы действия программы не моделировали понятие логического вывода, в отличие от системы Deductio.

Здесь следует также упомянуть Бахтиярова К. И.15, чьим основным направлением исследования является работа над методом арифметизации логики, успешно разрешающего проблему Лейбница - представления умозаключений в виде арифметических вычислений. К. И. Бахтияров ввел логические векторы для представления булевых консти-туент, записав их компоненты в троичной системе счисления (что соответствует семантической интерпретации силлогистических теорий, по К.И. Бахтиярову). На основе данного метода были построены компьютерные программы, особый интерес из которых для данного исследования представляют программа КЭРРОЛЛ - для решения аристотелевских силлогизмов и программа СОРИТ - для решения соритов со многими терминами. Данные программы реализуют идею так называемого «логического калькулятора». Однако принципы работы данных программ основаны на математических методах и потому не моделируют эвристические приемы, характерные для «естественных» рассуждений. Логика и компьютер. Выпуск 3. Доказательство и его поиск (курс логики и компьютерный практикум). Москва, «Наука», 1996. Стр.202.

12 Логика и компьютер. Выпуск 3. Доказательство и его поиск (курс логики и компьютерный практикум). Москва, «Наука», 1996.

13 Кулаичев А.П., Рамендик Д.М., Славуцкая М.В. Диалоговая система подготовки и предъявления зрительной информации//Вопросы психологии. Москва, 1984, №4, стр. 118-120.

14 Этот эксперимент описан в журнале «Вопросы психологии» 1987 г. №3. в статье Адашинской Г.А., Ра-мендика Д.М., Тихомирова O.K.

15 Бахтияров К. И. Умозаключения на персональных компьютерах. М., 1989; Компьютеризация логики// ФИ. 1990.

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

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

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

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

Для достижения данной уели ставятся следующие задачи:

• Сформулировать натуральные исчисления для указанных в работе аксиоматических систем негативной силлогистики (аксиоматизации предложены Ильиным А.А.18);

16 Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода в классической пропозициональной логике// Труды научно-исследовательского семинара логического центра института философии РАН. Москва, ИФРАН, 1996.

17 Логика и компьютер. Выпуск 3. Доказательство и его поиск (курс логики и компьютерный практикум). Москва, «Наука», 1996.

18 Ильин А.А. Негативная силлогистика аристотелевского типа. Логика и В.Е.К.: Сборник научных трудов: К 90-летию со дня рождения проф. Войшвилло Евгения Казимировича. Москва, Современные тетради, 2003; Ильин А.А. Силлогистика Б. Больцано. Москва, Современные тетради, 2003; Ильин А.А. Негативная силлогистика Л. Кэрролла // Современная логика: проблемы теории, истории и применения в науке: Материалы VII Общероссийской научной конференции. Москва, 2002; Ильин А.А. Системы негативной силлогистики // Современная логика: проблемы теории, истории и применения в науке: Материалы IX Общероссийской научной конференции. Санкт-Петербург, 2006; Ильин А.А. Негативная фундаментальная силлогистика// Смирновские чтения. 3 международня конференция. Москва, 2001.

• Доказать семантическую непротиворечивость и семантическую полноту указанных натуральных силлогистических систем;

• Дать содержательное описание предложенного алгоритма;

• Представить детальное описание компьютерной реализации алгоритма, привести примеры его работы.

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

Научная новизна исследования

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

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

Тезисы, выносимые на защиту:

1. Утверждение, что построенные в диссертационном исследовании силлогистические натуральные исчисления для традиционной негативной силлогистики, фундаментальной негативной силлогистики, негативных силлоги-стик Больцано, Кэрролла и Аристотеля являются семантически непротиворечивыми и семантически полными.

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

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

Методологические основы и источники исследования

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

В диссертационном исследовании использовались формулировки систем натурального вывода, предложенные Бочаровым В. А.и Маркиным В. И.19

В основе представленного в диссертационной работе алгоритма лежит алгоритм, построенный Бочаровым В. А., Болотовым А. Е., Горчаковым А. Е. для классического исчисления высказываний и идеи, сформулированные Смирновым А. В. и Новодворским А. Е.

Практическая значимость

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

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

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

Основные положения и результаты диссертационного исследования были представлены в виде тезисов доклада на IX Международной научной конференции «Современная логика: проблемы теории, истории и применения в науке» (Санкт-Петербург, 2006 г.). Также автором были опубликованы две статьи - в «Вестнике Московского Университета» (2008 год) и Сборнике научных исследований по логике ИФ РАН (2007 год).

19 Бочаров В.А., Маркин В.И. Основы логики. Учебник. Стр. 129. Москва, ИНФРА-М, 2002.

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

ЗАКЛЮЧЕНИЕ

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

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

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

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

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

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

Для этого докажем конечность СВ, конечность СЦ и конечность ветвления СЦ.

Докажем конечность СВ.

Число посылок у нас конечно по определению.

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

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

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

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

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

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

Докажем теперь конечность СЦ.

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

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

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

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

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

Но что делать, если на этапе достижения 1{елей мы столкнулись с недостижимой целью? Не приведет ли это к получению бесконечной ветви в доказательстве (выводе)?

Наш алгоритм построен таким образом, что в случае недостижимости той или иной текущей цели, он пытается получить их альтернативным путем, т.е. посредством еще не применявшихся к ним синтетических правил. Если такие правила нашлись, то у нас повторяется описанный выше конечный цикл. Заметим, что алгоритм ведет строгий контроль над применением данных правил - они применяются последовательно и по порядку, поэтому у нас абсолютно исключена ситуация, когда алгоритм «зацикливается», постоянно применяя одно и то же правило к одной и той же текущей цели. Здесь же отметим, что все формулы СВ, относящиеся к тупиковой ветви доказательства (вывода), удаляются из СВ. Если же все возможные варианты получения данной цели были отработаны и они не дали нужного нам результата, то они просто удаляется из СЦ, что обеспечивает последовательное и необходимое уменьшение числа целей, а, как следствие, выбраковку тупиковых ветвей, включая и опровержение главной цели.

Таким образом, мы показали конечность СЦ.

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

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

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

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

Так мы доказали конечность ветвления СЦ.

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

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

Похожий метод доказательства такого рода утверждений использовался Е. Д. Смирновой49.

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

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

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

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

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

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

• усовершенствование программного модуля, построенного на основе нашего алгоритма, уменьшение времени его работы и уменьшение вероятности

49См. Смирнова Е.Д. Логика и философия. Серия «Научная философия. Москва, РОССПЭН, 1996. Стр. 97, 99. комбинаторного взрыва, что сделает его применимым к более сложному классу задач.

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

1. Andreoli J. M. Focussing and Proof Construction. Annals of Pure and Applied Logic, 107 (1), pp. 131-163. Amsterdam, Reed Elsevier, 2001.

2. Banerji R. Theory of Problem Solving: An Approach to Artificial Intelligence. New York, American Elsevier Publishing Company, Inc., 1969.

3. Barwise J., Etchemendy J. Language, Proof and Logic. New York London, Seven Bridges Press, 1999

4. Basin D., Matthews S., Vigano L. Natural Deduction for non-classical logics. Studia Logica, vol. 60 (1), 1998.

5. Feigenbaum E., Feldman J. Computers and Thought. New York, McGraw-Hill Book Company, 1963.

6. McVitie D. G., Wilson L. B. The Stable Marriage Problem. Commm.ACM, 14, № 7, 1971.

7. Porn I. Action Theory and social science. Some formal models. Dordrecht-Holland/Boston-U.S.A., D. Reidel Publishing Company, 1977.

8. Rasiowa H., Sikorski R. The Mathematics of Metamathematics. Warsza-wa, Panstowe wydawnictwo naukowe, 1963.

9. Shannon C. Programming a Digital Computer for Playing Chess, Philosophy Magazine, 41, 356 375, 1950.

10. Адашинская Г.А., Рамендик Д.М., Тихомиров O.K. Избирательность отношения к помощи ЭВМ. «Вопросы психологии», №3, Москва, 1987.

11. Аристотель «Первая Аналитика», Первая книга, гл. 46, Москва, «Мысль», 1978.

12. Бахтияров К. И. Умозаключения на персональных компьютерах. Москва, «Наука», 1989.

13. Бахтияров К. И. Компьютеризация логики// ФИ, М., 1990.

14. Болотов А.Е., Бочаров В.А., Горчаков А.Е. Алгоритм поиска вывода в классической пропозициональной логике// Труды научно-исследовательского семинара логического центра института философии РАН. Москва, ИФРАН, 1996 год.

15. Бочаров В.А, Маркин В.И. Введение в логику. Университетский курс. Москва, ИД «Форум» -ИНФРА-М, 2002.

16. Бочаров В.А. Аристотель и традиционная логика. Издательство Московского университета, Москва, 1984.

17. Бочаров В.А., Маркин В.И. Основы логики. Учебник. Москва, ИНФРА-М, 2002.

18. Братко И. Программирование на языке ПРОЛОГ для искусственного интеллекта. Москва, «Мир», 1990.

19. Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 2. Языки и исчисления. Москва, МЦНМО, 2000 г.

20. Вирт Н. Алгоритмы и структуры данных. Санкт-Петербург, «Невский диалект», 2001.

21. Войшвилло Е. К. Процедура поиска доказательства для формул системы Е.Философско-методологические аспекты релевантной логики. Москва, МГУ, 1989.

22. Гашков С. Б., Чубариков В.Н. Арифметика. Алгоритмы. Сложность вычислений; Учебное пособие для вузов. Москва, «Высшая школа», 2000.

23. Гильберт Б., Бернайс П. Основания математики. Логические исчисления и формализация арифметики. Москва, «Наука», Главная редакция физико-математической литературы, 1979.

24. Глушков В.М. Введение в кибернетику. Издательство Академии Наук Украинской ССР, Киев, 1964.

25. Горчаков А.Е., Макаров В.В., Спирин С.В. О некоторых особенностях построения компьютерной реализации алгоритма автоматического доказательства теорем в натуральном исчислении, http://www. logic.ru (Логические исследования). Москва, 1998.

26. Драгалина-Черная Е. Г. «Логика: от тривия к инженерии знаний» Научный журнал Московского гуманитарного университета «Знание. Понимание. Умение» № 4, Москва, Издательство Московского гуманитарного университета, 2006 г.

27. Есенин-Вольпин А. С. Формулы или формулоиды? XI Международная конференция. Логика, методология, философия науки. Секции: 1. Логика и основания математики. - Москва-Обнинск 1995. — Т.1 стр.29-32.

28. Зайцев Д. В. Понятие как релевантная функция// Труды научно-исследовательского семинара Логического центра ИФ РАН. Выпуск XVI. Москва, 2002.

29. Ильин А.А. Негативная силлогистика аристотелевского типа. Логика и В.Е.К.: Сборник научных трудов: К 90-летию со дня рождения проф. Войшвилло Евгения Казимировича. Москва, Современные тетради, 2003.

30. Ильин А.А. Силлогистика Б. Больцано. Москва, Современные тетради, 2003.

31. Ильин А.А. Негативная силлогистика Л. Кэрролла // Современная логика: проблемы теории, истории и применения в науке: Материалы VII Общероссийской научной конференции. Москва, 2002.

32. Ильин А.А. Системы негативной силлогистики // Современная логика: проблемы теории, истории и применения в науке: Материалы IX Общероссийской научной конференции. Санкт-Петербург, 2006.

33. Ильин А.А. Негативная фундаментальная силлогистика// Смирновские чтения. 3 международня конференция. Москва, 2001.

34. Клини С. Математическая логика. Москва, «Мир», 1973.

35. Колмогоров А.Н., Драгалин А.Г. Математическая логика. Москва, КомКнига, 2006

36. Кормен Т., Лейзерсон Ч. Алгоритмы: построение и анализ. 2-ое издание. Москва, «Вильяме», 2007.

37. Кулаичев А.П., Рамендик Д.М., Славуцкая М.В. Диалоговая система подготовки и предъявления зрительной информации// Вопросы психологии. Москва, 1984 год. №4, стр. 118 120.

38. Кук Д., Бейз Г. Компьютерная математика. Москва, «Наука», Главная редакция физико-математической литературы, 1990.

39. Кэрролл Л. История с узелками. Москва, «Мир», 2000.

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

41. Логика и компьютер. Выпуск 3. Доказательство и его поиск (курс логики и компьютерный практикум). Москва, «Наука», 1996.

42. Логика и компьютер. Выпуск 5. Пусть докажет компьютер. Москва, «Наука», 2004.

43. Логическое программирование. Сборник статей. Москва, «Мир»,1988 г.

44. Маркин В.И. Силлогистические теории в современной логике. Издательство Московского университета, Москва, 1991.

45. Маркин В.И. Системы силлогистики, адекватные двум переводам силлогистических формул в исчисление предикатов В.А. Смирнова // Труды научно-исследовательского семинара Логического центра Института философии РАН 1997. М., 1998.

46. Математическая теория логического вывода. Сборник переводов под редакцией А. В. Идельсона и Г. Е. Минца. Москва, «Наука», Главная редакция физико-математической литературы, 1967.

47. Математический энциклопедический словарь. Москва, «Советская энциклопедия», 1988.

48. Мендельсон Э. Введение в математическую логику. Москва, «Наука», Главная редакция физико-математической литературы, 1971.

49. Нильсон Н. Искусственный интеллект. Методы поиска решений. Москва, «Мир», 1973.

50. Павлюкевич В. И. Логические отношения между высказываниями. Логика и В.Е.К.: Сборник научных трудов: К 90-летию со дня рождения проф. Войшвилло Евгения Казимировича. Москва, Современные тетради, 2003.

51. Подбельский В.В. Язык С++. Москва,»Финансы и статистика», 2003.

52. Сикорский Р. Булевы алгебры. Москва, «Мир», 1969 .

53. Смирнова Е.Д. Логика и философия. Серия «Научная философия. Москва, РОССПЭН, 1996.

54. Стяжкин Н. И. Формирование математической логики. Москва, «Наука», 1967.

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

56. Успенский В. А. Лекции о вычислимых функциях. Москва, Государственное издательство физико-математической литературы, 1960.

57. Фаронов В. В. Delphi 6. Учебный курс. Москва, Издатель Молгачева С. В., 2001 .

58. Фейс Р. Модальная логика. Перевод с дополнениями под редакцией Г. Е. Минца. Москва, «Наука», Главная редакция физико-математической литературы, 1974.

59. Черч А. Введение в математическую логику. Том 1. Глава I. § 17. Издательство иностранной литературы, Москва, 1960.

60. Шангин В.О. Автоматических поиск натурального вывода в классической логике предикатов. Диссертация на соискание ученой степени кандидата философских наук. Специальность 09.00.07 Логика. Москва, 2004.

61. Шангин В.О. Автоматический поиск вывода для натуральной системы интуиционистской логики и проблемы дубликации. Москва, Современные тетради, 2003.

62. Шиян Т. А. Множество формальных силлогистик с простыми "общими" термами (структурное описание и количественный анализ). Москва, Online Journal "Logical Studies". No.8, 2002.

63. Шиян T.A. Классификация силлогистических теорий // Смирновские чтения. 3 Международная конференция. Москва, 2001.

64. Шиян Т.А. Методы классификации формальных теорий и множество силлогистик // Аспекты: Сборник статей по философским проблемам истории и современности. Москва, "Современные тетради", 2002.

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

66. Данное различение необходимо для корректного осуществления эвристического поиска.

67. Обозначим указанную функцию через у.

68. Отношение частичного порядка < на множестве силлогистических формул (т.е.простых с пропозициональной точки зрения формул) определяется так: А < В <=> \|/(А) < \|/(В). Так же, как и для пропозициональных формул, оно монотонно.

69. Оценим, например, при помощи функции у формулу Sa—P. vj/(Sa—Р) = \|/(Sa~P) + 1 = y(SaP) + 1 + 1= 0+1 + 1=2.

70. Оценим правило XaY ь- ~Ya~X. \)/(ХaY) = 0. < [\]/(~Ya~X) = i|/(Ya~X) + V(YaX) + 1 + 1=0 + 1 + 1=2].

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