Главная » 2014 » Сентябрь » 1 » Скачать Алгоритм поиска вывода для систем негативной силлогистики. Красненкова, Анастасия Владимировна бесплатно
7:37 AM
Скачать Алгоритм поиска вывода для систем негативной силлогистики. Красненкова, Анастасия Владимировна бесплатно
Алгоритм поиска вывода для систем негативной силлогистики
Диссертация
Автор: Красненкова, Анастасия Владимировна
Название: Алгоритм поиска вывода для систем негативной силлогистики
Справка: Красненкова, Анастасия Владимировна. Алгоритм поиска вывода для систем негативной силлогистики : диссертация кандидата философских наук : 09.00.07 / Красненкова Анастасия Владимировна; [Место защиты: Моск. гос. ун-т им. М.В. Ломоносова] - Москва, 2009 - Количество страниц: 114 с. ил. Москва, 2009 114 c. :
Объем: 114 стр.
Информация: Москва, 2009
Содержание:
ВВЕДЕНИЕ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
Введение:
Актуальность темы исследования
Вопросы, связанные с поиском логического вывода, составляют ядро многих логических исследований. Как отмечает В. О. Шангин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.
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.
