ГОСТ Р 56271-2014
Доказательство. Для любой модели, удовлетворяющей формуле Ф л A -CJс,л<?из леммы 2 следует, что
она также удовлетворяет о. и. таких» образом, справедливо Флф. С другой стороны, предположим, что существует
модель Мдля Флф Ни Ф. ни фназваний шаблонов не содержат. Поэтому Мможет быть расширена по индукции над
конструкцией Sдо новой модели М’. интерпретирующей базовые символы типа Ми все названия шаблонов N. так
что аксиомы шаблона... удовлетворяются в М’. Это означает, что W удовлетворяет Ф л А-.С5Исполь
зуя лемму 2 повторно, получаем, что М’также удовлетворяет о. Что и требовалось доказать.
Необходимо проверить непротиворечивость формул о тилал-^-З, содержащей только базовые символы, в
контексте аксиоматики Ф по ИСО 15926-2. Для ответа на данный вопрос может быть использована стандартная
технология описательной логики. Также предпочтительным может оказаться метод гипертаблиц. описанный в при
ложении G.
К.2.1 Трансляция языка ИСО 15926-2 в описательную логику
Аксиоматику ИСО 15926-2 можно транслировать в ТВох врамках ALCIQ (описательной логики с обратными
ролями и квантифицированными числовыми ограничениями). Это есть подмножество хорошо изученной и исполь
зуемой на практике описательной логики SHIQ. Для оценки имеющихся возможностей нужно проанализировать
различные аксиомы, используемые в формализациях ИСО 15926-2 первого порядка в соответствии с 4.1:
- одноместные предикаты А(х) для сущностей EXPRESS отображаются на элементарные понятия описа
тельной логики;
- двухместные предикаты hasR(x) атрибутов языка EXPRESS отображаются на роли hasR описательной
логики (DL);
- типы данных списков EXPRESS в аксиомах фактически не используются;
- практическая реализация А(х) •-* В(х). представляющая отношение подтипов языка EXPRESS, отобража
ется на аксиомуАС в описательной логики DL;
- аксиома А(х)(B(x)vC(x)vD(x)) декларации ABSRACT языка EXPRESS отображается на аксиому
* В U С U D в DL:
- аксиома
-.(A(
x
)
a
(B(
x
)
v
C(
x
)))
декларации ONEOF языка EXPRESS отображается на аксиомуA C-^SUC);
- аксиома hasR(x, у) -» (А(х)/В(х)). представляющая область атрибута языка EXPRESS, отображается на
аксиому Т с VftasR’.(A U S);
- аксиома A(x),- hasR(x, у) -* F(y) локального ограничения диапазона языка EXPRESS отображается на ак
сиому А С VhasR .F;
- аксиома A(x)AhasR(x.y)AhasR(x. z) — у = z, необходимая для ограничения кардинального числа [0.1] в
языке EXPRESS, отображается на аксиомуА с VhasR max 1Т в описательной логике (DL);
- аксиома А(х) —3y(hasR{x. у)), дополнительно необходимаядля задания ограничения кардинального числа
[1.1] в языке EXPRESS, отображается на аксиому А С BhasR.T в описательной логике (DL);
- аксиома A(x)*A(y)AhasR(x, z).-hasR{y. z) — х = у для правила UNIOUE языка EXPRESS отображается на
аксиому Т с hasR max 1А в описательной логике DL.
Это аксиомы ТВох описательной логихи для ИСО 15926-2.
К.2.2 Проверка достоверности расширения шаблона
®r
Для проверки достоверности формула о типа
a
-
v
-З сколемизируется. При этом каждая экзистенциаль
но связанная переменная заменяется на новый постоянный символ, порождающий й В этом случае, формула
Флфнепротиворечива, если и только если непротиворечива формула ФлфЭто снова можно проверить путем пре
образования о вдизъюнктивную нормальную форму:
-»p,v-v<n
где ф,— это сопряжения основных элементов над 1$. Указанные сопряжения можно интерпретировать как сущно
сти АВох над предварительно определенной трансляцией ТВох для ИСО 15926-2. Формула Флфнелротиворечива
только в том случае, если одна из указанных сущностей АВох непротиворечива по отношению к ТВох. Данная
проблема известна как «проблема непротиворечивости АВох». Ее можно решать с помощью ультрасовременных
систем доказательств описательной логики (DL).
П р и м е р — Пример расширения и проверки достоверности см. в приложении F.
91