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

Актуальность темы

исследования.

Вопросы, связанные с поиском логического вывода, составляют ядро многих логических исследований. Как отмечает В. О. Шангин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. комбинаторного взрыва, что сделает его применимым к более сложному классу задач.