ГОСТ Р 56271-2014
Легко заметить, что соответствие I по отношению к Тразрешимо, если для любого последовательности при
ложений
S
изI.
U dom(f)
ш
конечно, где t s s означает, что t — это начальная последовательность s.
Это типовой случай, когда можно ограничить число новых членов, появляющихся вследствие отказа от 3.
Единственные аксиомы формализации по ИСО 15926-2. дающие формулы с кванторами существования. — это
аксиомы ролей, например:
ClassOfClassOfComposition(x)
a
hasClassOfClassOfWhole(x.y) -» ClassOfClassOflndividualiy)
ClassOfClassOfComposition(x) -> hasClassOfClassOfWhole(x.y))
Последняя аксиома является потенциальновредной. Если а — это композиция ClassOfClassOfComposition,
то она может генерировать новый член б как заполнитель hasClassOfClassOfWhole. из которого следует
ClassOfClassOflndividual(b). Но так как это действительно впечет ClassOfClassOfComposition(b), то не суще
ствует неограниченная генерация новых членов на базе указанных аксиом.
Соединение с когерентной логикой CL не противоречит ИСО 15926-2 / настоящему стандарту. Имеет смысл
ее дальнейшее изучение по нескольким причинам:
- синтаксическая форма формул когерентной логики (CL) допускает использование очень простой проце
дуры доказательства, известной как «forward ground reasoning» (опережающее базовое логическое обоснование).
Данная процедура эффективна для формул когерентной логики (CL). с ее помощью легко строить умозаключения.
Предполагается, что алгоритмы проверки соответствия, основанные на лотке CL. могут быть использованы для
настоящего стандарта и ИСО 15926-2, которые более эффективны, чем алгоритмы, основанные на трансляции в
описательную логику (DL). Знание о структурах ИСО 15926-2 может быть использовано при построении исследо
вательских процедур;
- логика CL более выразительна, чем логика DL. Можно идентифицировать разрешимые фрагменты логики
CL, которые более удобны, чем логика DLдля приложений типа ИСО 15926, например, при указании ограничений
на архивы данных:
- когерентная лотка CL конструктивна. Это означает, что она более структурирована, чем логика первого
порядка FOL. Во многих ситуациях рассматриваемая структура способствует изучению мета-свойств.
Так как когерентная логика — это недостаточно изученный фрагмент логики первого порядка FOL, мы здесь
приводим некоторые ключевые сведения:
- когерентная логика CL возникла благодаря норвежцу Торалфу Скол ему (Thoralf Skolem), разработавшему
ее в 1920 г.Его целью было получение мета-математических результатов в теории кристаллических решеток и про
ективной геометрии [24]. [25]. Она также известна как геометрическая логика:
- недавно когерентная логика CL была открыта повторно: см. работу [15] (на предмет обоснования ее со
ответствия компьютерной науке) и работу [
12
] (в части достигнутого прогресса в компьютерных исследованиях,
выполненных на основе когерентной логики CL):
- «восходящие» процедуры доказательств, используемые сегодня в дедуктивных базах данных, и система
SATCHMO [21] (для логик слабее когерентной логики CL) описаны в работе [24];
- когерентная логика CL расширяет логику дизьюнкга Хорна [19]. на котором основан язык программирова
ния Пролог [20]. В нем. в заключение, можно получить полную дизъюнкцию экзистенциально квантифицированных
сопряжений элементов;
- неразрешимость когерентной логики CL без символов функций доказана в работе [13]:
- когерентная логика CL менее выразительна, чем полная лотка первого порядка FOL. Вместе с тем. суще
ствует естественная трансляция FOL в CL [14], дающая удовлетворительные результаты, правда, путем резкого
увеличения громоздкости формул. Каждая теория первого порядка имеет консервативное (определительное) рас
ширение. эквивалентное когерентной теории.
86