Опустим часть определения величины угла, запишем сразу в готовом виде:

◄O: <R[угла](O, a¹,a²) | M[a]{180}>

Смежные углы этот такие углы у которых один луч общий. Если применить оператор Sy к смежным углам по общему лучу, то углы объединяются в один угол, градусная мера которого равна сумме градусных мер смежных углов:

Op[угла](a¹,b¹ ,O) => ◄BOA: <R[угла]{O, b¹,a¹}>;

WEAK [( Sy[ma](◄BOA, g1) )]=> ◄BOA: <R[угла]{O, b¹,a¹}, M[a](g1)>

Op[угла](a¹,c¹ ,O) => ◄AOC: <R[угла]{O, a¹,c¹}>

WEAK [( Sy[ma](◄AOC, g1) )]=> ◄AOC: <R[угла]{O, a¹,c¹}, M[a](g2)>

Введем два новых продуцированных оператора: оператор построения дополнительного смежного угла (оператор смежности) и оператор деления угла на смежные (оператор деления угла).

Итак, применим оператор An по общему лучу и общей точке к углу BOC:

An[cl](◄BOC, O,a¹) => 
◄BOA: <R[угла]{O, b¹,a¹}, R[cl]{◄AOC, a¹}, M[a]{k}>;

◄AOC: <R[угла]{O, a¹,c¹}, R[cl]{◄BOA, a¹}, M[a]{n}>;

◄BOC: <R[угла]{O, b¹,c¹}, M[a]{g}| R[cl]{◄BOA, a¹},R[cl]{◄AOC, a¹} >;

где k+n = g

Элемент «Общий луч» включает в себя общую точку и общую линию с другими лучами.

Еще раз отметим, что индуцирование элемента ◄BOC создаст новый оператор, результатом применения которого будет не только разделение угла – операнда по общей линии, но и появление двух новых, смежных углов. Что вполне логично – продуцированные отношения деленного угла не могут указывать на не существующие элементы. Итак:

In(◄BOA: <R[угла]{O, b¹,a¹}, R[cl]{◄AOC, a¹}, M[a]{k}>;  => Op[деления-угла](◄, cl).

◄AOC: <R[угла]{O, a¹,c¹}, R[cl]{◄BOA, a¹}, M[a]{n}>;

◄BOC: <R[угла]{O, b¹,c¹}, M[a]{g}| R[cl]{◄BOA, a¹},R[cl]{◄AOC, a¹} >)

Новое определение угла будет выглядеть:

◄BOC: <R[угла]{O, b¹,c¹}|M[a]{k}| R[cl]{◄BOA, a¹},R[cl]{◄AOC, a¹} |Op[деления-угла](◄, cl) >

Далее подобно предыдущему оператору применим оператор Sy по общему лучу a¹ к углам ]◄BOA и ◄COA

Sy[cl](◄BOA, ◄COA, a¹) =>

◄BOC: <R[угла]{O, b¹,c¹}, M[a]{g= k+n}>

◄BOA: < R[угла]{O, b¹,a¹}, M[a]{k} | R[cl]{◄AOC, a¹}, >;

◄AOC: < R[угла]{O, a¹,c¹}, M[a]{n}| R[cl]{◄BOA, a¹} >;

где k+n = g

Про индуцируем любой из результатов применения Sy[cl]: ◄BOA или ◄AOC:

In(◄AOC: < R[угла]{O, a¹,c¹}| R[cl]{◄BOA, a¹}| M[a]{n} >) => Op[объединения углов по – a¹];

Полное определение угла ◄AOC будет выглядеть:

◄AOC :<R[угла]{O, a¹,c¹}, M[a](n) | Op[объединения углов по – a¹]>

Описание (прототип, сигнатура) индуцированного оператора специально везде опускается – для простоты демонстрации.

Теорема 4:

Сумма углов треугольника равно 180 градусам.

Доказательство теоремы в терминах геометрии сводится к построению

дополнительной прямой от одной из вершин треугольника параллельно противоположной стороне.

Из построения видно что если прямые a и d параллельные, то прямые на которых отложены отрезки AB и BC являются секущими. Таким образом,

◄D1BA = ◄BAC и далее ◄DBC = ◄CAB, так как они накрест лежащие, согласно данному построению углы ◄D1BA, ◄DBC и ◄ABC вместе составляют развернутый угол, таким образом сумма углов треугольника равна 180 градусам или развернутому углу.

Теперь докажем теорему в терминах теории сущностей:

1. Построим определение треугольника и прямую d:

Op[▲](A, B, C) => ▲ABC: <R[▲]{a,b,c, A, B,C}|

R[отрезка]{a, A, C}, R[угла]{A, a¹, b¹},

R[отрезка]{b, A, B}, R[угла]{B, b¹, c¹},

R[отрезка]{c, B, C}, R[угла]{C, c¹, a¹}| Op[▲]>

Прямая d проходит через точку B и параллельна прямой а:

Sy[sl]S => d:<Rs[sl]>

WEAK [( Sy[ptl](B, d) )] =>

d:<Rs[sl] | R[ptl]{B}>;

B:<R[▲]{a, b, c, A, C}| R[ptl]{d}, R[отрезка]{AB, b}, R[отрезка]{BC, c},

R[угла]{ b¹, c¹ } >

WEAK [( Sy[psl](a, d) )] =>

d: <Rs[sl] | R[ptl]{B}, R[psl]{a}>

a: <R[▲]{b, c, A, B, C}| R[отрезка]{A, B}, R[угла](A, b¹}, R[угла](A, с¹}, R[psl]{d}>

Тогда, по теореме доказанной выше имеем градусная мера углов равны:

◄D1BA = ◄BAC, ◄DBC = ◄ACB

2. Выпишем равные углы:

Согласно определениям геометрии равными углами в планиметрии называются углы градусная мера которых равна, то есть если ◄A = ◄B, определения углов должны соответствовать следующим формулам

◄A: <R[угла]{a¹,c¹}| M[a]{l}}>

◄B: <R[угла]{b¹,d¹}| M[a]{l}}>

Тогда определения вышеуказанных углов будет выглядеть как

◄D1BA = ◄BAC, ◄DBC = ◄ACB:

◄D1BA: < R[угла]{B, d²,b¹}| M[a]{n} >;

◄BAC: < R[угла]{b¹,a¹}| M[a]{n} >;

◄DBC: < R[угла]{d¹,c¹}| R[cl]{◄ABC, c¹}, M[a]{k} >;

◄ACB: < R[угла]{a¹,c¹}| M[a]{k} >;

Так как нас интересует только градусная мера углов, для построения доказательства будем далее использовать углы ◄D1BA, ◄DBC. Если мы сможем доказать что сумма углов ◄D1BA, ◄DBC и ◄ABC равна 180 градусам – значит теорема доказана.

3. Вывод.

Применяя композитивно оператор построения смежного угла «объединение углов по - ?»

последовательно к DBC, CBA получем объединенный угол D1BD.

WEAK [( Op[объединение углов по – c¹]

(◄DBC, (Op[объединение углов по - b¹](◄ABC, ◄D1BA, b¹ )), с¹ ) )]=>

◄D1BD: <R[угла]{O, d¹,d²}| M[a]{g= k+n+l}>

◄DBC: < R[угла]{d¹,c¹}| R[cl]{◄ABC, c¹}, M[a]{l} >;

◄ABC: < R[угла]{ b¹,c¹}| R[cl]{◄ABD1, b¹},R[cl]{◄DBC, c¹}, M[a]{k} >;

◄ABD1: < R[угла]{ b¹,d²}| R[cl]{◄ABC, b¹}, M[a]{n} >;

Как видно из вышеприведенной формулы новый угол (◄D1BD) образованный применением операторов – есть развернутый угол, то есть сумма углов составляющих его есть 180 градусов, но при построении этого развернутого угла использовались углы равные углам треугольника, то есть градусная мера всех углов треугольника также равна 180 градусам.

Дополнительные замечания

В выше приведенном примере многие моменты построения опущены, возможно, для чистоты демонстрации следовало бы выписывать все построения подробно и достаточно четко. Например, опущена часть работы с абстрактными элементами – выражения мер длин и углов. Не было демонстрации примеров применения оператора T (терминирования), а между тем данным оператором должны заканчиваться все теоремы и аксиомы. Опущены все детали применения оператора индукции и т.д. Это не значит, что данная работа не проводилась, скорее демонстрируемый пример был максимально упрощен, дабы показать основные моменты теории без излишних деталей и технических подробностей. Конечно, находясь, в начале развития своего развития теория покажется громоздкой не очень понятной и без достаточно серьёзной базы аксиоматизации.

Планиметрия как пример была взята потому что этот раздел математики не настолько абстрактен, как например, алгебра с одной стороны и не настолько конкретен как химия или физика. Абстрактные структуры данных сложнее представлять и ими сложнее манипулировать.

Так, например, классическая механика в физике может быть представлена существенно проще, чем школьный курс геометрии. В классической механики значительно меньше первичных чувственных восприятий и конец готовых сущностей.

Как уже было указано – математика, вернее её абстрактная числовая часть занимает особое место в теории – как подсистема элементов с пустым «чувственным восприятием». Данная подсистема безусловно также должна получить соответствующее развитие.

Что дальше?

Жизнеспособность каждой теории определяется её применимостью на практике.

В наш современный компьютерный критерием полезности подобной системы также является возможность её реализации в программном виде. То есть как некоторого компьютерного приложения. Реализация вышеизложенного примера из планиметрии – довольно бессмысленное занятие. Так как в лучшем случае – это будет весьма забавная игрушка, но не более того. Гораздо интереснее реализовать теорию в каком-нибудь из следующих видов:

1. Узко специфическое, но законченное приложение для целей хранения, развития и применения системы знаний в той или иной области деятельности человека.

2. Общая задача – создание систем, которые позволят общаться с компьютером на естественном языке

3. Старые, частично решенные задачи распознавания образов: визуально-статических, визуально-динамических, звуковых.

Итак для реальной модели будет выбрано одно из направлений и реализовано в виде компьютерного приложения.