Формальная семантика совы

Question

Из того, что я понял, читая книгу Основы технологий семантической паутины относительно формальной семантики сов, Hitzler и др. Предложили два типа теоретико-модельной семантики для SROIQ: один - проверка модели подобный подход (где мы проверяем различные интерпретации, чтобы найти модели нашей базы знаний), а другой - с помощью логики предикатов. В последнем подходе книга просто переводит SROIQ в логику предикатов.

Однако книга немного сбивает меня с толку, и я не знаю, правильно ли я понял некоторые пункты, поэтому вот мои вопросы:

1. Является ли проверка моделей разновидностью теоретико-модельной семантики?

2. Является ли перевод вашего SROIQ в логику предикатов также теоретико-модельной семантикой?

3. Как перевод SROIQ в логику предикатов является своего рода "семантикой"? Это потому, что после преобразования мы можем подобрать семантику и алгоритмы FOL?

Спасибо!

P.S. Это ссылка на книгу! На всякий случай!

Answer 1

Теоретическая семантика модели - это способ определения значения аксиом, т. Е. Какие правила доступны для построения модели или проверки ее правильности. Два примера: семантика OWL и семантика RDF. Они имеют много общего, но не идентичны.

Проверка модели не определяет семантику, она применяет семантические правила, определенные в модели, к фактическим базам знаний. Перевод в другой формализм, например предикаты, может поддерживать одинаковую семантику (т. Е. Все модели остаются одинаковыми в обоих формализмах), но это зависит от используемого формализма.