Consequence-Based Reasoning beyond Horn Ontologies
Frantisek Simancik, Yevgeny Kazakov and Ian Horrocks
Consequence-based ontology reasoning procedures have so far been known only for Horn ontology languages. A difficulty in extending such procedures is that non-Horn axioms, such as $A \sqsubseteq B\sqcup C$, seem to require reasoning by case, which causes non-determinism in tableau-based procedures. In this paper we present a consequence-based procedure for ALCH that overcomes this difficulty by using rules similar to ordered resolution to deal with disjunctive axioms in a deterministic way; it retains all the favourable attributes of existing consequence-based procedures, such as goal-directed ``one pass'' classification, optimal worst-case complexity, and ``pay-as-you-go'' behaviour. Our preliminary empirical evaluation demonstrates that the procedure scales well to non-Horn ontologies without adversely affecting performance on Horn ontologies.