Построение Семантической Сети Теории Множеств с Помощью Программы MATHSEM. ЗнанияОнтологииТеории (зонт17) Построение Семантической Сети Теории Множеств с Помощью Программы
 Скачать 0.87 Mb.
|
|
Знания-Онтологии-Теории (ЗОНТ-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 Формулы языка Описание объектов, выводимых в дедуктивной системе. Это или формулы, обозначающие предикаты, или формулы, описывающие математические объекты (понятия). Основная идея. У нас есть предикат принадлежности. Рассмотрим предикаты, которые можно выразить через него и выразимые множества этих предикатов. Атомарными считаются формулы: P0(xi, Aj):=xi Aj Способы построения новых формул: 1. Отрицание P j : = P i 2. Объединение с помощью логических связок P k :=P i /\P j , P k :=P i \/P j , P k :=P i P j 3. Навешивание кванторов. Для любой свободной переменной x в предикате Pi можно построить новые предикаты: P j :=( x P i , P k := x Pi 4. Пусть есть конечный набор переменных x 1 , x 2 ,…, x n , тогда можно определить строку x 1 , x 2 ,…,x n -это кортеж из n переменных. 5. Построение математического объекта (понятия). Пусть есть предикат P(x 1 , x 2 ,…,x k ) , (где x 1 , x 2 ,…, 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 M(x n+1 , …,x k ) P(x 1 , x 2 ,…,x n , x n+1 , …,x k ) или P0( x 1 , x 2 ,…,x n M(x n+1 , …,x k )) P(x 1 , x 2 ,…,x n , x n+1 , …,x k ). 6. Подстановка переменных. В предикате P или объекте M можно заменять переменные. Математические объекты, по сути, являются множествами, их можно подставлять в качестве переменных в предикаты. Уровень переменной при подстановке должен сохраняться. 5.3 Определение уровня переменной. Уровень переменной определяется по индукции, это строка из нулей и треугольных скобок (вложенные кортежи из нулей). Пусть x A, y B – атомарные формулы, тогда уровень x, y будет 0. Уровень A, B – 0 A B, A B множества уровня 0 , т.к. состоят из x: A B={x | x A x B}, x A B (x A x B). Уровень A B будет 0 . Множества, состоящие из множеств 0 уровня - это множества уровня 0 , R= {A| A B}, A R A B. Если у нас множество состоит из кортежей элементов уровня 0, например (AxB )= { x , y | P 6 ( x , A , y , B ) }, то уровень (AxB) = 0,0 K , уровень K будет 0, 0 F, уровень F будет 0 , 0 V, уровень V будет 0, 0 , 0 В общем случае, если у нас есть кортеж переменных из множества, мы все переменные заменяем на их уровни и получаем уровень множества, кому принадлежит кортеж. Здесь важно отметить роль интерпретации. При различных интерпретациях мы будем получать различные семантические значения предикатов и множеств истинности. Для предотвращения логических парадоксов мы ввели иерархию на множествах. В общем случае сами правила построения множеств могут быть устроены так, чтобы избежать возможных парадоксов. 6 Описание программного обеспечения Для построения семантических сетей используются программа VUE (Visual Understanding Environment), написанная в американском университете и свободно распространяемая [13]. На данный момент в программе реализован только синтаксис, семантика планируется в будущем. В программе из атомарных формул в «ручном» режиме строятся более сложные. Есть возможность сохранять построенные формулы с их описанием в вордовском файле. Есть возможность загружать и сохранять файлы в специальном формате. Ниже приведен пример построения около 30 формул. В начале есть четыре атомарные формулы: ( x 0 A 0 ), ( x 0 B 0 ), ( y 0 A 0 ), ( y 0 0 ). С помощью описанных выше правил строятся новые формулы. Интересно, что все основные понятия (сигнатура) теории множеств строятся из формул, чья длина по количеству атомарных не превышает двух. На рис.1-3 показаны интерфейсы программы для построения и просмотра формул. Рис.1. Стартовый интерфейс программы. Рис.2. Интерфейс для логического объединения формул. Рис.3. Таблица для работы с формулами. На Рис.4-5 показано построение семантической сети. В верхнем ряду атомарные формулы. Во втором их отрицания. Дальше построенные предикаты и множества. Рис.4. Обозначения, используемые для узлов и связей в семантической сети. Первая часть семантической сети. Рис.5. Вторая часть семантической сети. Таблица 1. Построенные формулы. N Формула Обозначение Символ Начальный текст Перевод на естественный язык 1 [ ( x 0 A 0 ) ] P 0 ( x 0 , A 0 ) 2 [ ( x 0 B 0 ) ] P 0 ( x 0 , B 0 ) 3 [ ( y 0 A 0 ) ] P 0 ( y 0 , A 0 ) 4 [ ( y 0 B 0 ) ] P 0 ( y 0 , B 0 ) 5 [ ( ( x 0 A 0 ) ) ] P 1 ( x 0 , A 0 ) 6 (x 0 ) [ ( x 0 A 0 ) ] P 2 ( A 0 ) A 0 =U A 0 -универсум 7 (A 0 ) [ ( x 0 A 0 ) ] P 3 ( x 0 ) 8 (x 0 ) [ ( x 0 A 0 ) ] P 4 ( A 0 ) A 0 A 0 -не пустое множество 9 (A 0 ) (x 0 ) [ ( x 0 A 0 ) ] P 5 ( ) TRUE аксиома 10 [ ( ( x 0 A 0 ) ( x 0 B 0 ) ) ] P 6 ( x 0 , A 0 , B 0 ) 11 [ ( ( x 0 A 0 ) ( x 0 B 0 ) ) ] P 7 ( x 0 , A 0 , B 0 ) 12 [ ( ( ( x 0 A 0 ) ) ( x 0 B 0 ) ) ] P 8 ( x 0 , A 0 , B 0 ) 13 [ ( (( x 0 A 0 ) ) ( x 0 B 0 ) ) ] P 9 ( x 0 , A 0 , B 0 ) 14 { x 0 | ( ( x 0 A 0 ) ( x 0 B 0 ) ) } M 0 ( A 0 , B 0 ) A 0 B 0 Пересечение множеств A 0 и B 0 15 { x 0 | ( ( x 0 A 0 ) ( x 0 B 0 ) ) } M 1 ( A 0 , B 0 ) A 0 B 0 Объединение множеств A 0 и B 0 16 { x 0 | ( (( x 0 A 0 ) ) ( x 0 B 0 ) ) } M 2 ( A 0 , B 0 ) B 0 \A 0 Разность множеств B 0 и A 0 17 ( A 0 B 0 ) P 10 ( A 0 , B 0 ) (x 0 )[ ( ( ( x 0 A 0 ) ) ( x 0 B 0 ) ) ] A 0 подмножество B 0 18 [ ( ( x 0 A 0 ) ( y 0 A 0 ) ) ] P 11 ( x 0 , A 0 , y 0 ) 19 [ ( ( x 0 A 0 ) ( y 0 B 0 ) ) ] P 12 ( x 0 , A 0 , y 0 , B 0 ) 20 { x 0 , y 0 | ( ( x 0 A 0 ) ( y 0 A 0 ) ) } D 0 ( A 0 ) A 0 xA 0 Декартово произведение A 0 и A 0 21 x 0 , y 0 D 0 ( A 0 ) P 011 ( x 0 , A 0 , y 0 ) 22 x 0 , y 0 G 0 ( A 0 ) P 13 ( x 0 , y 0 , G 0 ) 23 G 0 (A 0 ) D 0 ( A 0 ) P 14 ( A 0 , G 0 ) G 0 граф на A 0 (бинарное отношение на A 0 ) 24 { x 0 , y 0 | ( ( x 0 A 0 ) ( y 0 B 0 ) ) } D 1 ( A 0 , B 0 ) A 0 xB 0 Декартово произведение A 0 и B 0 25 { A 0 | ( A 0 B 0 ) } R 0 ( B 0 ) множество подмножеств B 0 26 ( (A 0 B 0 ) B 0 ) P 15 ( A 0 , B 0 ) В четвёртом столбце таблицы символьные обозначения, расширяющие изначальный язык (сигнатуру). Из предиката принадлежности мы получили включение, пересечение, объединение, дополнение, разность, декартово произведение множеств, множество-степень. Set; Set; , , ,x , Новые обозначения вписываются в таблицу (четвертый столбец) человеком, так как компьютер их не знает. Затем они переносятся в первый столбец, и программа продолжает работать уже с новыми обозначениями (в 17 строке уже перенесено). Включение, пересечение, объединение, дополнение - это семантические понятия теории множеств. Отношения между ними в нашей сети связаны со способом построения формул, которые обозначают эти понятия. Поэтому мы построили одновременно и синтаксическую и семантическую сеть. При построении множества истинности программа по желанию пользователя может построить предикат принадлежности этому множеству и построить подмножество этого множества (см. строки 21-23). Пользователь может выбрать обозначение для подмножества. 7 Устранение термов и доказательство теорем Мы в начале нашей программы c помощью логических операций из атомарных строим более сложные формулы, кроме применения логических операций мы можем множество истинности как терм подставлять в предикат. На всех множествах истинности существует иерархия (или типизация), чтобы избежать парадоксов. Есть операция замены переменных, при этом должен сохраняться уровень переменной. Например, в теории множеств есть теорема (A 0 B 0 ) B 0 =TRUE (строка 26 таблицы) (*) Пересечение двух множеств целиком лежит в каждом из множеств, это простая теорема для человеческого понимания. Чтоб получить теорему (A 0 B 0 ) B 0 =TRUE, нужно сделать замену в P 10 ( A 0 , B 0 ), A 0 заменить на A 0 B 0. ( A 0 B 0 )= (x 0 )[ ( ( ( x 0 A 0 ) ) ( x 0 B 0 ) ) ] Заменять переменные можно только одного уровня. P 10 ((A 0 B 0 ) , B 0 ) =TRUE Как её доказать формально? P 10 ((A 0 B 0 ) , B 0 ) = (x 0 )[ ( ( ( x 0 A 0 B 0 ) ) ( x 0 B 0 ) ) ] x 0 A 0 B 0 = ( x 0 A 0 ) ( x 0 B 0 ) P 10 ((A 0 B 0 ) , B 0 ) = (x 0 )[ ( (( x 0 A 0 ) ( x 0 B 0 ) ) ( x 0 B 0 ) ) ] P 10 ((A 0 B 0 ) , B 0 ) = (x 0 )[ ( ( x 0 A 0 ) ( x 0 B 0 ) ( x 0 B 0 ) ) ]= (x 0 )[ ( ( x 0 A 0 ) TRUE Использован закон Де Моргана при доказательстве A B)= A и закон исключенного третьего A A Это был пример одной подстановки при построении и много подстановок (замен) при доказательстве. При построении формул мы заменяем переменные. При доказательстве мы заменяем множество, которое было подставлено при построении «по определению». Далее расписываем предикат через атомарные формулы, затем, используя законы логики, упрощаем. Здесь использованы конкретные законы логики. Это был пример, где устраняется терм (A 0 B 0 ), и в формуле остаются только предикаты принадлежности (атомарные формулы), связанные логическими связками, кванторы можно всегда вынести вперёд. Можно привести к сколемовскому виду и далее использовать, например, метод семантических таблиц для доказательства теорем. Можно доказать, что множества истинности (термы, других термов нет) устранимы всегда. Мы всегда можем получить формулу только с атомарными предикатами принадлежности. Это ещё проще, так как в общем случае при доказательстве методом резолюций или методом семантических таблиц предикаты могут быть разные. Например x z[P(x, y)&Q(z, x) S(x, y, z)]. У нас будут только предикаты принадлежности. Например, x A[(P(x, A)&P(x, B) P(x, A)], т.е. двуместные несимметричные предикаты одного типа, но от разных переменных. Примеры других теорем: (C 0 ) (B 0 ) (A 0 ) ( ( A 0 B 0 ) ( B 0 C 0 ) ( A 0 C 0 ) ) =TRUE; A 1 A 0 A 1 ) =TRUE; A 1 A 1 A 0 ) A 1 A 0 При доказательстве примера (*) мы не использовали ни одной аксиомы теории множеств ZFC, нас не интересовал вопрос: конечны ли множества A и B. Мы пользовались определением включения и пересечения множеств и законами логики. Многие аксиомы теории множеств по сути являются определением пустого множества, объединения множеств, пары элементов. Интерпретация нашей системы задается на конечном или счетном наборе x i , A i , M i , R i Для логики предикатов первого порядка существуют стандартные алгоритмы автоматического доказательства. Метод резолюций и метод аналитических (семантических) таблиц описаны в [2,11]. Мы построили семантическую сеть понятий и утверждений из теории множеств. Компьютерная программа MathSem может использоваться как компьютерный практикум, например, по дискретной математике. Используя эту программу, можно изучать математическую логику, теорию множеств, теорию отношений, теорию графов, теорию групп. Это знакомит студентов с такими современными направлениями в науке как семантические сети, представление знаний, онтологии, логический вывод. Литература [1] Верещагин Н.К., Шень А. Языки и исчисления. М.: Изд-во МЦНМО, 2008. [2] Вагин В.Н., Головина Е.Ю., Загорянская А.А., Фомина М.В. . Достоверный и правдоподобный вывод в интеллектуальных системах.-M:Физматлит, 2004. [3] Захаров В.К. Локальная теория множеств.// Математические заметки- 2005 , c.194–212. [4] Лавров И.А. Математическая логика. М. :Академия, 2006. [5] Люксембург А.А. Автоматизированное построение математических теорий. М.: Изд-во УРСС, 2005. [6] Маслов С.Ю. Теория дедуктивных систем и ее применения - М.: Радио и связь, 1986. [7] Непейвода Н.Н. Прикладная логика. Учебное пособие. — Новосибирск, 2000. [8] Осипов Г.С. Лекции по искусственному интеллекту.-М.: Красанд, 2009. [9] Подколзин А.С. Компьютерное моделирование логических процессов. Архитектура и языки решателя задач. -М.: Физматлит, 2008. [10] Давыденко И.Т., Житко В.А., Заливако С.С., Корончик Д.Н., Мошенко С.Г., Савельева О.Ю., Старцев С.С., Шункевич Д.В. Интеллектуальная справочная система по геометрии - Минск -Труды конференции OSTIS, 2011. [11] Robinson J.A., Voronkov A. (Eds.). Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, 2001. [12] Stephen G. Simpson. Subsystems of Second Order Arithmetic, 2006. [13] Интернет, программа VUE http://vue.tufts.edu/about/index.cfm |