ГОСТ Р 56271-2014
Приложение G
(справочное)
Проверка соответствия с помощью когерентной логики
Проверка показывает, что язык формализации ИСО 15926-2 и настоящего стандарта попадает внутрь фраг
мента логики первого порядка (FOL), известного как когерентная логика (CL), составленная из формул вида.
V x (4
л
-.-
л
Д, -* 3 y ,.C ,v v 3 y „.C m)
гдеА, — это элементы (атомы), a Cj— их сопряжения. При записи формул когерентной логики (CL) универсальные
кванторы обычно опускают. При этом свободные переменные неявно универсально квантифицируются. В примере
из приложения В:
- универсальная аксиома Vx(Thing(x)) — это формула когерентной логики (CL)
— Thing(x):
- аксиомы нелвресвчения могут быть записаны в кодах с помощью операции х. например.
-^(IntegerNumber(x)
a
(MultidimensionalNumber(x)))
записывается в виде:
lntegerNumber(x) л MultidimensionalNumber(x) -*1.
- все другие аксиомы уже имеют форму CL.
Отметим, что логика CL включает оба квантора V и 3. Но их возможное чередование ограничено: единствен
ная допустимая смена кванторов производится благодаря квантору существования во втором элементе, который
может появляться внутри области применения универсальных кванторов, вмещающих всю формулу:
hasClassOfClassOfWhole(x.y)->(ClassOfClassOfComposition(x)vCtossOfNamespace(x)).
Рассматриваемая здесь проблема — это проблема соответствия множеств Т и X: для заданного множе
ства Т формул когерентной логики (CL) (когерентная теория) и множества формул I типа
a
-
v
-З необходим
идентифицировать такие условия для Т и Z, что проверка множества ТЫ на соответствие логике первого
порядка (FOL) будет разрешима. Ключевое наблюдение: достаточно проверить множество ГЫ
7
на соответствие
когерентной логике (CL).
Важное место CL: когерентные формулы можно использовать как генерирующие правила, формирующие
полную процедуру доказательства для лотки CL. В настоящем примечании мы используем ту же идею для ре
шения проблемы соответствия множеств Г. X. Реализации процедуры способствуют знание констант и знание ос
новных элементарных формул (число которых всегда конечно). Мы изначально предполагаем, что множество X
содержит, по крайней мере, один символ константы. Если же существует индивидуальный объект, о котором мы
ничего не знаем, то используется представление Thing(a).
Технически мы представляем последовательность приложений, которое является строкой приложений пра
вил. Для каждой последовательности приложений s. fml(s) — это множество формул и dom(s) — это множество
констант. Множество последовательностей приложений из I индуктивно определяется следующим образом:
- пустая строка е— это последовательность приложений; fml(c) = I и dom(r) — это множество символов
констант из fml(c).
- Если s — это последовательность приложений, s.rозначает, что реализация г— одна из нижеследующих:
- замкнутая реализация А^
л
...
а
А
п
— С для формулы из Г такая, что каждое A/sfml(s). Тогда fml(s.r) =
fm!(sMC} и dom(s.r) = dom(s):
- <4,vA
2
-* Ar где A,vA ^ fml(s), и ни один из членов s не относится кA,vA
2
—»Аа.г Тогда fml(s.r) = fmKs)_»{A}
и dom(s.r) =dom(s);
- А,
а
А
2
—Аг где каждое A^fml(s). Тогда fml(s.r) =fml(sMA) и dom(s.r) =dom(s):
- ЗхА(х) -♦ A(0 для 3xA(x)e fml(s) такое, что ни одна из формул формы A(f) не относится к fml(s). В данном
случае f — это новый символ константы, fml(s.r) = fml(s)i~>(A(<)}и dom(s.r) = dom(s)o{/};
- А(э) -♦ А(Ь) для А(а), и либо а =Ь. либо
6
= а из fml(s). Тогда fml(s.r) = fml(s)u{A(b)} и dom(s.r) = dom(s).
Необходимо пояснить невозможность использования сопряжения «или» в следующем случае. Из последо
вательности приложений для сущности {Possiblelndividual(a)vAbstractObject(a)> следует, что либо а — это воз
можный индивидуальный объект, либо а — абстрактный объект, но не то и другое вместе.
Необходимо пояснить возможность отсутствия 3. когда в логике CL можно избежать сколемизации. Если,
например, выведено R(a. б), то 3х/?(а. х) дальше не может быть расширено (свидетель уже есть). Это основной
источник улучшения полной логики первого порядка FOL (также используемый в механизмах доказательства опи
сательной лотки DL).
7
Отметим, что указанное покрывает проблему проверки соответствия из раздела К.2. выполнить проверку
соответствия Ф л<5где Ф —формула, представляющая аксиоматизацию ИСО 15926-2, S— множество шаблонов и
^— это нормальная формула. R(S) для
9
— замкнутая формула типа
a
-
v
-З, подлежащая проверке насоответствие.
85