авторефераты диссертаций БЕСПЛАТНАЯ БИБЛИОТЕКА РОССИИ

КОНФЕРЕНЦИИ, КНИГИ, ПОСОБИЯ, НАУЧНЫЕ ИЗДАНИЯ

<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ


Pages:     | 1 |   ...   | 10 | 11 || 13 | 14 |

«В.В. Голенков, О.Е. Елисеева, В.П. Ивашенко, В.М. Казан Н.А. Гулякина, Н.В. Беззубенок, Т.Л. Лемешева, Р.Е. Сердюков И.Б. Фоминых ПРЕДСТАВЛЕНИЕ И ...»

-- [ Страница 12 ] --

anal yseStruct ure fi Goals /* необязательное условие – дуга из a n a l y s e S t r u c t u r e */ Операция анализирует структуру неатомарных формул входящих в связку q i отношения a s s o c i a t i v e и формирует связки отношения бинарного структурного включения i n c l u s i o n между формулами.

Если две формулы взаимно включают друг друга по структуре, и кванторы, которые навешены на переменные формул совпадают, то между такими формулами формируется связка отношения синонимии.

Результатом применения операции могут быть конструкции вида:

( ( formula Formula1 ), in_ : ( formula Formula2 ) ) ;

inclusion Formula1 Formula2 ;

Операция выполнения логических рассуждений (SCL reasoning operation).

Условием выполнения операции выполнения логических рассуждений является наличие конструкции вида:

deduce gq qi /* необходимое условие – дуга g q */ 338 Раздел 1. 0BГрафодинамические ассоциативные машины вывода Операция находит элемент v x включённой в связку q i отношения r e a s o n i n g, помеченный атрибутом e x p e c t a t i o n s _, проверяет являются ли все элементы найденного множества v x запросами, на которые получен ответ и если это так, то операция находит g a – компонент связки q i, помеченный атрибутом e f f e c t _. Если g a включён во множество d e n y _, то он также включается во множество d e n i e d _. Если g a включён во множество c o n f i r m _, то он также включается во множество c o n f i r m e d _. Если связка q i включена во множество временных конструкций, то она удаляется.

М и к р о п р о г р а м м а операции выполнения логических рассуждений имеет следующий вид:

Ш а г 1. Вначале операция проверяет структуру запроса: в качестве допустимой разрешается структура запроса только следующего вида, когда узел запроса является знаком связки отношения r e a s o n i n g :

qi ;

reasoning Ш а г 2. Если проверка структуры запроса осуществлена безуспешно, то операция завершается с возвратом ошибки, иначе – удаляется дуга g q.

Ш а г 3. Отыскивается константная позитивная дуга g e, выходящая из узла q i и помеченная атрибутом e f f e c t _. Если поиск осуществлён безуспешно, то операция завершается с возвратом ошибки.

Ш а г 4. Ищется константная позитивная дуга g a, выходящая из узла G o a l s, входящая в искомый константный узел v a, в которую входит дуга g e. Если поиск осуществлён безуспешно, то операция завершается с возвратом ошибки.

Ш а г 5. Ищется константная позитивная дуга, выходящая из узла q i, входящая в искомый константный узел v x и помеченная атрибутом e x p e c t a t i o n s _. Если поиск осуществлён безуспешно, то осуществляется переход на шаг 7.

Ш а г 6. Во множестве v x отыскиваются элементы, которые не входят ни во множество d e n i e d _, ни во множество c o n f i r m e d _. Если найден хотя бы один такой элемент, то операция завершается успешно, иначе – удаляется узел v x.

Ш а г 7. Если дуга g a, включена хотя бы в одно из множеств d e n i e d _ и c o n f i r m e d _, то операция завершается успешно.

Ш а г 8. Если дуга включена во множество c o n f i r m _, то осуществляется генерация конструкции, удовлетворяющей образцу задаваемому узлом v a. Генерируемая конструкция включается в формулу, являющуюся соответствующим фактографическим высказыванием (либо квазиатомарной логической формулой), формируется полное соответствие интерпретации между образцом v a и сгенерированной формулой. В дугу v a генерируется дуга из узла c o n f i r m e d _.

Ш а г 9. Если дуга включена во множество d e n y _, то осуществляется генерация квазиатомарной формулы f j, удовлетворяющей образцу задаваемому узлом v a. Генерируемая конструкция включается в формулу f j, формируется полное соответствие интерпретации между образцом v a и сгенерированной формулой f j. В дугу v a генерируется дуга из узла d e n i e d _.

Ш а г 1 0. При наличии константной позитивной дуги из узла t e m p o r a r y в узел q i. Генерируется константная позитивная дуга из узла r e l e a s e в узел q i.

Ш а г 1 1. Операция завершается успешно.

Конец микропрограммы.

Операция реализации продукции (SCL producing operation).

Условием выполнения операции реализации продукции является наличие sc-конструкции вида:

t heory ti gi ini t_ al l ai fi i mpl Операция находит левую часть импликативной формулы f i и ищет формулу r i релевантную этой части. Если левая часть является атомарной формулой, то поиск новой формулы заключается в поиске структуры, которая является фрагментом обобщённого атомарного (фактографического) высказывания теории t i, структуры, изоморфной этой атомарной формуле с учётом привязки констант, и формировании узла, из которого проводятся константные позитивные дуги во все найденные элементы структуры, являющегося знаком искомой формулы. Если же левая часть является сложной формулой, то осуществляется поиск релевантной ей формулы, которая включена во множество t i. Между левой частью импликации и найденной релевантной ей формулой r i формируется конструкция отношения релевантности, в рамках которой каждая переменная формулы, являющейся левой частью импликации получает своё значение – константу, включённую в какую-либо атомарную формулу формулы r i. Затем операция находит правую часть формулы f i, которая является атомарной формулой и формирует релевантную ей формулу v n, являющуюся фактографическим высказыванием, структура которого изоморфна правой части импликации с учётом привязки констант. Затем все значения тех переменных из найденных левой и правой частей импликации, которые связаны квантором общности в рамках кванторной формулы a i, склеиваются.

Дуга g i удаляется. Элементы сформированной формулы v n добавляются в обобщённое атомарное (фактографическое) высказывание теории t i, а сама формула включается в теорию t i.

Результатом выполнения операции реализации продукции является следовательно конструкция вида:

theory i ni t_ vn ai 340 Раздел 1. 0BГрафодинамические ассоциативные машины вывода Приведём пример выполнения данной операции. При наличии в базе знаний конструкции:

t heory uni on_ точка прямая ti fix_ gi init _ ai _a _b al l fi impl if_ t hen_ прямая точка _a _a _b _b atExpr exi st At Expr после выполнения операции реализации продукции мы получим следующую конструкцию:

theory union_ точка ti fi x_ i ni t _ ai _a _b al l прямая fi i mpl if_ then_ прямая точка _a _b _a atExpr _b exi st AtExpr М и к р о п р о г р а м м а операции реализации продукции имеет следующий вид:

Ш а г 1. Вначале операция осуществляет поиск неизвестных элементов конструкции, являющейся условием выполнения этой операции. Такими неизвестными элементами являются все элементы вышеприведённой конструкции-условия за исключением ключевых узлов: “ t h e o r y ”, “ i n i t _”, “ a l l ” и “ i m p l ”. В ходе выполнения этого шага операция находит, в частности, такие соответствующие элементы вышеприведённой конструкции-условия как: константную позитивную дугу g i, выходящую из ключевого узла “ i n i t _”, константный узел t i, являющийся знаком формальной теории, константный узел a i, являющийся знаком кванторной формулы, являющейся в рамках теории t i истинным высказыванием о всеобщности, а также константный узел f i, являющийся знаком импликативной формулы.

Ш а г 2. Если хотя бы один из элементов g i, t i, a i и f i или хотя бы одна соответствующая константная позитивная дуга из вышеприведённой конструкции не найдена на предыдущем шаге, то операция завершает свою работу, иначе – удаляется дуга g i.

Ш а г 3. Осуществляется поиск константного узла v c, в который входит константная позитивная дуга, выходящая из узла f i, которая является элементом ключевого множества “ i f _”. Из этого следует, что искомый узел v c является посылкой импликативной формулы f i. Таким образом формула f i и её посылка связаны между собой конструкцией вида:

if_ : vc ;

fi Ш а г 4. Осуществляется поиск константного узла v e, в который входит константная позитивная дуга, выходящая из узла f i, которая является элементом ключевого множества “ t h e n _”. Из этого 342 Раздел 1. 0BГрафодинамические ассоциативные машины вывода следует, что искомый узел v c является следствием импликативной формулы f i. Таким образом формула f i и её следствие связаны между собой конструкцией вида:

then_ : ve ;

fi Ш а г 5. Осуществляется поиск константного узла v f, в который входит константная позитивная дуга, выходящая из узла a i, которая является элементом ключевого множества “ f i x _”. Из этого следует, что искомый узел v f является множеством переменных связываемых квантором общности в рамках кванторного высказывания о всеобщности a i. Таким образом искомое множество связываемых переменных и кванторная формула a i связаны между собой конструкцией вида:

fix_ : vf ;

ai Ш а г 6. Проверяется наличие константной позитивной дуги, выходящей из узла, являющегося одним из двух таких ключевых узлов как: “ a t E x p r ” и “ e x i s t A t E x p r ”, и входящей в узел v c : если такой дуги нет, то осуществляется переход на шаг 30, иначе – наличие такой дуги означает что, посылка v c является атомарной формулой, либо кванторной формулой о существовании интерпретации атомарной формулы.

ci “релевантность sc Шаг 7. Осуществляется поиск связки отношения к о н с т р у к ц и й ”, которая включает узел v s, являющийся знаком связки, включающего формулу v c и узел “ 1 _ ” под атрибутом “ а т р и б у т _ ”. Таким образом искомая связка и известные формула v c и отношение “ р е л е в а н т н о с т ь s c - к о н с т р у к ц и й ” связаны конструкцией вида:

релевантность sc-конструкций атрибут_ ci vs 1_ vc Если такая связка не найдена, то осуществляется переход на шаг 14.

Шаг 8.

Ш а г 9. Осуществляется поиск узла r i отличного от узла v c, который включён в одно из таких множеств как: “ a t E x p r ” и “ e x i s t A t E x p r ”, который также включён в искомую пару s d одновременно с узлом“ 2 _ ” под атрибутом “ а т р и б у т _ ”, в которую проведена константная позитивная дуга, выходящая из связки c i и не включённая во множество “ о т н о ш е н и е _ ”. Если узел r i не найден, то осуществляется переход на шаг 14.

Ш а г 1 0. Осуществляется поиск узла i i, в который проведена константная позитивная дуга из узла c i, в которую входит константная позитивная дуга из ключевого узла “ о т н о ш е н и е _ ”. Если узел i i найден, то осуществляется переход на шаг 18.

Ш а г 1 1. Элементы множества r i и только они включаются во множество, обозначенное узлом u f.

Ш а г 1 2. Множество r i очищается, то есть удаляются все выходящие из него константные позитивные дуги.

Ш а г 1 3. Осуществляется переход на шаг 16.

Ш а г 1 4. Осуществляется поиск всех элементов, в которые входят константные позитивные дуги из узла v c, если ни один такой элемент не найден, то операция завершается с возвратом ошибки.

Ш а г 1 5. Осуществляется поиск константного узла u f, в который входит константная позитивная дуга, выходящая из узла t i, которая является элементом ключевого множества “ u n i o n _”. Из этого (фактографическим) следует, что искомый узел u f является обобщённым атомарным высказыванием формальной теории t i. Таким образом теория t i и формула u f связаны между собой конструкцией вида:

union_ : uf ;

ti Ш а г 1 6. Осуществляется поиск конструкции, являющейся фрагментом конструкции, включенной во множество u f, – поиск фрагмента изоморфного (с учётом привязки констант) конструкции, которую образуют все элементы, найденные на четырнадцатом шаге. Искомый фрагмент – искомая конструкция будет являться изоморфной с учётом привязки констант в том и только в том случае, если каждому переменному узлу или переменному элементу неопределённого типа, найденному на четырнадцатом шаге соответствует некоторый константный узел или константный элемент соответственно, каждому константному узлу, дуге или элементу неопределённого типа – он сам, каждой переменной дуге – константная дуга аналогичной степени чёткости, выходящая из узла искомой конструкции, соответствующего узлу, из которого выходит переменная дуга, и входящая в элемент искомой конструкции, соответствующий элементу, в который входит переменная дуга, когда других элементов в искомой конструкции нет, причём для каждого элемента, найденного на четырнадцатом шаге соответствует один единственный элемент искомой конструкции. Все элементы искомой конструкции и только они включаются во множество, обозначенное узлом r i. Каждый элемент искомой конструкции e s, соответствующий какому-либо найденному на четырнадцатом шаге переменному элементу e i, связывается с этим переменным элементом ориентированной парой – парой вида:

( 1_ : ei, 2_ : es ) ;

Ш а г 1 7. Если поиск изоморфной конструкции прошёл безуспешно, то осуществляется переход на шаг 28, иначе – все сформированные на предыдущем шаге ориентированные пары и только они включаются во множество, обозначенное узлом i i.

Ш а г 1 8. Если узел c i не был найден (на седьмом шаге), то генерируется связка отношения “ р е л е в а н т н о с т ь s c - к о н с т р у к ц и й ”, в которую включаются узлы r i и v c и только. Формула r i добавляется во множество t i.

сi ii Шаг 19.В случае отсутствия, во множество добавляется узел под атрибутом “отношение_”.

Ш а г 2 0. Проверяется наличие константной позитивной дуги, выходящей из узла, являющегося одним из двух таких ключевых узлов как: “ a t E x p r ”, “ e x i s t A t E x p r ”, и входящей в узел v e : если такой дуги нет, то осуществляется переход на шаг 28, иначе – наличие такой дуги означает что, посылка v e является атомарной формулой, либо кванторной формулой о существовании интерпретации атомарной формулы.

344 Раздел 1. 0BГрафодинамические ассоциативные машины вывода Ш а г 2 1. Генерируются узлы v n, v r, v o и i n. Генерируется конструкция вида:

vo in vr атрибут_ 1_ ve vn 2_ Ш а г 2 2. Во множество i n включается каждая ориентированная пара b i, включённая во множество i i и имеющая в качестве первого элемента какую-либо переменную _ V a r, включённую во множества v f и v e, то есть пара, связанная конструкцией вида:

ve ii vf 1_ bi _Var Ш а г 2 3. Во множество v n включается каждый элемент e v, являющийся вторым элементом хотя бы одной ориентированной пары b i, включённой во множество i n, то есть элемент, связанный конструкцией вида:

: ev ;

in bi 2_ Ш а г 2 4. Каждый константный элемент множества v e включается во множество v n.

Ш а г 2 5. Для каждого переменного узла или переменного элемента неопределённого типа, включённого во множество v e и не включённого во множество v f, генерируется и включается во множество v n константный узел или константный элемент неопределённого типа соответственно. Для каждого генерируемого константного элемента генерируется включаемая во множество i n ориентированная пара, включающая в качестве второго этот генерируемый элемент, а в качестве первого – переменный элемент, соответствующий генерируемому константному элементу.

Ш а г 2 6. Для каждой переменной дуги, включённой во множество v e и не включённой во множество v f, генерируется и включается во множество v n константная дуга аналогичной степени чёткости, выходящая из узла, лежащего во множестве v n, соответствующего узлу, из которого выходит переменная дуга, и входящая в элемент, лежащий во множестве v n, соответствующий элементу, в который входит переменная дуга. Для каждой генерируемой константной дуги генерируется включаемая во множество i n ориентированная пара, включающая в качестве второго эту генерируемую дугу, а в качестве первого – переменную дугу, соответствующую генерируемой константной дуге.

Ш а г 2 7. Генерируется связка отношения “ р е л е в а н т н о с т ь s c - к о н с т р у к ц и й ”, в которую включаются узлы v o и v r, а также узел i n под атрибутом “ о т н о ш е н и е _ ” и только. Формула v n добавляется во множества t i и “ a t E x p r ”. Все не добавленные элементы множества v n добавляются в обобщённое атомарное (фактографическое) высказывание u f формальной теории t i, связанное с теорией t i конструкцией вида:

union_ : uf ;

ti Ш а г 2 8. Осуществляется переход на шаг 34.

Ш а г 2 9. Если узел r i был найден на девятом шаге, то операция завершается с возвратом ошибки, иначе – осуществляется переход на шаг 28.

Ш а г 3 0. Проверяется наличие константной позитивной дуги, выходящей из узла, являющегося одним из двух таких ключевых узлов как: “ a l l ”, “ a l l E q E x p r ”, “ a l l I m p l ”, “ a l t ”, “ c o n j ”, “ d i s j ”, “ e x i s t ”, “ e q E x p r ” и “ i m p l ”, и входящей в узел v e : если такой дуги нет, то осуществляется переход на шаг 28.

Ш а г 3 1. Осуществляется поиск константного узла r i, в который проведена константная позитивная дуга из узла t i. Искомый узел r i кроме этого должен являться формулой релевантной формуле v c. В процессе поиска формируется связка c i отношения “ р е л е в а н т н о с т ь л о г и ч е с к и х ф о р м у л ”, в которую включены узел v s, являющийся знаком связки, в которую включен узел “ 1 _ ” под атрибутом “ а т р и б у т _ ” и узел s c, включающий всю структуру формулы v c. В связку c i также должен быть включён узел v d, являющийся знаком связки, в которую включен узел “ 2 _ ” под атрибутом “ а т р и б у т _ ” и узел s r, включающий всю структуру формулы r i. Кроме этого в связку c i также должен быть включён узел i i под атрибутом “ о т н о ш е н и е _ ”, являющийся знаком множества, ориентированных пар соответствия релевантности, которые выходят из элементов множества s c в соответствующие элементы множества s r. Таким образом искомые на данном шаге элементы в итоге будут связаны конструкцией вида:

релевантность лог ических формул ci отношение_ атрибут_ vd ii vs sr sc 2_ 1_ ri vc......

Ш а г 3 2. Если такой узел r i не найден, то осуществляется переход на шаг 28.

Ш а г 3 3. Осуществляется переход на шаг 20.

Ш а г 3 4. Работа операции успешно завершается.

Конец микропрограммы.

346 Раздел 1. 0BГрафодинамические ассоциативные машины вывода Операция обработки положительного ответа на запрос (SCL positive answer processing operation).

Условием выполнения операции обработки положительного ответа на запрос является наличие конструкции вида:

confirmed_ fi Goals /* необходимое условие – дуга из c o n f i r m e d _ */ Операция анализирует: не является подтверждённый запрос какой-либо ожидаемой И-подцелью и если это так, то операция переносит подцель из разряда ожидаемых (из компонента соответствующей связки отношения r e a s o n i n g, помеченного атрибутом e x p e c t a t i o n s _ ) в достигнутые (в компонент этой связки, помеченный атрибутом c a u s e s _ ), создавая условия для применения операции выполнения логических рассуждений.

Операция обработки отрицательного ответа на запрос (SCL negative answer processing operation).

Условием выполнения операции обработки отрицательного ответа на запрос является наличие конструкции вида:

deni ed_ fi Goal s /* необходимое условие – дуга из d e n i e d _ */ Операция анализирует: не является опровергнутый запрос какой-либо ожидаемой И-подцелью и если это так, то операция переносит подцель из разряда ожидаемых (из компонента соответствующей связки отношения r e a s o n i n g, помеченного атрибутом e x p e c t a t i o n s _) в достигнутые (в компонент этой связки, помеченный атрибутом c a u s e s _ ), создавая условия для применения операции выполнения логических рассуждений.

Операция уничтожения промежуточных конструкций (SCL structure releasing operation). Операция уничтожает все конструкции, которые включены во множество удаляемых конструкций.

Операция склейки идентичных формул (SCL formula optimizing operation). Операция склеивает две синонимичные формулы.

Операция добавления факта (SCL fact adding operation). Операция добавляет факт в SCL теорию, если он не противоречит другим фактам и высказываниям.

Операция добавления высказывания (SCL expression adding operation). Операция добавляет высказывание в SCL теорию, если оно не противоречит фактам и другим высказываниям.

Более подробное рассмотрение операций абстрактной scl-машины приведено в работах (Г о л е н к о в В. В.. 1 9 9 5 м о - О п е р а Я S C L д О П З ;

Голенков В.В..1995мо [148;

150, 153] Р е ш е н Н Я S C L З и О Г ;

Г о л е н к о в В. В.. 1 9 9 6 м о - Б а з о в П Т Я S C L ).

348 Раздел 1. 0BГрафодинамические ассоциативные машины вывода 1.2. Решение задач в графодинамических ассоциативных машинах вывода К л ю ч е в ы е п о н я т и я : задача, решение задачи, аксиома, определение, вывод.

Рассмотрим решение задач (см. уточнение понятия задача в подразделе 6.3) на SCL. Пусть нам необходимо доказать, что существуют две параллельные прямые. Мы обладаем следующей исходной информацией.

Условие задачи:

/* Описание формальной теории из области планиметрии */ atExpr theory union_ Планиметрия точка прямая точка неопределяемые понятия _ Pln_basis прямая теория_ аксиомы_ аксиоматика параллельность /* Формирование аксиоматики */ /* “через не лежащую на прямой точку можно провести параллельную этой прямой прямую и только одну” */ Pl n_basi s all Impl Аксиома о параллельной прямой then_ PSA_effect i f_ параллельность conj PSA_cause прямая negExpr _sf PSA_neg прямая _sf _p _ss точка _p PSA_at om _p _sf PSA_neg_at om exi stAtExpr pwExi st 350 Раздел 1. 0BГрафодинамические ассоциативные машины вывода /* “для каждой прямой существуют точки принадлежащие ей и не принадлежащие ей” */ Pl n_basis al lImpl Аксиома о прямой then_ i f_ SA_effect conj SA_cause SA_effect _neg_atom прямая точка точка _s _s _p _p _s SA_effect_at om exi st At Expr /* “через любые две точки можно провести прямую и только одну” */ Pl n_basi s all Impl Аксиома о прямой и двух точках then_ if_ SPPA_effect SPPA_cause прямая точка _s _a _b _a _b existAtExpr pwExi st /* “существуют две точки” */ Pl n_basi s точка exi st AtExpr _a _b Аксио ма о существовании дву х точек /* “две прямые параллельны тогда и только тогда, когда ни одна точка не принадлежит их пересечению” */ Pln_basi s al lEqExpr Определение параллельности PD_at om параллельность all PD_def fix_ PD_def_fi x _sf пересечение результат_ _a _ss _i _a _e _ss _sf _e прямая точка PD_def_at om existAtExpr pwExi st /* “если элемент принадлежит прямой, то этот элемент – точка” */ 352 Раздел 1. 0BГрафодинамические ассоциативные машины вывода all Impl if_ t hen_ Pl n_basis Свойство прямой SP_cause SP_effect прямая точка _s _s _p _p SP_effect _effect SP_effect _cause existAtExpr /* “фигура прямолинейна тогда и только тогда, когда существует прямая включающая все элементы фигуры” */ Определение прямолинейной фигуры ;

Pln_basis Определение прямолинейной фигуры ;

allEqExpr SFD_def, SFD_atom ;

Определение прямолинейной фигуры SFD_atom ;

existAtExpr SFD_atom [ прямолинейная фигура _f ;

] ;

SFD_def ;

exist SFD_def ;

existAtExpr SFD_def [ подмножество (· п о д м н о ж е с т в о _ : _f, м н о ж е с т в о _ : _s ·) ;

_s ;

] ;

прямая /* “пересечением произвольного количества множеств является множество, включающее такие и только такие элементы, каждый из которых принадлежит каждому множеству, образующему пересечение” */ Set_basis ;

Pln_basis Определение пересечения ;

Set_basis Определение пересечения ;

conj DD_forward, DD_backward ;

Определение пересечения DD_forward, DD_backward ;

allImpl if_ : DD_def_f, then_ : DD_atom ;

DD_forward if_ : DD_atom, then_ : DD_def_b ;

DD_backward DD_atom ;

existAtExpr DD_atom [ пересечение _c ;

] ;

DD_def_f ;

exist fix_ : DD_fix, DD_def_conj ;

DD_def_f DD_def_b ;

exist fix_ : DD_fix, DD_def_equivalence ;

DD_def_b D D _ f i x [ _d ] ;

DD_def_equivalence ;

allEqExpr DD_def_conj ;

conj DD_def_equivalence_equivalence, DD_def_atom ;

DD_def_conj DD_def_equivalence_equivalence, DD_def_atom ;

DD_def_equivalence DD_def_atom ;

existAtExpr D D _ d e f _ a t o m [ _c р е з у л ь т а т _ : : _d ;

] ;

DD_def_equivalence_equivalence ;

allEqExpr DD_equivalence_atom, DD_implication ;

DD_def_equivalence_equivalence DD_equivalence_atom ;

existAtExpr D D _ e q u i v a l e n c e _ a t o m [ _d _e ;

] ;

DD_implication ;

allImpl if_ : DD_cause, then_ : DD_effect ;

DD_implication DD_cause, DD_effect ;

existAtExpr D D _ c a u s e [ _c _s ;

] ;

D D _ e f f e c t [ _s _e ;

] ;

/* “множество _s s является подмножеством множества _s, если каждый элемент _s s принадлежит множеству _s ” */ Определение подмножества ;

Set_basis Определение подмножества ;

conj SSD_forward, SSD_backward ;

Определение подмножества SSD_forward, SSD_backward ;

allImpl if_ : SSD_def_f, then_ : SSD_atom ;

SSD_forward if_ : SSD_atom, then_ : SSD_def_b ;

SSD_backward SSD_atom ;

existAtExpr SSD_atom [ подмножество _c ;

] ;

SSD_def_f ;

exist fix_ : SSD_fix, SSD_def_conj ;

SSD_def_f S S D _ f i x [ _s s, _s ] ;

SSD_def_conj ;

conj SSD_def_b ;

allEqExpr SSD_def_atom, SSD_implication ;

SSD_def_b SSD_def_atom, SSD_implication ;

SSD_def_conj SSD_def_atom ;

existAtExpr S S D _ d e f _ a t o m [ _c п о д м н о ж е с т в о _ : : _s s, м н о ж е с т в о _ : : _s ;

] ;

SSD_implication ;

allImpl if_ : SSD_cause, then_ : SSD_effect ;

SSD_implication SSD_cause, SSD_effect ;

existAtExpr 354 Раздел 1. 0BГрафодинамические ассоциативные машины вывода S S D _ c a u s e [ _s s _e ;

] ;

S S D _ e f f e c t [ _s _e ;

] ;

Далее следует формулировка запроса.

/* “существуют параллельные прямые” */ query_atom1 ;

existAtExpr query_atom1 [ параллельность (·_a, _c ·) ;

п р я м а я _a, _c ;

] ;

Приведём описание решения задачи на естественном языке.

Процесс решения состоит из следующих этапов:

1) определение множества формальных теорий описывающих закономерности свойств понятий, обозначенных константными элементами в запросе;

2) для конкретной теории заранее формируется множество целей (запросов) и множество предположений;

3) начинается обработка запроса, определяется тип высказывания запроса;

4) проверяется выводимость отрицания высказывания в рамках формальной теории, перебираются все истинные интерпретации (этапы 5, 6), каждая интерпретация на каждом этапе и только на нём включается во множество предположений;

5) осуществляется поиск семантически близких истинных высказываний формальной теории, при необходимости используются факты формальной теории, в данном примере такими высказываниями изначально являются: “ А к с и о м а о п а р а л л е л ь н о й п р я м о й ”, “ А к с и о м а о п р я м о й ”, “Определение параллельности”, “Cвойство прямой”, “Определение п р я м о л и н е й н о й ф и г у р ы ” и т. п. ;

6) осуществляется протоколирующийся логический вывод с помощью отобранных на предыдущем этапе высказываний, этапы 5 и 6 повторяются, пока не закончатся семантически близкие высказывания или будет выявлено противоречие, в последнем случае высказывание ложно и при условии возникновения противоречия на каждой истинной интерпретации осуществляется переход на этап 10;

7) проверяется выводимость высказывания в рамках формальной теории, перебираются все ложные интерпретации (этапы 8, 9), каждая интерпретация на каждом этапе и только на нём включается во множество предположений;

8) осуществляется поиск семантически близких истинных высказываний формальной теории, при необходимости используются факты формальной теории;

9) осуществляется протоколирующийся логический вывод с помощью отобранных на предыдущем этапе высказываний, этапы 8 и 9 повторяются, пока не закончатся семантически близкие высказывания или будет выявлено противоречие, в последнем случае высказывание истинно;

10) на основании результатов полученных на этапах 6 и 9, формируется ответ: истинно ли, ложно или невыводимо высказывание в рамках текущей формальной теории;

уничтожается множество предположений, выводится протокол решения;

11) процесс повторяется со второго этапа для каждой найденной формальной теории.

Рассмотрим более детально этот процесс для данного примера.

На первом этапе анализируются все константные элементы, входящие хотя бы в одно из атомарных высказываний запроса. В данном случае это элементы: “п р я м а я ”, “п а р а л л е л ьн о с т ь ”, то есть те элементы, которые также входят во множество, помеченное атрибутом “u n i o n _” в рамках какой-либо формальной теории. На основе этого анализа осуществляется построение множества “t h e o r y _ s e t ” всех таких формальных теорий. В данном примере множество “t h e o r y _ s e t ” будет содержать элемент “П л а н и м е т р и я ”.

На втором этапе формулируется запрос к каждой формальной теории:

query1 ;

Goals gq active_, confirm_ gq1 ;

query1 [ theory query_atom1 ] ;

Планиметрия На третьем этапе начинается обработка запроса (распишем последующие этапы по шагам) :

Ш а г 1. К запросу “q u e r y 1 ” применяется операция классификации и управления запросами, которая формирует конструкцию следующего вида:

search : query1 ;

Goals Ш а г 2. К запросу “q u e r y 1 ” применяется операция эпизодического информационного поиска.

Которая завершается безуспешно:

active_ : searched : query1 ;

Goals query1 ;

factual Ш а г 3. К запросу “q u e r y 1 ” применяется операция классификации и управления запросами, которая формирует конструкцию следующего вида:

traceUp : query1 ;

Goals Ш а г 4. К запросу “q u e r y 1 ” применяется операция трассировки запроса снизу-вверх в сложном высказывании, которая завершается безуспешно:

tracedUp : active_ : query1 ;

Goals Ш а г 5. К запросу “q u e r y 1 ” применяется операция классификации и управления запросами, которая формирует конструкцию следующего вида:

traceDown : query1 ;

Goals Ш а г 6. К запросу “q u e r y 1 ” применяется операция трассировки запроса сверху-вниз, которая формирует конструкцию следующего вида:

query1 ;

Goals gq tracedDown, active_ gq1 ;

(e f f e c t _ : g q 1, e x p e c t a t i o n s _ : (g x 1 ), c a u s e s _ : C 1 ) ;

reasoning query_atom1 ;

Goals gx tracedUp, confirm_, active_ gx1 ;

Ш а г 7. К запросу “q u e r y _ a t o m 1 ” применяется операция классификации и управления запросами, которая формирует конструкцию следующего вида:

search : query_atom1 ;

Goals Ш а г 8. К запросу “q u e r y _ a t o m 1 ” применяется операция эпизодического информационного поиска. Которая завершается безуспешно:

active_ : searched : query_atom1 ;

Goals query_atom1 ;

factual 356 Раздел 1. 0BГрафодинамические ассоциативные машины вывода Ш а г 9. К запросу “q u e r y _ a t o m 1 ” применяется операция классификации и управления запросами, которая формирует конструкцию следующего вида:

a s s o c i a t e S i m p l y : (a s s o c i a t i v e (· Goals ( formula query_atom1 ), ( theory П л а н и м е т р и я ), _a s ·) ;

Ш а г 1 0. К атомарному высказыванию “q u e r y _ a t o m 1 ” применяется операция простого ассоциирования атомарных формул. Среди таких формул будут формулы: “P S A _ a t o m ”, “P S A _ e f f e c t ”, “S A _ c a u s e ”, “S P P A _ e f f e c t ”, “P D _ d e f _ a t o m ”, “P D _ a t o m ”, “S P _ c a u s e ”, “S F D _ d e f ”. Будет построена конструкция:

( ( formula query_atom1 ), ( theory Планиметрия ), associative (P S A _ a t o m, P S A _ e f f e c t, S A _ c a u s e, S P P A _ e f f e c t, P D _ d e f _ a t o m, P D _ a t o m, S P _ c a u s e, S F D _ d e f )) ;

active_ : query_atom1 ;

Goals Ш а г 1 1. К атомарному высказыванию “q u e r y _ a t o m 1 ” применяется операция выявления идентичных, входящих и пересекающихся атомарных формул. Результатом применения операции будут конструкции:

( ( formula PSA_atom ), in_ : ( formula SP_cause ) ) ;

inclusion ( ( formula PSA_atom ), in_ : ( formula SA_cause ) ) ;

inclusion SA_cause [ прямая _s ] ;

/* q a 1 _ P S A a _ i n t e r s e c t i o n */ ( ( formula query_atom1 ), in_ : ( formula PD_atom ) ) ;

inclusion ( ( formula PSA_effect ), in_ : ( formula PD_atom ) ) ;

inclusion ( ( formula PSA_effect ), in_ : ( formula SP_cause ) ) ;

inclusion ( ( formula PSA_effect ), in_ : ( formula SA_cause ) ) ;

inclusion PD_atom [ параллельность (·_s f, _s s ·) ;

] ;

/* q a 1 _ P S A e _ i n t e r s e c t i o n */ ( ( formula SPPA_effect ), in_ : ( formula SP_cause ) ) ;

inclusion ( ( formula SPPA_effect ), in_ : ( formula SA_cause ) ) ;

inclusion SA_cause [ прямая _s ] ;

/* q a 1 _ S P P A e _ i n t e r s c t n */ ( ( formula query_atom1 ), in_ : ( formula inclusion qa1_PDda_intersection ) ) ;

( ( formula PD_def_atom ), inclusion in_ : ( formula qa1_PDda_intersection ) ) ;

qa1_PDda_intersection [ прямая _s 1, _s 2 ;

] ;

( ( formula qa1_PDda_intersection ), in_ : ( formula inclusion SP_cause ) ) ;

( ( formula qa1_PDda_intersection ), in_ : ( formula inclusion SA_cause ) ) ;

( ( formula SFD_def ), in_ : ( formula SP_cause ) ) ;

inclusion ( ( formula SFD_def ), in_ : ( formula SA_cause ) ) ;

inclusion ( formula SP_cause ) ( formula SA_cause ) ;

Ш а г 1 2. К атомарным формулам “S A _ c a u s e ” и “S P _ c a u s e ” применяется операция склейки атомарных формул: в результате чего формируется формула “S _ _ c a u s e ”, а формулы “S A _ c a u s e ” и “S P _ c a u s e ” уничтожаются, а сгенерированные на предыдущем шаге конструкции преобразуются следующим образом:

( ( formula PSA_atom ), in_ : ( formula Scause ) ) ;

inclusion ( ( formula PSA_effect ), in_ : ( formula Scause ) ) ;

inclusion ( ( formula SPPA_effect ), in_ : ( formula Scause ) ) ;

inclusion ( ( formula qa1_PDda_intersection ), in_ : ( formula inclusion Scause ) ) ;

( ( formula SFD_def ), in_ : ( formula Scause ) ) ;

inclusion Ш а г 1 3. К атомарному высказыванию “q u e r y _ a t o m 1 ” применяется операция декомпозиции запроса на вывод атомарной формулы на запросы к семантически близким атомарным формулам.

Запрос будет выставлен к формулам “P S A _ a t o m ”, “P S A _ e f f e c t ”, “S _ _ c a u s e ”, “S P P A _ e f f e c t ”, “P D _ d e f _ a t o m ”, “P D _ a t o m ”, “S F D _ d e f ”.

decomposed, searched, confirm_, active_ gx1 ;

effect_ : gx1, expectations_ : gx2), causes_ : C2 ) ;

reasoning PD_atom ;

Goals gx searched, confirm_, active_ gx2 ;

effect_ : gx1, expectations_ : gx3), causes_ : C3 ) ;

reasoning qa1_PDda_intersection ;

Goals gx searched, confirm_, active_ gx3 ;

effect_ : gx3, expectations_ : gx4), causes_ : C4 ) ;

reasoning Scause ;

Goals gx searched, confirm_, active_ gx4 ;

effect_ : gx4, expectations_ : gx5), causes_ : C5 ) ;

reasoning PSA_atom ;

Goals gx searched, confirm_, active_ gx5 ;

effect_ : gx2, expectations_ : E6, causes_ : C6 ) ;

reasoning effect_ : gx4, expectations_ : E6, causes_ : C6 ) ;

reasoning gx6 ;

E PSA_effect ;

Goals gx searched, confirm_, active_ gx6 ;

effect_ : gx4, expectations_ : gx7), causes_ : C7 ) ;

reasoning SPPA_effect ;

Goals gx searched, confirm_, active_ gx7 ;

effect_ : gx3, expectations_ : gx8), causes_ : C8 ) ;

reasoning PD_def_atom ;

Goals gx searched, confirm_, active_ gx8 ;

effect_ : gx4, expectations_ : gx9), causes_ : C9 ) ;

reasoning SFD_def ;

Goals gx searched, confirm_, active_ gx9 ;

358 Раздел 1. 0BГрафодинамические ассоциативные машины вывода factual PD_atom, qa1_PDda_intersection, Scause, PSA_atom, PSA_effect, SPPA_effe ct, PD_def_atom, SFD_def ;

Ш а г 1 4. Остальные операции к высказыванию “q u e r y _ a t o m 1 ” не применимы, что выясняется в процессе применения к нему операции классификации и управления запросами.

Ш а г 1 5. Начиная с формулы “P S A _ c a u s e ” ко всем входящим формулам высказывания “А к с и о м а о п а р а л л е л ь н о й п р я м о й ” ставится запрос на применение и применяется операция формирования множества свободных или связываемых переменных. Формируются, в частности, конструкции:

( ( formula PSA_cause ), ( theory Планиметрия ), unassigned PSA_cause_uVars ) ;

P S A _ c a u s e _ u V a r s [ _s f, _p ] ;

( ( formula PSA_neg ), ( theory Планиметрия ), unassigned PSA_neg_uVars ) ;

P S A _ n e g _ u V a r s [ _s f, _p ] ;

( ( formula Аксиома о параллельной прямой ), PSA_uVars, unassigned ( theory Планиметрия ) ) ;

P S A _ u V a r s [ _s f, _p ] ;

Ш а г 1 6. После операции классификации и управления запросами к атомарной формуле “P S A _ a t o m ” применяется операция трассировки запроса снизу-вверх, которая находит формулу “P S A _ c a u s e ”. В результате формируется конструкция:

effect_ : gx5, expectations_ : gx10), causes_ : C10 ) ;

reasoning ( ( formulaPSA_cause ), ( theory Планиметрия ), unassigned PSA_cause_uVars ) ;

PSA_cause_uVars ;

Goals gx searched, confirm_, active_ gx10 ;

tracedUp, active_ gx5 ;

Ш а г 1 7. Затем к формуле “P S A _ c a u s e ” применяется операция трассировки запроса сверху вниз, которая находит формулу “P S A _ n e g ”. В результате формируется конструкция:

(e f f e c t _ : g x 1 0, e x p e c t a t i o n s _ : (g x 5, g x 1 1 ), c a u s e s _ : C 1 1 ) ;

reasoning ( ( formula PSA_neg ), ( theory Планиметрия ), unassigned PSA_neg_uVars ) ;

PSA_neg_uVars ;

Goals gx searched, confirm_, active_ gx11 ;

tracedDown, active_ gx10 ;

Ш а г 1 8. К формуле “P S A _ c a u s e ” применяется операция трассировки запроса снизу вверх, которая находит априори истинное импликативное высказывание “А к с и о м а о п а р а л л е л ьн о й п р я м о й ”, следствием которого является формула “P S A _ e f f e c t ”. В результате формируются конструкции:

(e f f e c t _ : g x 1 4, e x p e c t a t i o n s _ : (g x 1 2, g x 1 3 ), c a u s e s _ : C 1 2 ) ;

reasoning ( ( formula Аксиома о параллельной прямой ), PSA_uVars, unassigned ( theory Планиметрия ) ) ;

PSA_uVars ;

Goals gx searched, confirm_, active_ gx12 ;

PSA_effect ;

Goals gx deny_, active_ gx13 ;

[ refuse gx10 ] ;

Goals gx gx14 ;

confirm_ tracedUp, active_ gx10 ;

Ш а г 1 9. К формуле “А к с и о м а о п а р а л л е л ь н о й п р я м о й ” применяется операция трассировки запроса снизу-вверх. В результате формируется конструкция:

gx12 ;

confirmed_ Ш а г 2 0. К формуле “P S A _ n e g ” применяется операция трассировки запроса сверху-вниз, которая находит формулу “P S A _ n e g _ a t o m ”. В результате формируется конструкция:

(e f f e c t _ : g x 1 1, e x p e c t a t i o n s _ : (g x 1 5 ), c a u s e s _ : C 1 5 ) ;

reasoning PSA_neg_atom ;

Goals gx deny_, active_ gx15 ;

tracedDown, active_ gx11 ;

Ш а г 2 1. К атомарной формуле “P S A _ e f f e c t ” применяется операция эпизодического информационного поиска. Которая завершается безуспешно:

PSA_effect ;

factual searched, active_ gx13 ;

Ш а г 2 2. К атомарной формуле “P S A _ e f f e c t ” применяется операция трассировки запроса снизу вверх, которая находит априори истинное импликативное высказывание “А к с и о м а о п а р а л л е л ьн о й п р я м о й ”, посылкой которого является формула “P S A _ c a u s e ”. В результате формируется конструкция:

(e f f e c t _ : g x 6, e x p e c t a t i o n s _ : (g x 1 0 ), c a u s e s _ : C 1 3 ) ;

reasoning gx12 ;

C tracedUp, active_ gx6 ;

Ш а г 2 3. К формуле “P S A _ c a u s e ” применяется операция трассировки запроса сверху вниз, которая находит формулы “P S A _ a t o m ” и “P S A _ n e g ”. В результате формируется конструкция:

(e f f e c t _ : g x 1 0, e x p e c t a t i o n s _ : (g x 1 1, g x 5 ), c a u s e s _ : C 1 4 ) ;

reasoning tracedDown, active_ gx10 ;

360 Раздел 1. 0BГрафодинамические ассоциативные машины вывода Ш а г 2 4. К атомарной формуле “P S A _ a t o m ” применяется операция простого ассоциирования атомарных формул. Будет построена конструкция:

( ( formula PSA_atom ), ( theory Планиметрия ), associative (q u e r y _ a t o m 1, P S A _ e f f e c t, S _ _ c a u s e, S A _ e f f e c t _ a t o m, S A _ e f f e c t _ n e g _ a t o m, S P PA_cause, SPPA_effect, Аксиома о существовании двух т о ч е к, P D _ d e f _ a t o m, S F D _ d e f, S P _ e f f e c t _ e f f e c t )) ;

searched, confirm_, active_ gx5 ;

Ш а г 2 5. К атомарной формуле “P S A _ a t o m ” применяется операция выявления идентичных, входящих и пересекающихся атомарных формул. Результатом применения операции будет:

( ( formula PSA_atom ), in_ : ( formula Scause ) ) ;

inclusion ( ( formula qa1_PDda_intersection ), in_ : ( formula inclusion Scause ) ) ;

( ( formula query_atom1 ), in_ : ( formula inclusion qa1_PDda_intersection ) ) ;

( ( formula PSA_effect ), in_ : ( formula Scause ) ) ;

inclusion ( ( formula PSA_atom ), in_ : ( formula SP_effect_effect ) ) ;

inclusion ( ( formula SA_effect_atom ), in_ : ( formula inclusion SP_effect_effect ) ) ;

( ( formula SA_effect_neg_atom ), inclusion in_ : ( formula SP_effect_effect ) ) ;

SP_effect_effect [ точка _p ] ;

/* P S A a _ S A e a _ i n t e r s e c t i o n */ ( ( formula SPPA_cause ), in_ : ( formula SP_effect_effect ) ) ;

inclusion ( ( formula Аксиома о существовании двух точек ), inclusion in_ : ( formula SP_effect_effect ) ) ;

( in_ : ( formula Аксиома о существовании двух точек ), inclusion in_ : ( formula SPPA_cause ) ) ;

( ( formula SPPA_effect ), in_ : ( formula Scause ) ) ;

inclusion ( ( formula PD_def_atom ), inclusion in_ : ( formula qa1_PDda_intersection ) ) ;

( ( formula PD_def_atom ), in_ : ( formula PSA_atom ) ) ;

inclusion ( ( formula SFD_def ), in_ : ( formula Scause ) ) ;

inclusion Ш а г 2 6. К атомарному формуле “P S A _ a t o m ” применяется операция декомпозиции запроса на вывод атомарной формулы на запросы к семантически близким атомарным формулам. В результате будут добавлены следующие конструкции:

effect_ : gx5, expectations_ : gx4), causes_ : C15 ) ;

reasoning decomposed, searched, confirm_, active_ gx5 ;

effect_ : gx4, expectations_ : gx3), causes_ : C16 ) ;

reasoning searched, confirm_, active_ gx4 ;

effect_ : gx3, expectations_ : gx1), causes_ : C17 ) ;

reasoning searched, confirm_, active_ gx3 ;

effect_ : gx5, expectations_ : gx18), causes_ : C18 ) ;

reasoning SP_effect_effect ;

Goals gx searched, confirm_, active_ gx18 ;

effect_ : gx18, expectations_ : gx19), causes_ : C19 ) ;

reasoning SA_effect_atom ;

Goals gx searched, confirm_, active_ gx19 ;

effect_ : gx18, expectations_ : gx20), causes_ : C20 ) ;

reasoning SA_effect_neg_atom ;

Goals gx searched, confirm_, active_ gx20 ;

effect_ : gx18, expectations_ : gx21), causes_ : C21 ) ;

reasoning SPPA_cause ;

Goals gx searched, confirm_, active_ gx21 ;

effect_ : gx18, expectations_ : gx22), causes_ : C22 ) ;

reasoning «Аксиома о существовании двух точек» ;

Goals gx searched, confirm_, active_ gx22 ;

effect_ : gx22, expectations_ : gx21), causes_ : C21 ) ;

reasoning effect_ : gx21, expectations_ : gx22), causes_ : C22 ) ;

reasoning effect_ : gx5, expectations_ : gx8), causes_ : C23 ) ;

reasoning factual SP_effect_effect, SA_effect_atom, SA_effect_neg_atom, SPPA_cause, Аксиома о существовании двух точек ;

Ш а г 2 7. К атомарной формуле “P S A _ e f f e c t ” применяется операция простого ассоциирования атомарных формул. Будет построена конструкция:

( ( formula PSA_effect ), ( theory associative П л а н и м е т р и я ), (q u e r y _ a t o m 1, P S A _ a t o m, S _ _ c a u s e, S P P A _ e f f e c t, P D _ d e f _ a t o m, P D _ a t o m, S F D _ d e f )) ;

searched, deny_, active_ gx13 ;

“P S A _ e f f e c t ” Шаг 28.К атомарной формуле применяется операция выявления идентичных, входящих и пересекающихся атомарных формул. Результатом применения операции будут найденные конструкции:

( ( formula qa1_PDda_intersection ), in_ : ( formula inclusion Scause ) ) ;

( ( formula query_atom1 ), in_ : ( formula inclusion qa1_PDda_intersection ) ) ;

( ( formula PSA_effect ), in_ : ( formula Scause ) ) ;

inclusion ( ( formula PSA_atom ), in_ : ( formula Scause ) ) ;

inclusion ( ( formula PD_def_atom ), inclusion in_ : ( formula qa1_PDda_intersection ) ) ;

( ( formula PSA_effect ), in_ : ( formula PD_atom ) ) ;

inclusion ( ( formula SFD_def ), in_ : ( formula Scause ) ) ;

inclusion Ш а г 2 9. К атомарной формуле “P S A _ e f f e c t ” применяется операция декомпозиции запроса на вывод атомарной формулы на запросы к семантически близким атомарным формулам. В результате будут добавлены следующие конструкции:

362 Раздел 1. 0BГрафодинамические ассоциативные машины вывода decomposed, searched, deny_, active_ gx13 ;

effect_ : gx13, expectations_ : gx24), causes_ : C24 ) ;

reasoning Scause ;

Goals gx searched, deny_, active_ gx24 ;

effect_ : gx13, expectations_ : gx25), causes_ : C25 ) ;

reasoning PSA_effect ;

Goals gx searched, deny_, active_ gx25 ;

Scause, PSA_effect ;

factual Ш а г 3 0. Ко всем входящим формулам высказывания “А к с и о м а о п р я м о й ” ставится запрос на применение и применяется операция формирования множества свободных или связываемых переменных. Формируются, в частности, конструкции:

( ( formula SA_effect ), ( theory Планиметрия ), unassigned SA_effect_uVars ) ;

S A _ e f f e c t _ u V a r s [ _s ] ;

( ( formula Аксиома о прямой ), SA_uVars, unassigned ( theory Планиметрия ) ) ;

S A _ u V a r s [ _s ] ;

Ш а г 3 1. Применяется операция трассировки запроса снизу-вверх, которая находит априори истинное импликативное высказывание “А к с и о м а о п р я м о й ”, следствием которого является конъюнктивная формула “S A _ e f f e c t ”. В результате формируется конструкция:

effect_ : gx28, expectations_ : gx26, gx27), causes_ : C26 ) ;

reasoning ( ( formula Аксиома о прямой ), SA_uVars, unassigned ( theory Планиметрия ) ) ;

SA_uVars ;

Goals gx searched, confirm_, active_ gx27 ;

SA_effect_uVars ;

Goals gx searched, deny_, active_ gx26 ;

[ refuse gx4 ] ;

Goals gx gx28 ;

confirm_ tracedUp, active_ gx4 ;

Ш а г 3 2. К формуле “А к с и о м а о п р я м о й ” применяется операция трассировки запроса снизу вверх. В результате формируется конструкция:

gx27 ;

confirmed_ Ш а г 3 3. К формуле “S A _ e f f e c t ” применяется операция трассировки запроса сверху-вниз, которая находит формулы: “S A _ e f f e c t _ n e g _ a t o m ” и “S A _ e f f e c t _ a t o m ”. В результате формируется конструкция:

effect_ : gx26, expectations_ : gx29), causes_ : C29 ) ;

reasoning SA_effect_atom ;

Goals gx searched, deny_, active_ gx29 ;

effect_ : gx26, expectations_ : gx30), causes_ : C30 ) ;

reasoning SA_effect_neg_atom ;

Goals gx searched, deny_, active_ gx30 ;

Ш а г 3 4. Для атомарной формулы “S A _ e f f e c t _ a t o m ” выполняется операция эпизодического информационного поиска. Которая завершается безуспешно:

SA_effect_atom ;

factual “S A _ e f f e c t _ n e g _ a t o m ” Ш а г 3 5. Для атомарной формулы выполняется операция эпизодического информационного поиска. Которая завершается безуспешно:

SA_effect_neg_atom ;

factual Ш а г 3 6. Для атомарной формулы “S A _ e f f e c t _ a t o m ” выполняется операция трассировки запроса снизу-вверх, которая находит конъюнктивную формулу “S A _ e f f e c t ”. В результате формируется конструкция:

effect_ : gx19, expectations_ : gx026), causes_ : C026 ) ;

reasoning SA_effect_uVars ;

Goals gx searched, confirm_, active_ gx026 ;

Ш а г 3 7. Для атомарной формулы “S A _ e f f e c t _ n e g _ a t o m ” выполняется операция трассировки запроса снизу-вверх, которая находит конъюнктивную формулу “S A _ e f f e c t ”. В результате формируется конструкция:

effect_ : gx20, expectations_ : gx026), causes_ : C027 ) ;

reasoning Ш а г 3 8. Для атомарной формулы “S A _ e f f e c t ” выполняется операция трассировки запроса снизу-вверх, которая находит априори истинное импликативное высказывание “А к с и о м а о п р я м о й ”, посылкой которого является формула “S A _ c a u s e ”. В результате формируется конструкция:


effect_ : gx026, expectations_ : gx4), causes_ : gx27) ) ;

reasoning Ш а г 3 9. К атомарной формуле “S A _ e f f e c t _ a t o m ” применяется операция простого ассоциирования атомарных формул. Будет построена конструкция:

( ( formula PSA_effect_atom ), ( theory associative П л а н и м е т р и я ), (P S A _ a t o m, S A _ e f f e c t _ n e g _ a t o m, S P P A _ c a u s e, А к с и о м а о с у щ е с т в о в а н и и д в у х т о ч е к, P D _ d e f _ a t o m, S P _ e f f e c t _ e f f e c t )) ;

searched, deny_, active_ gx29 ;

Ш а г 4 0. К атомарной формуле “S A _ e f f e c t _ a t o m ” применяется операция выявления идентичных, входящих и пересекающихся атомарных формул. Результатом применения операции будут конструкции:

( ( formula PSA_atom ), in_ : ( formula SP_effect_effect ) ) ;

inclusion ( ( formula SA_effect_atom ), in_ : ( formula inclusion SP_effect_effect ) ) ;

364 Раздел 1. 0BГрафодинамические ассоциативные машины вывода ( ( formula SA_effect_neg_atom ), inclusion in_ : ( formula SP_effect_effect ) ) ;

( ( formula SPPA_cause ), in_ : ( formula SP_effect_effect ) ) ;

inclusion ( ( formula Аксиома о существовании двух точек ), inclusion in_ : ( formula SP_effect_effect ) ) ;

( in_ : ( formula Аксиома о существовании двух точек ), inclusion in_ : ( formula SPPA_cause ) ) ;

( ( formula PD_def_atom ), in_ : ( formula PSA_atom ) ) ;

inclusion Ш а г 4 1. К атомарному формуле “S A _ e f f e c t _ a t o m ” применяется операция декомпозиции запроса на вывод атомарной формулы на запросы к семантически близким атомарным формулам. В результате будут добавлены следующие конструкции:

decomposed, searched, deny_, active_ gx29 ;

effect_ : gx29, expectations_ : gx31), causes_ : C31 ) ;

reasoning SA_effect_atom ;

Goals gx SP_effect_effect ;

Goals gx searched, deny_, active_ gx31 ;

SP_effect_effect ;

factual Ш а г 4 2. Начиная с формулы “S P _ e f f e c t ” ко всем входящим формулам высказывания “С в о й с т в о п р я м о й ” ставится запрос на применение и применяется операция формирования множества свободных или связываемых переменных. Формируются, в частности, конструкции:

( ( formula SP_effect ), ( theory Планиметрия ), unassigned SP_effect_uVars) ;

S P _ e f f e c t _ u V a r s [ _s, _p ] ;

( ( formula Свойство прямой ), SP_uVars, unassigned ( theory Планиметрия ) ) ;

S P _ u V a r s [ _s ] ;

Ш а г 4 3. Применяется операция трассировки запроса снизу-вверх, которая находит импликативную формулу “S P _ e f f e c t ”. В результате формируется конструкция:

effect_ : gx18, expectations_ : gx32, gx33), causes_ : C32 ) ;

reasoning effect_ : gx31, expectations_ : gx34, gx33), causes_ : C34 ) ;

reasoning ( ( formula SP_effect ), SP_effect_uVars, unassigned ( theory Планиметрия ) ) ;

SP_effect_uVars ;

Goals gx searched, confirm_, active_ gx32 ;

SP_effect_uVars ;

Goals gx searched, deny_, active_ gx34 ;

SP_effect_cause ;

Goals gx confirm_, active_ gx33 ;

tracedUp, active_ gx31 ;

tracedUp, active_ gx18 ;

Ш а г 4 4. Применяется операция трассировки запроса снизу-вверх, которая находит априори истинное импликативное высказывание “С в о й с т в о п р я м о й ”, посылкой которого является атомарная формула “S P _ c a u s e ”. В результате формируется конструкция:

effect_ : gx32, expectations_ : gx35, gx4), causes_ : C35 ) ;

reasoning effect_ : gx34, expectations_ : gx36, gx4), causes_ : C36 ) ;

reasoning ( ( formula Свойство прямой ), SP_uVars, unassigned ( theory Планиметрия ) ) ;

SP_uVars ;

Goals gx searched, confirm_, active_ gx35 ;

SP_uVars ;

Goals gx searched, deny_, active_ gx36 ;

Scause ;

Goals gx tracedUp, active_ gx32 ;

tracedUp, active_ gx34 ;

Ш а г 4 5. К атомарной формуле “S _ _ c a u s e ” применяется операция простого ассоциирования атомарных формул. Будет построена конструкция:

( ( formula Scause ), ( theory associative П л а н и м е т р и я ), (q u e r y _ a t o m 1, P S A _ a t o m, P S A _ e f f e c t, S A _ c a u s e, S P P A _ e f f e c t, P D _ d e f _ a t o m, S F D _ d e f )) ;

searched, confirm_, active_ gx4 ;

“S _ _ c a u s e ” Шаг 46.К атомарной формуле применяется операция выявления идентичных, входящих и пересекающихся атомарных формул. Результатом применения операции будут конструкции:

( ( formula query_atom1 ), in_ : ( formula inclusion qa1_PDda_intersection ) ) ;

( ( formula qa1_PDda_intersection ), in_ : ( formula inclusion Scause ) ) ;

( ( formula PSA_atom ), in_ : ( formula Scause ) ) ;

inclusion ( ( formula PSA_effect ), in_ : ( formula Scause ) ) ;

inclusion ( ( formula SPPA_effect ), in_ : ( formula Scause ) ) ;

inclusion ( ( formula PD_def_atom ), in_ : ( formula PSA_atom ) ) ;

inclusion ( ( formula SFD_def ), in_ : ( formula Scause ) ) ;

inclusion Ш а г 4 7. К атомарному высказыванию “S _ _ c a u s e ” применяется операция декомпозиции запроса на вывод атомарной формулы на запросы к семантически близким атомарным формулам. В результате будут добавлены следующие конструкции:

decomposed, searched, confirm_, active_ gx4 ;

Ш а г 4 8. Ко всем формулам высказывания “А к с и о м а о п р я м о й и д в у х т о ч к а х ” ставится запрос на применение и применяется операция формирования множества свободных или связываемых переменных. Формируется, в частности, конструкция:

366 Раздел 1. 0BГрафодинамические ассоциативные машины вывода ( ( formula Аксиома о прямой и двух точках ), unassigned SPPA_uVars, ( theory Планиметрия ) ) ;

S P P A _ u V a r s [ _a, _b ] ;

Ш а г 4 9. Применяется операция трассировки запроса снизу-вверх, которая находит априори истинное импликативное высказывание “А к с и о м а о п р я м о й и д в у х т о ч к а х ”, которое включает формулу “S P P A _ c a u s e ” в качестве посылки. В результате формируется конструкция:

effect_ : gx7, expectations_ : gx37, gx21), causes_ : C37 ) ;

reasoning ( ( formula SP_effect ), SPPA_uVars, unassigned ( theory Планиметрия ) ) ;

SPPA_uVars ;

Goals gx searched, confirm_, active_ gx37 ;

SPPA_cause ;

Goals gx searched, confirm_, active_ gx21 ;

Ш а г 5 0. К атомарной формуле “S P P A _ c a u s e ” применяется операция простого ассоциирования атомарных формул. Будет построена конструкция:

( ( formula SPPA_cause ), ( theory associative П л а н и м е т р и я ), (P S A _ a t o m, S A _ e f f e c t _ a t o m, S A _ e f f e c t _ n e g _ a t o m, А к с и о м а о с у щ е с т в о в а н и и д в у х т о ч е к, P D _ d e f _ a t o m, S P _ e f f e c t _ e f f e c t )) ;

searched, confirm_, active_ gx21 ;

Ш а г 5 1. К атомарной формуле “S P P A _ c a u s e ” применяется операция выявления идентичных, входящих и пересекающихся атомарных формул. Результатом применения операции будут конструкции:

( ( formula PSA_atom ), in_ : ( formula SP_effect_effect ) ) ;

inclusion ( ( formula SPPA_cause ), in_ : ( formula SP_effect_effect ) ) ;

inclusion ( ( formula SA_effect_atom ), in_ : ( formula inclusion SP_effect_effect ) ) ;

( ( formula SA_effect_neg_atom ), inclusion in_ : ( formula SP_effect_effect ) ) ;

( ( formula Аксиома о существовании двух точек ), inclusion in_ : ( formula SP_effect_effect ) ) ;

( in_ : ( formula Аксиома о существовании двух точек ), inclusion in_ : ( formula SPPA_cause ) ) ;

( ( formula PD_def_atom ), in_ : ( formula PSA_atom ) ) ;

inclusion Ш а г 5 2. К атомарной формуле “S P P A _ c a u s e ” применяется операция декомпозиции запроса на вывод атомарной формулы на запросы к семантически близким атомарным формулам. В результате будут добавлены следующие конструкции:

decomposed, associatedSimply, searched, confirm_, active_ gx21 ;

effect_ : gx21, expectations_ : gx18), causes_ : C33 ) ;

reasoning effect_ : gx18, expectations_ : gx5), causes_ : C39 ) ;

reasoning Ш а г 5 3. Для атомарного формулы “А к с и о м а о с у щ е с т в о в а н и и д в у х т о ч е к ” выполняется операция эпизодического информационного поиска. Которая завершается безуспешно:

Аксиома о существовании двух точек ;

factual Ш а г 5 4. Применяется операция трассировки запроса снизу-вверх, которая выявляет истинность высказывания “А к с и о м а о с у щ е с т в о в а н и и д в у х т о ч е к ”.

e f f e c t _ : g x 2 2, e x p e c t a t i o n s _ : E 3 9, c a u s e s _ : g x 3 9 )) ;

reasoning query2 ;

Goals gx gx39 ;

confirmed_ [ theory query2 Планиметрия Аксиома о существовании двух точек ] ;

searched, active_ gx22 ;

Ш а г 5 5. Применяется операция формирования фиктивной интерпретации атомарной формулы, которая формирует следующую конструкцию:

( ( formula interpretation Аксиома о существовании двух т о ч е к ), i n t e r p r e t a t i o n _ : ( ( v a r _ : _a, v a l u e _ : a v ), v a r _ : _a a, v a l u e _ : a a v ), v a r _ : _b, v a l u e _ : b v ), v a r _ : _b a, v a l u e _ : b a v ) ), ( f o r m u l a f ));

f [ точка av ;

точка bv ;

] ;

aav bav gx22 ;

confirmed_ где _a a и _b a соответственно переменные дуги, включённые в высказывание и входящие в _a и в _b.

Ш а г 5 6. К формуле “S P P A _ c a u s e ” применяется операция формирования интерпретации формулы, которая формирует аналогичную конструкцию:

( ( formula SPPA_cause ), ( formula interpretation f ), i n t e r p r e t a t i o n _ : ( ( v a r _ : _a, v a l u e _ : a v ), v a r _ : _a a, v a l u e _ : a a v ), v a r _ : _b, v a l u e _ : b v ), v a r _ : _b a, v a l u e _ : b a v ) ) ;


gx21 ;

confirmed_ Ш а г 5 7. К формуле “S P P A _ u V a r s ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula SPPA_uVars ), ( formula interpretation f 2 ), i n t e r p r e t a t i o n _ : ( ( v a r _ : _a, v a l u e _ : a v ), v a r _ : _b, v a l u e _ : b v ) ) ;

f2 [ av, bv ] ;

gx37 ;

confirmed_ Ш а г 5 8. К высказыванию “S P P A _ e f f e c t ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula SPPA_effect ), ( formula interpretation f 3 ), i n t e r p r e t a t i o n _ : ( ( v a r _ : _a, v a l u e _ : a v ), v a r _ : _b, v a l u e _ : b v ), v a r _ : _b a, v a l u e _ : b a v ), v a r _ : _a a, v a l u e _ : a a v ), v a r _ : _s, v a l u e _ : s v ), v a r _ : _s, v a l u e _ :

s a v ))) ;

f3 [ прямая sv ;

sv av, bv ;

] ;

gx7 ;

confirmed_ 368 Раздел 1. 0BГрафодинамические ассоциативные машины вывода Ш а г 5 9. К высказыванию “S _ _ c a u s e ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula interpretation S _ _ c a u s e ), i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s v ), ( v a r _ : _s, v a l u e _ : s a v ) ), ( formula f4 ) ) ;

f4 [ прямая sv ;

] ;

gx4 ;

confirmed_ Ш а г 6 0. К высказыванию “S A _ u V a r s ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula interpretation S A _ u V a r s ), i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s v ) ), ( f o r m u l a f5 ) ) ;

f5 [ sv ] ;

gx027 ;

confirmed_ gx27 ;

refuse Ш а г 6 1. К высказыванию “S P _ u V a r s ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula SP_uVars ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s v ) ), ( f o r m u l a f6 ) ) ;

f6 [ sv ] ;

gx35 ;

confirmed_ Ш а г 6 2. К высказыванию “S A _ e f f e c t _ u V a r s ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula SA_effect_uVars ), ( formula interpretation f 7 ), i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s v ) ) ) ;

f7 [ sv ] ;

gx026 ;

confirmed_ gx26 ;

refuse Ш а г 6 3. К высказыванию “S A _ e f f e c t _ n e g _ a t o m ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula SA_effect_neg_atom ), ( formula interpretation f 8 ), i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s v ), v a r _ : _s n, v a l u e _ : s n v ), v a r _ : _p, v a l u e _ : p v ), v a r _ : _p a, v a l u e _ : p a v ) ) ) ;

f8 [ sv pv ;

точка pv ;

] ;

gx20 ;

confirmed_ gx30 ;

refuse “S A _ e f f e c t _ a t o m ” Шаг 64.К высказыванию применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula SA_effect_neg_atom ), ( formula interpretation f 8 ), i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s v ), v a r _ : _s a, v a l u e _ : s a v ), v a r _ : _p, v a l u e _ : b v ), v a r _ : _p a, v a l u e _ : b a v ) ) ) ;

f8 [ sv bv ;

точка bv ;

] ;

gx19 ;

confirmed_ gx29 ;

refuse Ш а г 6 5. К высказыванию “S P _ e f f e c t _ e f f e c t ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula S P _ e f f e c t _ e f f e c t ),( f o r m u l a f9 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _p, v a l u e _ : p v ), v a r _ : _p a, v a l u e _ : p a v ) ) ) ;

f9 [ точка pv ;

] ;

gx18 ;

confirmed_ Ш а г 6 6. К высказыванию “P S A _ a t o m ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula SA_effect_neg_atom ), ( formula f10 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _p, v a l u e _ : p v ), v a r _ : _p a, v a l u e _ : p a v ) ) ) ;

f10 [ точка pv ;

] ;

gx5 ;

confirmed_ Ш а г 6 7. К высказыванию “P S A _ a t o m ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula PSA_atom ), ( formula f11 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _p, v a l u e _ : p v ), v a r _ : _p a, v a l u e _ : p a v ) ) ) ;

f11 [ точка pv ;

] ;

gx5 ;

interpreted Ш а г 6 8. К высказыванию “P S A _ с a u s e ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula PSA_cause_uVars ), ( formula f12 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _p, v a l u e _ : p v ) ) ) ;

f12 [ pv ] ;

gx10 ;

interpreted Ш а г 6 9. К высказыванию “P S A _ n e g ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula PSA_neg_uVars ), ( formula f13 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _p, v a l u e _ : p v ) ) ) ;

f13 [ pv ] ;

gx11 ;

interpreted 370 Раздел 1. 0BГрафодинамические ассоциативные машины вывода “P S A _ n e g _ a t o m ” Шаг 70.К высказыванию применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula PSA_neg_atom ), ( formula f14 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _p, v a l u e _ : p v ) ) ) ;

f14 [ pv ] ;

gx15 ;

interpreted “P S A _ n e g _ a t o m ” Шаг 71.К высказыванию применяется операция расширенного ассоциирования атомарных формул. Будет построена временная конструкция:

temporary, associative ( ( formula PSA_neg_atom ), ( theory П л а н и м е т р и я ), (S A _ e f f e c t _ n e g _ a t o m, S P _ e f f e c t _ e f f e c t )) ;

searched, confirm_, active_ gx15 ;

Ш а г 7 2. К атомарному высказыванию “P S A _ n e g _ a t o m ” применяется операция выявления идентичных, входящих и пересекающихся атомарных формул. Результатом применения операции будут генерируемые конструкции:

( ( formula SA_effect_neg_atom ), inclusion in_ : ( formula PSA_neg_atom ) ) ;

( ( formula SP_effect_effect ), inclusion in_ : ( formula PSA_neg_atom ) ) ;

Ш а г 7 3. К атомарному высказыванию “P S A _ n e g _ a t o m ” применяется операция декомпозиции запроса на вывод простого высказывания на запросы к семантически близким простым высказываниям. В результате будут добавлены следующие конструкция:

e f f e c t _ : g x 1 5, e x p e c t a t i o n s _ : E 4 0, c a u s e s _ : g x 1 9 )) ;

reasoning “P S A _ n e g _ a t o m ” Шаг 74.К высказыванию применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula PSA_neg_atom ), ( formula f15 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s v ), v a r _ : _s n, v a l u e _ : s n v ), v a r _ : _p, v a l u e _ : p v ) ) ) ;

f15 [ sv pv ;

] ;

gx15 ;

denied_ Ш а г 7 5. К высказыванию “P S A _ n e g ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula PSA_neg_uVars ), ( formula f13 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s v ), v a r _ : _p, v a l u e _ : p v ) ) ) ;

f13 [ pv, sv ] ;

gx11 ;

confirmed_ Ш а г 7 6. К высказыванию “P S A _ с a u s e ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula PSA_cause_uVars ), ( formula f12 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s v ), v a r _ : _p, v a l u e _ : p v ) ) ) ;

f12 [ pv, sv ] ;

gx10 ;

interpreted Ш а г 7 7. К высказыванию “P S A _ a t o m ” применяется операция формирования интерпретации формулы, которая на основании формул “S _ _ c a u s e ” и “P S A _ с a u s e ” формирует конструкцию:

( ( formula PSA_cause_uVars ), ( formula f11 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s a v ), v a r _ : _s, v a l u e _ : s v ), v a r _ : _p a, v a l u e _ : p a v ), v a r _ : _p, v a l u e _ : p v ) ) ) ;

f11 [ прямая sv ;

точка pv ;

] ;

gx5 ;

confirmed_ Ш а г 7 8. К высказыванию “P S A _ с a u s e ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula PSA_cause_uVars ), ( formula f12 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s v ), v a r _ : _p, v a l u e _ : p v ) ) ) ;

f12 [ pv, sv ] ;

gx10 ;

confirmed_ Ш а г 7 9. К высказыванию “А к с и о м а о п а р а л л е л ь н о й п р я м о й ” применяется операция формирования интерпретации формулы, которая формирует конструкцию:

( ( formula PSA_uVars ), ( formula f16 ), interpretation i n t e r p r e t a t i o n _ : ( ( v a r _ : _s, v a l u e _ : s v ), v a r _ : _p, v a l u e _ : p v ) ) ) ;

f16 [ pv, sv ] ;

gx12 ;

confirmed_ Ш а г 8 0. К высказыванию “P S A _ e f f e c t ” применяется операция формирования интерпретации формулы, которая формирует соответствующую конструкцию.

Ш а г 8 1. К высказыванию “P D _ a t o m ” применяется операция формирования интерпретации формулы, которая формирует соответствующую конструкцию.

Ш а г 8 2. К высказыванию “q a 1 _ P D d a _ i n t e r s e c t i o n ” применяется операция формирования интерпретации формулы, которая формирует соответствующую конструкцию.

Ш а г 8 3. К высказыванию “q u e r y _ a t o m 1 ” применяется операция формирования интерпретации формулы, которая на основании формул “S _ _ c a u s e ” и “P S A _ с a u s e ” формирует соответствующую конструкцию.

Ш а г 8 4. К высказыванию “q u e r y _ a t o m 1 ” применяется операция вычисления значения высказывания. Высказывание приобретает истинностное значение истина:

query_atom1 ;

Планиметрия 372 Раздел 1. 0BГрафодинамические ассоциативные машины вывода Ш а г 8 5. Ко всем высказываниям входящим во множество “t e m p o r a r y ” применяется операция уничтожения промежуточных конструкций, которая удаляет интерпретации и различные служебные конструкции используемые исключительно для вывода.

Конец решения задачи Приведём фрагмент результирующего состояния памяти графодинамической ассоциативной машины вывода, являющийся положительным ответом на поставленный нами запрос.

existAtExpr Планиметрия query_at om прямая параллельность интерпретация sv интерпретация_ В процессе решения будет сформирована конструкция, поясняющая результат решения.

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

Такие системы баз знаний являются неотъемлимой частью любой интеллектуальной системы. Это справедливо для интеллектуальных обучающих систем, систем построения виртуальных организаций и любых прикладных экспертных систем. Система операций машины логического вывода открыта для дополнения, и в случае реализации новых механизмов вывода, такие механизмы легко могут быть интегрированы (особенно в случае использования языка SCP в качестве языка микропрограммирования) с описанной выше графодинамической ассоциативной машиной вывода.

Представление и обработка знаний в графодинамических ассоциативных машинах Заключение Завершая данную книгу, сделаем ряд замечаний.

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

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

• фактографический язык SCB (Semantic Code Basic), описанный в разделах 2 и 3;

• язык SC (Semantic Code), являющийся основой для построения различных логических языков и языков представления знаний, описанный в разделе 4;

• язык SCL (Semantic Code Logic), являющийся одним из возможных (но не единственно возможным) логических языков, построенных на основе языка SC, описанный в разделах 5 и 6;

• язык описания целей (заданий) в графодинамических ассоциативных машинах, описанный в разде ле 6;

• навигационно-поисковая графодинамическая ассоциативная машина, описанная в разделе 7;

• графодинамические ассоциативные машины вывода, описанные в разделе 8.

2. Аспекты реализации графодинамических ассоциативных машин обработки знаний рассмотрены в книге [411] (П р о г р В А М - 2 0 0 1 к н ), которая является естественным продолжением данной книги.

В основе реализации графодинамических ассоциативных машин обработки знаний лежит язык про граммирования SCP (Semantic Code Programming), специально ориентированный на обработку инфор мации в графодинамической (структурно перестраиваемой) ассоциативной памяти.

3. Применение графодинамических моделей обработки знаний в области автоматизации обучения рассмотрено в книге [236] (И н т е л О С и В У О - 2 0 0 1 к н ). В ней рассмотрены вопросы проектирования интеллектуальных обучающих систем и интеллектуальных виртуальных учебных организаций.

Литература Абдрахманов Б.К.1990ст-ИсслеВРА 1.

Абдрахманов Б.К. Исследование возможностей распараллеливания алгоритмов функционирования экс пертных систем и реализация их на однородной вычислительной среде //Методы и средства параллель ной обработки данных в системах связи. - М.: Моск. ин-т связи, 1990. - с. 60-74.

Авербух А.Б..1990ст-оПринцПВЯ 2.

Авербух А.Б., Коваль В.Н., Рабинович З.Л. О принципах построения внутреннего языка ЭВМ, ориентиро ванной на решение широкого класса задач искусственного интеллекта // II Всесоюзная конференция "Ис кусственный интеллект-90". - Минск, 1990. - Т. 2. - с. 121-124.

Агафонов В.Н..1988ст-ЛогичП 3.

Агафонов В.Н., Борщев В.Б., Воронков А.А. Логическое программирование в широком смысле (обзор) // Логическое программирование. - М.: Мир, 1988. - с. 298-366.

Агафонов В.Н.1982ст- ТипыИАД 4.

Агафонов В.Н. Типы и абстракция данных в языках программирования (обзор) // Данные в языках про граммирования. Абстракция и типология. - М.: Мир, 1982. - с. 265-327.

Агафонов В.Н.1990кн-СпециП 5.

Агафонов В.Н. Спецификация программ: понятийные средства и их организация. 2-е издание. - Новоси бирск: Наука, 1990.

Агафонов В.Н.ред.1982сб-АбстрИТ 6.

Данные в языках программирования. Абстракция и типология: Сб. статей / Пер. с англ. под ред. Агафоно ва В.Н. - М.: Мир, 1982.

Агафонов В.Н.ред.1988сб-ЛогичП 7.

Логическое программирование: Сб. статей / Пер. с англ. и франц.;

Под ред. Агафонова В.Н. - М.: Мир, 1988.

Агеев В.Н.1984ст- ПримеГиГС 8.

Агеев В.Н. Примеры гипертекстовых и гипермедиа систем (обзор)// Компьютерные технологии в высшем образовании: Сб. статей. М.: Изд-во МГУ,1994.-с.225-229.

Айелло Л..1986ст-ПредсИИМ 9.

Айелло Л., Чекки К., Сартини В. Представление и использование метазнаний // ТИИЭР. - 1986. - Т. 74. – N 10. - с. 12-32.

10. А й з е р м а н М. А.. 1 9 8 8 с т - Д и н а м П к А С Айзерман М.А., Гусев Л.А., Петров С.В., Смирнова И.М., Тененбаум Л.А. Динамический подход к анализу структур, описываемых графами (основы графодинамики) // Исследования по теории структур. - М.: Наука, 1988. - с. 5-76.

11. А й з е р м а н М. А.. 1 9 7 7 с т - Д и н а м П к А С Динамический подход к анализу структур, описываемых графами / Айзерман М.А., Гусев Л.А., Петров С.В., Смирнова И.М. // Автоматика и телемеханика. - 1977. - N 7. - с.136-151;

- N 8. - с. 123-136.

12. А й л и ф Д ж. 1 9 7 3 к н - П р и н ц П Б М Айлиф Дж. Принципы построения базовой машины / Пер. с англ. - М.: Мир, 1973.

13. А к о ф ф Р.. 1 9 7 4 к н - о Ц е л е у С Акофф Р., Эмери Ф. О целеустремленных системах. Пер. с англ. - М.: Сов.радио, 1974.

14. А л е к с а н д р о в В. В. 1 9 9 2 с т - В о с п р В И Александров В.В. Восприятие визуальной информации в системах искусственного интеллекта // Новости искусственного интеллекта. - 1992. - N 1. - с.25-45.

15. А л е ш и н а Н. А.. 1 9 9 0 к н - Л о г и к И К Логика и компьютер. Моделирование рассуждений и проверка правильности программ / Н.А. Алешина, А.М. Анисов, П.И. Быстров и др.- - М.: Наука, 1990.

16. А м а м и я М.. 1 9 9 3 к н - А р х и т Э В М Амамия М., Танака Ю. Архитектура ЭВМ и искусственный интеллект: Пер. с япон.- М.: Мир, 1993.

Литература 17. А м о с о в Н. М.. 1 9 7 5 с т - А к т и в С С Амосов Н.М., Касаткин А.М., Касаткина Л.М. Активные семантические сети в роботах с автономным управлением // Труды IV Международной объединенной конференции по искусственному интеллекту: Т.9.

- М., 1975.

18. А н а с т а з и А. 1 9 8 2 к н - П с и х о Т Анастази А. Психологическое тестирование. Т.1.М., 1982.

19. А р б и б М. 1 9 6 8 к н - М о з г М и М Арбиб М. Мозг, машина и математика. - М.: Наука, 1968.

20. А р б и б М. А. 1 9 7 6 к н - М е т а ф М Арбиб М.А. Метафорический мозг / Пер. с англ. - М.: Мир, 1976.

21. А р л а з а р о в В. Л.. 1 9 9 8 с т - Т е о р и И М С И К С АрлазаровВ.Л., Журавлев Ю.И., Ларичев О.И., Лохин В.М., Макаров И.М., Рахманкулов В.З., Финн В.К.

Теория и методы создания интеллектуальных компьютерных систем// Информационные технологии и вычислительные системы.- М, №1, 1998. - с.3-13.

22. А с е л ь д е р о в З. М. 1 9 8 7 п р - П р е д с Г Асельдеров З.М. Представление графов и операции над ними. - Киев, 1987. (Препринт / АН УССР. Ин-т кибернетики им. В.М.Глушкова;

N 87-49).

23. А с р а т я н Р. Э.. 1 9 7 9 с т - А п п а р Р С А Асратян Р.Э., Волков А.Ф., Лысиков В.Т. Аппаратная реализация синтаксического анализатора с помощью ассоциативной памяти // Автоматика и телемеханика. - 1979. - N 4.

24. А х о А.. 1 9 7 9 к н - П о с т р И А В А Ахо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. - М.: Мир, 1979.

25. А ч а с о в а С. М.. 1 9 9 0 к н - К о р р е П В П Ачасова С.М., Бандман О.Л. Корректность параллельных вычислительных процессов. - Новосибирск:

Наука. Сиб. отд-ние, 1990.

26. Б а б а е в И. О.. 1 9 8 1 с т - Я з ы к Д е к а р т Бабаев И.О., Новиков Ф.А., Петрушина Т.И. Язык Декарт - входной язык системы СПОРА // Прикладная информатика. М.: Финансы и статистика, 1981. - Вып.1. - с. 35-73.

27. Б а б а я н Б. А.. 1 9 8 6 с т - У р о в е П Бабаян Б.А. Уровень программирования и архитектурные принципы построения ЭВМ // Кибернетика и вы числительная техника. М.: Наука, 1986. - Вып. 2. - с. 18-27.

28. Б а з и с Р Е Ф А Л - 1 9 7 7 у ч Базисный РЕФАЛ и его реализация на вычислительных машинах. Методическое пособие М.: ЦИИПИАС, 1977.

29. Б а й к о в А. М.. 1 9 8 0 с т - У п р а в К Ц А И Управляемый контекстом целенаправленный анализ изображений на основе использования семантиче ской сети / Байков А.М., Кузин Е.С., Хахалин Г.К., Шамич А.П. // Вопросы радиоэлектроники. Сер. ЭВТ. 1980. - Вып. 1. - с. 50-58.



Pages:     | 1 |   ...   | 10 | 11 || 13 | 14 |
 





 
© 2013 www.libed.ru - «Бесплатная библиотека научно-практических конференций»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.