1

It has always been hard to me to understand why OWL-DL reasoning is so efficient in real-world application.

For example, I often use ontologies which are in ALCQI fragment processed by the Fact++ reasoner, and it is well-known that concept satisfiability is PSPACE-complete and logical implication is EXPTIME.

Here, at slide 29 is clearly stated that:

the state-of-the-art DL reasoning systems are based on tableaux techniques and not on automata techniques

  • +easier to implement

  • -not computationally optimal (NEXPTIME, 2NEXPTIME)

    -->the systems are highly optimized

    despite the high computational complexity, the performance is surprisingly good in real world applications:

  • knowledge bases with thousands of concepts and hundreds of axioms
  • outperform specialized modal logics reasoners

From one side it is proven that computationally they are not optimal, on the other hand they are efficient in the real world application even for large input, but I can't find sources online that explain why this is possible and how this is handled.

Definitively, I'm missing this step that I'm really trying to understand.

Does anybody here have an idea?

Wall
  • 293
  • 3
  • 13
  • 1
    Worst case complexity often is just that: worst case. Determining why "real-world problems" may be handled much better in practice often requires surprisingly deep theorems, the best of which put limits on how efficiently an optimal solution can be approximated. I don't know if anyone's taking to proving such things about OWL-DL, but it would require work -- the worst case analysis by itself typically provides no insight. – Jeroen Mostert Mar 24 '20 at 10:38
  • 1
    'Real world' can be used in many different ways. Ontologies used in anger tend to be relatively small or simple (e.g., see the number of EL++ ontologies in actual systems), and from what I've seen one reason for that is that many reasoners can't take the strain. There is a wide gap between the optimizations in Konclude and those in JFact, to name only two reasoners I'm familiar with. (Full disclosure, the one I manage loses in the comparison :-) ) – Ignazio Mar 24 '20 at 11:55

0 Answers0