ГОСТ Р ИСО 18629-13-2011
8.4.1 Примитивный символ отношения ubiquitous
KIF-формат обозначения примитивного символа отношения ubiquitous
таков:
(ubiquitous ??а1 ?а2)
Неформальнаясемантика дляпримитивногосимволаотношения
ubiquitous такова:
(ubiquitous ?а1 ?а2) в интерпретации теории автоморфизма дерева
элементов принимает значение TRUE тогда и только тогда, когда элементы
операции, которые сохраняются с помощью автоморфизма дерева элементов
для операции ?а1, являются элементами субоперации ?а2.
8.4.2 Определяющий символ отношения end_iso
KIF-формат обозначения определяющего символа отношения endjso
таков:
(endjso ?s1 ?s2 ?s3 ?s4)
Неформальная семантика для определяющего символа отношения
end ИСО такова:
(end iso ?s1 ?s2 ?s3 ?s4) в интерпретации теории автоморфизма дерева
элементов принимает значение TRUE тогда и только тогда, когда существует
один и тот же автоморфизм дерева элементов, который отображает элемент
?s1 в ?s2, а также элемент ?s3 в ?s4.
8.4.3 Определяющий символ отношения legal_map
KIF-формат обозначения определяющего символа отношения legal map
таков:
(legal map ?s3 ?s4 ?a)
Неформальная семантика для определяющего символа отношения
legal_map такова:
(legal map ?s3 ?s4 ?а) в интерпретации теории автоморфизма дерева
элементов принимает значение TRUE тогда и только тогда, когда существует
автоморфизм дерева элементов, который отображает элемент ?s3 в ?s4,
сохраняя допустимые элементы для операции ?а.
£.4