Мне всегда было трудно понять , почему обоснование OWL-DL так эффективно в реальных приложениях.
Например, я часто использую онтологии, которые есть во фрагменте ALCQI обработан аргументом Fact ++, и общеизвестно, что выполнимость концепции является PSPACE-полной, а логическое значение - EXPTIME.
Здесь , на слайде 29 четко указано, что:
современные системы рассуждений DL основаны на методах таблиц, а не на автоматах
+ проще в реализации
- неоптимально с вычислительной точки зрения (NEXPTIME, 2NEXPTIME)
-> системы высоко оптимизированы
, несмотря на высокие вычислительные сложность, производительность на удивление хорошая в реальных приложениях:
- базы знаний с тысячами концепций и сотнями аксиом
- превосходят специализированные рассуждения модальной логики
С одной стороны доказано, что в вычислительном отношении они не оптимальны, с другой стороны, они эффективны в реальных приложениях даже для большого ввода, но я не могу найти в Интернете источники, объясняющие, почему это возможно, и как это обрабатывается.
Определенно, мне не хватает этого шага, который я действительно пытаюсь понять.
У кого-нибудь здесь есть идея?