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

Атомарными считаются формулы: 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