Рассматривая проблему автоматизации доказательств, В.М.Глушков
снова приходит к проблеме языка. Он считает, что, прежде всего,
необходимо разработать практический, формальный язык для записи
математических предложений и их доказательств. Этот язык должен
быть близким к естественному языку математики и фактически представлять
собой формализацию той части естественного языка, на котором пишутся
книги по математике. Его отношение к существующим формальным языкам
математической логики должно быть таким же, как, скажем, язык машин
Тюринга или нормальных алгоритмов относится к развитым языкам программирования.
В. М. Глушков предлагал включить в язык доказательств элементы алгоритмических
языков, рассматривая оператор присваивания вида "G : = группа"
или "М : == множество", как аналоги предложений: "пусть
G - группа", "обозначим через М множество". Важную
роль в таком языке, играет понятие конструкции, которое формализует
такие выражения языка, как, например, "пересечение всех подгрупп
группы G/H, таких, что...". Реализацией языка математики является
"алгоритм очевидности", который позволяет проверять правильность
математических текстов, написанных в языке, если доказательства
достаточно подробны, или находить в них пробелы. На базе уже только
этих средств, строится "интеллектуальная" информационная
система, которая позволяет накапливать знания и пользоваться ими
в процессе выполнения математических исследований. Что же касается
открытия новых математических фактов и поиска доказательств трудных
теорем, то это должно выполняться в интерактивном режиме с использованием
специализированных дедуктивных средств, которые создаются на базе
языка, алгоритмов очевидности и информационной системы.
Программа исследований, намеченных в статье, была успешно
выполнена. Разработана версия языка теории, разработаны и экспериментально
проверены алгоритмы поиска вывода, которые вместе с языковыми средствами
составляли базу системы автоматизации доказательств (САД). Система
САД находилась в опытной эксплуатации в Институте кибернетики еще
в 90-е годы.
Принципы построения систем автоматизации доказательств.
В.М.Глушков уделял большое внимание работам по автоматизации доказательств
до конца своей жизни. В одной из своих последних работ, относящихся
к 1980 году, он формулирует основные принципы, которые должны быть
положены в основу дальнейшего развития системы САД и других систем
автоматизации доказательств. Основное назначение такого рода систем
- автоматизация в режиме диалога с компьютером различного рода дедуктивных
построений: доказательств теорем, формульных преобразований, построения
примеров проверки корректности различного рода конструкций - алгоритмов,
определений и т.д. В силу такой практической направленности эти
системы значительно отличаются по принципам своего построения от
обычных программных систем, реализующих процедуры поиска вывода
классической математической логики. Вот некоторые из важнейших отличий,
отмеченные в работе.
Первое отличие состоит в том, что язык записи математических
текстов, используемый в этих системах, должен быть максимально приближен
к обычному языку математических публикаций. В математических текстах
используются слова и конструкции обычного языка. По возможности
минимизируется употребление непривычной для содержательных разделов
математики символики классической математической логики. Приводится
такая аналогия: язык системы автоматизации доказательств относится
к языку классических логических систем (например, к языку узкого
исчисления предикатов), как современный развитый алгоритмический
язык (например Паскаль или Java) относится к языку записи программ
для простейших машин Тьюринга.
Второе, еще более существенное отличие - крупноблочность
построения системы. Под крупноблочностью здесь понимается использование
в качестве инструментов логического вывода не только фиксированного
небольшого числа простых аксиом и правил вывода, а всего богатства
предложений и процедур содержательных разделов математики.
Стремление минимизировать число аксиом и правил вывода,
характерное для современных теоретико-логических построений, имеет
свои исторические причины. Родившись как средство формализации дедуктивного
вывода, математическая логика в процессе своего развития подменила
первоначальную цель такой формализации другой целью. У истоков математической
логики лежала мечта (высказанная Лейбницем) о времени, когда люди
"вместо того чтобы спорить, станут вычислять". Однако
в конце 19 века и особенно в 20 веке эта, хотя и наивно сформулированная,
но, тем не менее, достаточно практическая цель развития математической
логики была заменена другой, сугубо теоретической - служить средством
обоснования математики.
С этой новой целью вполне согласуется стремление строить
логические системы на базе минимального числа наиболее элементарных
предложений и процедур. Однако подобная "атомизация" математической
логики делает ее совершенно не пригодной для практических применений
с целью автоматизации дедуктивных построений в содержательных разделах
математики. Всякий, кто ставит себе задачу построить сколько-нибудь
эффективный инструмент для реальной помощи человеку в развитии содержательных
разделов математики, должен, прежде всего, освободить свое мышление
от пут, накладываемых на него многими нынешними принципами развития
аппарата математической логики.
Третье отличие состоит в том, что используемые в САД
приемы логического вывода употребляют не классическое (предикатное),
а другое, более отвечающее характеру реальных доказательств в содержательной
математике представление предмета и приемов логического вывода,
которое В.М.Глушков называет объектным. Дело в том, что львиная
доля трудностей в доказательстве предложений содержательных разделов
математики заключается не в построении формальных логических преобразований,
а в построении подходящих объектных конструкций, дающих ключ к доказательству.
После нахождения нужных конструкций остающаяся собственно формально-логическая
часть вывода достаточно тривиальна: как правило, она сводится к
использованию простейших систем типа силлогизмов для предикатов
в бескванторной форме.
Например, если требуется доказать предложение вида,
то ключевым (и самым трудным) моментом доказательства является построение
(путем суперпозиции подходящих конструкций, извлекаемых из ранее
рассмотренных предложений, определений и процедур) объектной зависимости
, не обязательно однозначной, такой, чтобы высказывание было истинным
при всех значениях х.
Четвертое отличие - это формализация и автоматизация
процедур взаимодействия алгоритмов вывода с информационной частью
системы (математическими текстами). Здесь В.М.Глушков высказывает
идею построения и накопления математической базы знаний в виде формализованных
математических текстов, содержащих не только уже доказанные ранее
теоремы, но и их доказательства, которые могли бы служить источником
объектных конструкций при поиске доказательств теорем.
Пятое отличие заключается в том, что в систему включаются
формализованные процедуры для ее непрерывного пополнения и совершенствования
(свойство динамизма системы).
К другим, менее существенным, отличиям В.М.Глушков относит
необходимость использования типизированных переменных в кванторах.
Предполагается, что практическая направленность систем и диалоговый
режим их использования позволяют не включать априорные ограничения
на вводимые в них понятия. Можно, например, ввести и пользоваться
понятием "множество всех множеств", запретным для обычных
теоретико-логических систем. Задача защиты от возникающих при этом
парадоксов и противоречий возлагается на пользователей системы.
Впрочем, учитывая свойство динамизма системы, такие ограничения
в ней легко как снимать, так и вводить.
Руководители разработки: Капитонова Ю.В., Летичевский А.А.
Основные разработчики системы САД: Дегтярев А.И., Вершинин
К.П., Костырко В.Ф., Асельдеров З.М., Жежерун А.П., Лялецкий А.В.,
Мороховец М.К, Домрачев В.Н. , Соболева Н.В.., Парницкий В.И.,
Ю.В.Капитонова, А.А.Летичевский
|