|
Содержание
Введение
Создание математической теории является ярким примером интеллектуальной деятельности людей и творческого процесса. Задача формализации вывода математической теории относится к задачам искусственного интеллекта. В книге рассматривается дедуктивная система вывода формул формального языка, включающего в себя математические утверждения и определения математических объектов. Исторически математика формировалась из нужд практической деятельности людей, многие математические понятия и теории были абстрактным или идеализированным отражением действительности, окружающего мира, т.е. носили эмпирический характер. Затем с развитием математической логики, математика становилась все более формализованной наукой. После появления компьютеров многие математические задачи стало возможным решать с их помощью. В математике есть понятия и соответствующие теории: равенство, функция, элемент, множество, отношение, граф, включение, пересечение, объединение, дополнение, разность, операция, свойство, мера, метрика, интеграл, предел, производная, натуральные числа, комплексные числа, действительные числа, алгебраические структуры: группы, кольца, поля; окрестность, непрерывность, размерность, компактность, геометрические фигуры, многообразия, топологические структуры и т.д. и т.п. В принципе все вышеизложенные понятия и теории, их касающиеся, могут быть сформулированы достаточно формально. Точного математического определения, что такое математическая теория – нет. Можно говорить, что математическая теория – это набор формул, или набор аксиом и формул, которые могут быть выведены из аксиом. Но такие определения не отражают содержательной стороны теории. Чтобы точнее охарактеризовать теорию говорят об объектах, описываемых в этой теории. Например, теория групп, теория множеств и т.д. Считается, что создание математической теории является прерогативой математиков. Интересный вопрос: насколько создание математической теории может быть автоматизировано? Развитие формальных методов в математике и совершенствование вычислительной техники позволило разработать программы, реализующие дедуктивные системы, в частности направленные на доказательство теорем. В книге рассматривается математическое и программное обеспечение, позволяющее строить достаточно сложные дедуктивные системы, в том числе математические теории. В науке и на практике часто встречаются системы, которые можно описать следующим образом: имеется некоторое количество исходных объектов и некоторое количество правил построения новых объектов из исходных и уже построенных. Или так: имеется начальная позиция (начальное состояние) и заданы "правила игры" (правила перехода от состояний к состояниям). Такие системы называются дедуктивными или исчислениями. Задача заключается в построении дедуктивной системы и формального языка, которые описывают как математические объекты, так и утверждения об этих объектах, т.е. теоремы и аксиомы. Нужно разработать алгоритм, реализующий систему автоматического построения математических выражений, их анализа и перевода на естественный язык. Выражения могут быть двух типов. Одни описывают математические объекты, другие – высказывания об объектах. Существует несколько подходов, которые используются при построении математики – это теоретико-множественный, конструктивный (алгоритмический), теория топосов и др. Математическая логика тоже является частью оснований математики. И при построении математических теорий можно рассматривать различные логики (интуиционистскую, модальную и др.). Дедуктивная система, которая будет строиться, использует классическую логику предикатов первого порядка. В качестве исходного объекта рассматривается предикат принадлежности. Продуктами вывода этой дедуктивной системы являются математические понятия и теоремы. Взятые вместе эти понятия и теоремы образуют математическую теорию. Разработан и реализован на компьютере алгоритм, соответствующий дедуктивной системе. |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||