В SHOIN(D) это эквивалентно семейству DL, используемому OWL-DL; Правомерно ли это выражение:
F ⊑ (≤1 r. D) ⊓ (￢ (=0 r. D))
Где F, D — концепты, r — роль. Я хочу показать, что каждый экземпляр F связан не более чем с одним экземпляром D через r, а не с нулем экземпляров.
В общем, как решить, что какое-то выражение допустимо w. р. т. конкретный вариант DL? Я подумал, что использование синтаксиса BNF варианта может быть тем, на что я нацелен.
Один простой способ — проверить, можете ли вы написать это в Protege. Большинство того, что вы можете написать в Protege, будет разрешено OWL-DL. В Протеже можно написать:
F SubClassOf ((r max 1 D) и не(r точно 0 D))
Конечно, сказать, что что-то имеет не более 1 значения, и не совсем одно, было бы в точности то же самое, что сказать, что оно имеет ровно 1:
F SubClassOf r точно 1 D
Но есть несколько вещей, которые вы сможете делать в Protege и которые не будут разрешены OWL-DL. Более прямой способ узнать, что это такое, — это стандарт, а именно: >11 глобальных ограничений на аксиомы в OWL 2 DL. Как правило, единственная проблема, с которой вы можете столкнуться, — это попытка использовать составные свойства там, где вам это не разрешено.
Если вы не хотите проверять вручную, вы можете попробовать загрузить свою онтологию в OWL Validator и выберите профиль OWL2 DL.
