ГОСТ Р 56271-2014
Приложение К
(обязательное)
Свойства расширения шаблона
К.1 Логическое считывание определений шаблонов
Если определения шаблона на множестве рассматриваются как аксиомы эквивалентности, то сама формула
и ее расширение эквивалентны по отношению к указанным аксиомам.
Лемма 2 Пусть Se 7S(I0) — это множество шаблонов, а
0
и о’— это формулы типа
a
-
v
-З
над символами
из множества l^unames(S). Если
0
’— это расширение р. то S |= ф—* й>!
Доказательство леммы 2. Так как каждый шаг расширения шаблона заменяет одну подформулу другой,
эквивалентной ей в соответствии с рассматриваемыми аксиомами, то результирующая формула будет также экви
валентна исходной. Что и требовалось доказать.
П р и м е р — Аксиомы, соответствующие множеству шаблонов, рассмотренному выше:
Vx. (А(х) *-* Эу.(В{у)лЩх,у)))
Уу.(8(х)<-»С(х)лО(х))
В соответствии с леммой 2. указанные две аксиомы подразумевают эквивалентность
А(а)лВМ
o3y.((C(y)vD(y))AR(a.y))A(C(b)vD(b)}
исходной формулы и ее расширения в нашем примере.
К.2 Разрешимость соответствия ИСО 15926-2
Для практических приложений определений шаблонов представляет интерес нижеследующая проблема.
Пусть заданы:
- аксиоматизация по ИСО 15926-2 (формула Ф);
- множество шаблонов S;
- формула р типа
a
-
v
-З
без свободных переменных.
Необходимо проверить непротиворечивость выражения Ф л Л ;с14л0-
При м е ча н и е
- 0
может быть громоздкой формулой, ссылающейся на большое количество опреде
ленных шаблонов. Необходимо удостовериться в том. что
0
вместе с определениями шаблонов, не противоречат
базововой аксиоматике ИСО 15926-2.
П р и м е р — Аксиоматика ИСО 15926-2 включает аксиомы:
Activily(x) -» Possiblelndividual(x)
Relationship(x) -» AbstractObject(x)
-(Possiblelndividual(x)
a
AbstractObject(x)).
Из определений шаблонов:
AB(x) -* A(x)
a
S(x)
A(x) —•Activily(x)
B(x) -» Relationship(x)
и рассматриваемой формулы
О=АВ(а)
следует, что а — это и Possiblelndividual, иAbstractObject, что противоречит ИСО 15926-2. Данной при
мер это показывает. Для более громоздкой формулы р. большего набора шаблонов и. особенно, для
большего потребного число аксиом ИСО 15926-2 постановка указанной проблемы затрудняется. Целе
сообразно иметь возможность ставить такую проблему автоматически.
Нижеследующая лемма утверждает, что для решения указанной проблемы сначала нужно расширить все
шаблоны.
Лемма 3 Пусть р — это расширение о по отношению к множеству шаблонов S. Тогда фор\гула
Ф л А с £л
0
непротиворечива только в том случае, если непротиворечива формула Флр.
90