ГОСТ Р 59798—2021
мянутым выше; и, во-вторых, путем изменения последовательных слоев дочерних терминов, чтобы гарантировать
наличие цепочек отношений типа is-a.
В.2.5 Подтверждение соответствия BFO
В.2.5.1 Подтверждение соответствия онтологий, сформулированных на английском языке и исполь
зующих синтаксис OWL или CL
Для подтверждения соответствия BFO онтологии, полученной с помощью вышеупомянутых механизмов, не
обходимо продемонстрировать, что (а) онтология непротиворечива, и (b) BFO логически интерпретируема в ней
согласно определению, содержащемуся в настоящем стандарте. Для онтологий OWL выполнение условий (а) и (Ь)
демонстрируется при помощи стандартных средств обоснования. Для онтологий CL выполнение условий (а) и (Ь)
демонстрируется с помощью методов, описанных в разделах А.5 и А.6 соответственно.
В.2.5.2 Установление соответствия онтологий, сформулированных на другом языке или с примене
нием другого синтаксиса
Онтология может быть сформулирована на языке или с применением синтаксиса, отличных от используемых
в настоящем стандарте. Чтобы определить ее соответствие BFO, необходимо продемонстрировать, что:
- в онтологии предусмотрено сопоставление терминов и выражений отношения, представленных на этом
языке, с терминами и выражениями отношения на одном из языков, используемых в настоящем стандарте (OWL 2,
CL);
- охват такого сопоставления включает термины и выражения отношения в соответствующем представлении
BFO; набор терминов, сопоставляемых таким образом, представляет собой BFO-субсигнатуру онтологии;
- следствия аксиом этой онтологии, которые используют только термины и выражения отношения из этой
субсигнатуры, сопоставляются с подмножеством следствий BFO.
В.З Принципы демонстрации непротиворечивости аксиоматизации CL для BFO 2020
В.3.1 Обзор
Первый шаг для доказательства непротиворечивости аксиоматизации CL (в соответствии с ГОСТ Р
ИСО/МЭК 21838-1, п. 4.4.4) заключается в создании сокращенного набора аксиом CL, образованного путем уда
ления определенно эквивалентных аксиом: (i) для отношений R с инверсиями R’, сохраняются только аксиомы,
относящиеся к R; (ii) для бинарных отношений BR, перечисленных в Приложении А (п. А.2.3) и определенных
в терминах тернарных отношений CL — TR, сохраняются только аксиомы, относящиеся к TR. Во-вторых, использу
ются стандартные семантические методы для построения модели сокращенной теории, представленной по следу
ющей ссылке:
https://standards.iso.org/iso-iec/21838/-2/ed-1/en
(временная ссылка):
https://buffalo.app.box.com/v/bfo-
iso-owl-cl.
Расширение приложения Clausetester в пакете LADR Library для пакета Automated Deduction Research
Prover9 используется для демонстрации того, что все аксиомы редуцированной теории в этой модели верны. Таким
образом доказывается непротиворечивость, поскольку любая модель, в которой верна сокращенная теория, верна и
в расширенной теории.
В.3.2 Документация
Каталог моделей содержит модели в трех различных форматах:
- семантика CL: model.cl;
- средство автоматического доказательства теорем Prover9: model.р9;
- интерпретация формата тасе4: mace4-interpretation.txt.
В.3.3 Структура модели
Модель — это некая предметная область индивидов вместе с символами сопоставления интерпретаций
(термины и выражения отношений) с индивидами и отношениями между индивидами. Теория, основанная на акси
омах BFO 2020-CL, допускает конечные модели, а модель, использованная в доказательстве, включает 2 377 от
ношений в предметной области с 92 индивидами. Модель представлена как структура, состоящая из конечного
набора отношений, каждое из которых имеет символ отношения из теории BFO 2020-CL и последовательность
индивидов.
Индивиды в модели — это имена (произвольные строки). Отношения в модели — это те из них, которые ис
тинны, когда их символ и аргументы (имена) отношения образуют одно из отношений в структуре, и ложны в про
тивном случае. Каждая формула проверяется на соответствие каждому возможному назначению количественных
переменных отдельным индивидам в предметной области. Если модель удовлетворяет всем формулам, теория
непротиворечива.
В.4 Принципы обеспечения интерпретируемости аксиоматизации OWL 2 BFO 2020 в аксиоматизации
CL (в соответствии с ГОСТ Р ИСО/МЭК 21838-1, 4.4.5)
Интерпретируемость аксиоматизации OWL 2 в А.2 приложения А в аксиоматизации CL в А.З приложении А
была установлена путем включения CL-аналога аксиоматизации OWL-аксиоматизации в аксиоматизацию CL сле
дующим образом:
- аксиомы OWL 2 переведены в синтаксис CL;
23