ГОСТ Р ИСО 18629-13-2011
6.4.3 Примитивная функция отношения soomap
KIF-формат обозначения примитивной функции отношения soomap
таков:
(soomap ?s).
Неформальная семантика для примитивной функции отношения soomap
такова:
(= ?s1 (soomap ?s)) в интерпретации теории упорядочения элементов
субопераций принимает значение TRUE тогда и только тогда, когда элемент
операции ?s1 является элементом субоперации, упорядоченным так, чтобы он
соответствовал элементу ?s.
6.5 Определения теории упорядочения элементов субопераций
6.5.1 Определение 1 (связанное с символом отношения root_soo)
Элемент операции является корневым узлом упорядоченной структуры
элементов субоперации для операции ?а тогда и только тогда, когда он
является элементом упорядочения и отсутствует элемент операции, который
предшествует ему при упорядочении.
(forall (?s ?а) (iff (root_soo ?s ?a)
(and (soo ?s ?a)
(not (exists (?S1)
(soo_precedes ?s1 ?s ?a)))))
6.5.2 Определение 2 (связанное с символом отношения leaf_soo)
Элемент операции является конечным узлом упорядоченной структуры
элементов субоперации для операции ?а тогда и только тогда, когда он
является элементом упорядочения и отсутствует элемент операции, который
следует за ним при упорядочении.
(forall (?s ?а) (iff (leaf_soo ?s ?a)
(and (soo ?s?a)
(not (exists (?S1)
(soo„precedes ?s ?s1 ?a)))))
6.5.3 Определение 3 (связанное с символом отношения next soo)
Элемент операции ?s2 является следующим элементом субоперации
после элемента ?s1 в упорядочении элементов субопераций для операции ?а
12