Искусственный интеллект

Рассматривая проблему автоматизации доказательств, В.М.Глушков снова приходит к проблеме языка. Он считает, что, прежде всего, необходимо разработать практический, формальный язык для записи математических предложений и их доказательств. Этот язык должен быть близким к естественному языку математики и фактически представлять собой формализацию той части естественного языка, на котором пишутся книги по математике. Его отношение к существующим формальным языкам математической логики должно быть таким же, как, скажем, язык машин Тюринга или нормальных алгоритмов относится к развитым языкам программирования. В. М. Глушков предлагал включить в язык доказательств элементы алгоритмических языков, рассматривая оператор присваивания вида "G : = группа" или "М : == множество", как аналоги предложений: "пусть G - группа", "обозначим через М множество". Важную роль в таком языке, играет понятие конструкции, которое формализует такие выражения языка, как, например, "пересечение всех подгрупп группы G/H, таких, что...". Реализацией языка математики является "алгоритм очевидности", который позволяет проверять правильность математических текстов, написанных в языке, если доказательства достаточно подробны, или находить в них пробелы. На базе уже только этих средств, строится "интеллектуальная" информационная система, которая позволяет накапливать знания и пользоваться ими в процессе выполнения математических исследований. Что же касается открытия новых математических фактов и поиска доказательств трудных теорем, то это должно выполняться в интерактивном режиме с использованием специализированных дедуктивных средств, которые создаются на базе языка, алгоритмов очевидности и информационной системы.

Программа исследований, намеченных в статье, была успешно выполнена. Разработана версия языка теории, разработаны и экспериментально проверены алгоритмы поиска вывода, которые вместе с языковыми средствами составляли базу системы автоматизации доказательств (САД). Система САД находилась в опытной эксплуатации в Институте кибернетики еще в 90-е годы.

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

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

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

Стремление минимизировать число аксиом и правил вывода, характерное для современных теоретико-логических построений, имеет свои исторические причины. Родившись как средство формализации дедуктивного вывода, математическая логика в процессе своего развития подменила первоначальную цель такой формализации другой целью. У истоков математической логики лежала мечта (высказанная Лейбницем) о времени, когда люди "вместо того чтобы спорить, станут вычислять". Однако в конце 19 века и особенно в 20 веке эта, хотя и наивно сформулированная, но, тем не менее, достаточно практическая цель развития математической логики была заменена другой, сугубо теоретической - служить средством обоснования математики.

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

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

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

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

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

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

Руководители разработки: Капитонова Ю.В., Летичевский А.А.

Основные разработчики системы САД: Дегтярев А.И., Вершинин К.П., Костырко В.Ф., Асельдеров З.М., Жежерун А.П., Лялецкий А.В., Мороховец М.К, Домрачев В.Н. , Соболева Н.В.., Парницкий В.И.,

Ю.В.Капитонова, А.А.Летичевский