ГОСТ Р ИСО 18629-13-2011
8.4.4 Определяющий символ отношения tree_map
KIF-формат обозначения определяющего символа отношения tree map
таков:
(tree map ?s1 ?s2 ?a1 ?a2)
Неформальная семантика для определяющего символа отношения
tree map такова:
(end iso ?s1 ?s2 ?а1 ?a2) в интерпретации теории автоморфизма дерева
элементов принимает значение TRUE тогда и только тогда, когда любое
отображение на допустимое дерево элементов, которое сохраняет допустимые
элементы ?а1 и отображает элемент ?s1 в ?s2, сохраняя дерево операций для
?а2.
8.5 Определения теории автоморфизма дерева элементов
Определения, введенные теорией автоморфизма дерева элементов,
таковы:
8.5.1 Определение 1
Один и тот же автоморфизм, который отображает элемент ?s1 в ?s2, а
также отображает элемент ?s3 в ?s4.
(forall (?sl ?s2 ?s3?s4) (iff (endjso ?s1 ?s2 ?s3 ?s4)
(exists (?s5 ?s6)
(and (precedes ?s5 ?s1)
(precedes ?s5 ?s3)
(precedes ?s6 ?s2)
(precedes ?s6 ?s4)
(tree_equiv ?s1 ?s2)
(tree_equiv ?s3 ?s4)
(tree_equiv ?s5 ?s6))))
8.5.2 Определение 2
Автоморфизм дерева элементов, который отображает элемент ?s3 в ?s4
и сохраняет допустимые элементы операции ?а.
(forall (?s ?s3 ?s4) (iff (legal_map ?s3 ?s4 ?a)
(and (occurrence_of ?s3 ?a)
(occurrence_of ?s4 ?a)
(tree_equiv ?s3 ?s4)
(forall (?s1)
(implies (occurrence_of ?sl ?a)
(exists (?s2)
25