Файл: ЗнанияОнтологииТеории (зонт17) Построение Семантической Сети Теории Множеств с Помощью Программы.pdf

Знания-Онтологии-Теории (ЗОНТ-17)
Построение Семантической Сети Теории
Множеств с Помощью Программы
MATHSEM
А.А. Люксембург andr_lux@mail.ru
Аннотация. Популярное направление в ИИ - это инженерия и представление знаний.
Математические знания наиболее формализованы, поэтому их представление важно и
интересно. Различные математические теории составляют математическое знание. Мы
рассмотрим дедуктивную систему, выводящую математические понятия, аксиомы и теоремы
элементарной теории множеств. Объединённые вместе эти понятия, аксиомы и теоремы
можно считать небольшой математической теорией. Эта теория будет представлена в виде
семантической сети.
Ключевые слова: семантическая сеть, математическая логика, теория множеств,
аксиоматические теории, формальные системы, автоматическое доказательство теорем,
представление знаний, инженерия знаний
1 Введение
В этой работе описывается проект и часть компьютерной программы по автоматизированному построению математических теорий.
Создание математической теории является ярким примером интеллектуальной деятельности людей и творческого процесса. Задача формализации вывода математической теории относится к задачам искусственного интеллекта. Откуда берутся математические понятия, аксиомы, теоремы, математические теории? С развитием математической логики стало понятно, что большинство математических теорий можно описать формально (с помощью формальных языков, аксиоматических систем).
С развитием вычислительной техники и программирования многие математические задачи стало возможно решать с помощью компьютеров (вычисления, символьные преобразования, доказательство теорем). Проследить внутреннюю связь между аксиомами теории, ее понятиями
(определениями) и теоремами является важной задачей. При формальной записи математической теории на языке логики предикатов возникают вопросы, насколько много нужно базовых понятий и аксиом, чтобы выразить все другие определения и теоремы теории.
Почему одни формальные структуры что-то задают, а другие нет? Существуют ли критерии для определения важности тех или иных формальных объектов для теории? С формальной точки зрения все определения, аксиомы и теоремы являются набором неких символов. Почему один набор символов задает что-то важное и интересное, а другой нет?
Проект направлен на разработку математического и программного обеспечения для интерактивного построения математических теорий. Разрабатывается компьютерная программа не только для автоматического доказательства теорем, но и программа, способная с помощью эксперта строить определения и теоремы. Важную роль играет возможность обучения с помощью такой программы. Формализация вывода математической теории, изучение формальной структуры математических теорий является важной задачей с точки зрения математической логики, информатики и «чистой» математики. Актуальность проекта связана с тем, что он лежит на стыке математики, информатики, таких современных областей как представление знаний, семантические сети, онтологии, дедуктивные системы. Этот проект может быть полезен научным работникам в области математики, аспирантам, студентам.

Результаты проекта предназначены для изучения самой математики, логики, структуры математических теорий, связи формальных и естественных методов доказательства теорем и построения математических теорий. Основной сферой применения видится именно образование, когда с помощью визуального интерфейса можно будет изучать элементарные теории, просмотреть семантическую сеть изучаемой предметной области (различных математических теорий); изучить методы формального доказательства; проследить связь естественного языка (русского, английского) с языком логики первого или высших порядков; промежуточных языков, различных систем типизации, используемых в системах автоматического доказательства теорем (простая теория типов Б. Рассела, лямбда-исчисление, теория типов П. Мартин-Лефа).
Под термином «представление знаний» чаще всего подразумеваются способы представления знаний, ориентированные на автоматическую обработку современными компьютерами, и, в частности, представления, состоящие из явных объектов и из суждений или утверждений о них.
Из специальных методов и формализмов представления знаний нас будут интересовать:
1. Логика предикатов первого порядка [1,4];
2. Дедуктивные (продукционные системы). Есть набор начальных объектов, правила вывода новых объектов из начальных и уже построенных, и совокупность всех построенных и начальных объектов [6].
3. Семантическая сеть. В самом общем случае семантическая сеть представляет собой информационную модель предметной области и имеет вид графа, вершины которого соответствуют объектам (понятиям) предметной области, а дуги – отношениям между ними
[2,8].
2 Описание проекта
Разработан формальный язык (близкий к языку логики предикатов первого порядка), продукционная система, которая строит выражения в этом формальном языке [5].
Под продукционной системой понимаются правила построения формул в формальном языке.
Есть еще правила логического вывода, правила устранения термов, методы доказательства теорем. Мы будем различать систему построения формул и систему доказательств теорем.
Есть правила построения новых формул из начальных (атомарных) и уже построенных.
Формулами являются либо утверждения (предикаты), либо определения (могут быть предикатами или могут быть множествами истинности предикатов). Эти формулы (объекты) записываются в вершины сети (графа). Между объектами существует несколько видов отношений: логические, синтаксические, квантификационные, теоретико-множественные, семантические.
В качестве атомарной формулы рассматривается предикат принадлежности. Правила построения новых формул включают в себя логические операции (конъюнкцию, дизъюнкцию, отрицание, импликацию), добавление квантора всеобщности или существования, еще одно правило – это построение множества истинности предиката. Множество истинности предиката рассматривается как терм, никаких других функциональных символов и термов не вводится.
Можно говорить о символах, обозначающих предикаты и множества, и о самих предикатах и множествах (когда задана интерпретация или модель). Еще одно правило допускает подстановку как индивидной переменной, так и терма вместо переменной. Далее, когда мы построили новую формулу, мы можем ее упрощать с помощью правил переписывания термов и логических законов (методов автоматического доказательства). В стандартном исчислении предикатов нет операции построения множеств истинности (там все формулы являются предикатами), которые в нашей системе являются термами, и нет правил вывода, связанных с устранением этих термов. Можно доказать теорему, что все термы устранимы. После устранения термов, мы получим формулу, состоящую только из атомарных предикатов принадлежности, связанных логическими связками. Все кванторы можно вынести вперёд и привести формулу к сколемовскому виду.
Одним из результатов работы алгоритма будут замкнутые формулы (без свободных переменных), набор независимых таких формул можно рассматривать как аксиомы некой теории. Существование модели у такой теории является задачей исследования. Для доказательства теорем можно применять, как известные методы автоматического

доказательства (метод резолюций, метод аналитических таблиц, натуральный вывод, обратный метод), так и новые методы основанные на том, что известна «атомарная» структура формулы
(утверждения), которую мы пытаемся доказать.
При получении новой формулы на формальном языке эксперт математик может перевести ее на «естественный» язык (русский, английский), таким образом создается словарь основных понятий системы. Более сложные формулы переводятся на естественный язык с помощью алгоритма и словаря [5].
Существует несколько подходов, которые используются при построении математики - это теоретико-множественный, конструктивный (алгоритмический), теория топосов и др.
Математическая логика тоже является частью оснований математики. И при построении математических теорий можно рассматривать различные логики (интуиционистскую, модальную и др.). Дедуктивная система, которая строится, использует классическую логику предикатов первого порядка плюс правило построения множества истинности предиката
(термы), и к правилам логического вывода добавляются правила устранения этих термов. В качестве исходного объекта рассматривается предикат принадлежности. Продуктами вывода этой дедуктивной системы являются математические понятия и теоремы. В нашей системе узлами (вершинами) семантической сети являются формулы (строки). Формулы могут быть предикатами или математическими объектами (множествами истинности).
Основными отношениями между элементами сети являются отношения, связанные со способом получения элемента (узла или объекта) сети из других. Если формула получена объединением двух других, то она связана с ними отношением наследования типа предок- потомок. Другое отношение получается между множеством истинности предиката и предикатом, из которого оно получено. При подстановке объектов в предикаты и при объединении объектов возникают соответствующие отношения, которые соответствуют дугам между объектами (формулами). Отношения в сети можно разделить на семантические, синтаксические, логические, теоретико-множественные, квантификационные. Синтаксическое отношение означает, что одна формула входит в состав другой. Логические отношения делятся на дизъюнкцию, конъюнкцию, отрицание, импликацию, равенство. Теоретико-множественные определяют отношения между объектами как множествами. Квантификационные делятся в зависимости от квантора, отличающего формулы (логические кванторы общности и существования).
3 Современное состояние исследований в данной области науки
Исследования в данной области в основном связаны с написанием программ по автоматическому доказательству теорем, развитием семантического интернета, онтологиями.
Выходец из России А. Воронков вместе с коллегами написал прувер Vampire (на основе метода резолюций). Сейчас он профессор в Манчестере. Под его и Дж. А. Робинсона редакцией вышла книга « Handbook of Automated Reasoning» [11].
Во Франции разрабатывается проект Coq —интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования
(Gallina) с зависимыми типами. Coq позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ.
В институте Макса Планка в Германии написан прувер SPASS. Интерактивный прувер
Isabelle для логик, в том числе высокого порядка, использует в частности метод аналитических таблиц. Американский прувер Prover9 (наследник Otter) доказывает теоремы в логике первого порядка. Прувер компании Microsoft Z3 появился в связи с необходимостью верификации программного обеспечения такого крупного производителя. Проект MIZAR (в основном
Польша) верифицировал с помощью своего языка тысячи теорем.
Учениками академика В.М. Глушкова на Украине в рамках проекта «Алгоритм
Очевидности» («Evidence Algorithm») написана программа САД (система автоматизации дедукции). Система предназначена для автоматической обработки формальных математических

текстов, записанных в языке ForTheL (FORmal THEory Language). Также допускается ввод в языке первого порядка. Она использует прувер Moses и доступна на сайте http://nevidal.org/sad.ru.html. Белорусский проект OSTIS (Open Semantic Technology for Intelligent
Systems) направлен на создание массовой семантической технологии компонентного проектирования интеллектуальных систем различного назначения [10].
В МГУ на кафедре МАТИС А.С. Подколзиным вместе с учениками написана программа
«Компьютерный решатель задач» [9]. По своей логике и внутреннему устройству она отличается как от пруверов, которые в качестве алгоритмов используют в основном метод резолюций либо метод аналитических (семантических) таблиц, так и от решателей задач в
MathCad, MatLab, Mathematica.
Существуют другие компьютерные программы по автоматическому доказательству теорем.
В настоящее время в России нет проекта по автоматическому доказательству теорем, который обладал бы современным интерфейсом, использовал современные разработки в этой области, реально использовался математиками.
В предлагаемом проекте, в отличие от стандартных пруверов, где необходимо записать доказываемую теорему и аксиомы, необходимые для ее доказательства на формальном языке и непосредственно внутреннем языке самой системы, наоборот, формально записанные аксиомы и теоремы автоматически порождаются компьютерной программой и с помощью интерактивного алгоритма переводятся на естественный язык. Таким образом можно построить новые математические объекты, понятия, определения, теоремы. Можно придумать множество алгоритмов для построения формул в соответствии с правилами их построения. Эти алгоритмы должны выбирать формулы и сами правила, которые будут применяться к формулам для построения новых формул. Один из возможных алгоритмов описан в [5]. В данной статье описывается «ручной» способ построения формул. И сами формулы и правила построения выбираются пользователем программы на каждом шаге. С помощью языка теории множеств и аксиоматики теории множеств можно построить и обосновать значительную часть математики.
Именно поэтому в качестве исходного объекта взят предикат принадлежности.
В статье описывается построение основных операций и предикатов теории множеств. В математике есть основные структуры
1. алгебраические, 2. структуры порядка, 3. топологические.
Операции пересечения, объединения, дополнения уже определяют кольцо, алгебру множеств. Включение множеств - это структура порядка. С помощью теоретико- множественных операций можно определить аксиомы топологии. В этом заключается удивительная эффективность теории множеств в математике.
Множества с операциями объединения и пересечения образуют булеву алгебру. В этом есть некоторый дуализм логики и теории множеств.
Для конечных множеств можно определить мощность как количество элементов в них.
Например |A| - это кол-во элементов в множестве А. Тогда операции сложения и умножения натуральных чисел можно определить так: |A|+|B|=|A

B|, если A

B=

;
|A|

|B|=|A

B| , где A

B -декартово произведение множеств A и B.
Сложение и умножение натуральных чисел это - основные операции в арифметике.
В этом статье поэтому в качестве примера рассматривается получение основных понятий теории множеств (пустое множество, множество-универсум, множество подмножеств, принадлежность, разность, включение, пересечение, объединение, декартово произведение). Во всех этих понятиях (соответствующих формулах) количество атомарных формул не превышает двух. С помощью программы MathSem можно построить другие аксиомы и теоремы теории множеств. С помощью дедуктивной системы можно вывести и представить в виде семантической сети основы теории множеств, евклидовой геометрии, теории групп и теории графов.
В статье не вводится целиком аксиоматика ZFC, потому что целиком эта аксиоматика нужна для построения всей математики. В нашей системе можно построить аксиому объёмности, аксиому пустого множества, аксиому пары, аксиому объединения, аксиому бесконечности, аксиому степени, аксиому регулярности из аксиоматики Цермело-Френкеля для теории множеств. Схема выделения соответствует построению множества истинности. Связь схемы выделения и схемы преобразования с данной системой выходит за рамки этой статьи. Мы

строим наивную теорию множеств с простыми типами. Для предотвращения парадоксов множества истинности типизированы, имеют свой тип.
Многие теории и теоремы можно построить с некоторыми отдельными аксиомами. Область в математике Reverse Mathematics изучает вопросы, связанные с тем, какие именно нужны аксиомы для доказательства тех или иных теорем [12].
4 Определимость и выразимость
Из логики предикатов нам понадобятся определения предиката, что такое выполнимые, истинные и ложные формулы и что такое интерпретация.
Впервые вопрос об определимости был поднят в связи с рассмотрением отношения между
Евклидовой и неевклидовыми геометриями в работах А. Падоа. В дальнейшем в четкой форме понятие определимости было введено А. Тарским. Большое значение для теории определимости сыграли интерполяционная теорема Крейга и теорема Э. Бета [7]. В этих работах была показана тесная связь понятия определимости с понятием выводимости. В результате ряд важных проблем, относящихся к определимости, удалось свести к хорошо разработанным проблемам логического вывода.
Пусть фиксирована некоторая сигнатура и ее интерпретация с носителем D. Мы хотим определить понятие выразимого (с помощью формулы данной сигнатуры в данной интерпретации) k-местного предиката.
Выберем k переменных x
1
, x
2
,…, x k
. Рассмотрим произвольную формулу P, все параметры которой содержатся в списке x
1
, x
2
,…, x k
. Истинность этой формулы зависит только от значений переменных x
1
, x
2
,…x k
. Тем самым возникает отображение D
k

{И,Л}, то есть некоторый k- местный предикат на D. Говорят, что этот предикат выражается формулой P. Все предикаты, которые можно получить таким способом, называются выразимыми. Будем говорить, что предикат P на множестве D выразим через предикаты P
1
, P
2
,…, P
k на множестве D, если мы можем выразить некоторое предложение на языке, оперирующее только предикатами P
1
, P
2
,…,
P
k и такое, что оно истинно в том и только в том случае, если истинен предикат Р. Кроме самих предикатов можно использовать логические связки и кванторы [1].
Любой k-местный предикат P(x
1
, x
2
,…, x k
) (где x
1
, x
2
,…, x k
– свободные переменные) определяет некоторое множество M таким образом, что элементами множества M являются те и только те предметы

x
1
, x
2
,…, x
n

, для которых P(x
1
, x
2
,…, x n
, x n+1
, …, x k
) есть истинное высказывание. Это множество обычно обозначается в математике через
M(x n+1
, …, x k
):={

x
1
, x
2
,…,x
n

| P(x
1
, x
2
,…, x n
, x n+1
, …, x k
) } и читается так: «множество всех таких

x
1
, x
2
,…, x
n

, чтоP(x
1
, x
2
,…, x n
, x n+1
, …, x k
)». Это множество истинности предиката.
5 Описание дедуктивной системы
5.1 Алфавит языка
xi - переменные, обозначающие элементы множеств; Ai - переменные, обозначающие множества; P
i
- обозначение предикатов; M
i
, R
i
, D
i
- обозначение множеств, математических объектов (для разных типов множеств разные обозначения); /\ (&), \/,

,

- логические связки;

- квантор всеобщности;

- квантор существования;

- символ принадлежности;

x
1
, x
2
,…, x
n

- обозначение кортежей; {x
1
, x
2
} - поэлементное обозначение множеств.
5.2 Формулы языка
Описание объектов, выводимых в дедуктивной системе. Это или формулы, обозначающие предикаты, или формулы, описывающие математические объекты (понятия).
Основная идея. У нас есть предикат принадлежности. Рассмотрим предикаты, которые можно выразить через него и выразимые множества этих предикатов.