Satisfiability Checking and Query Answering for Large Ontologies
Christoph Weidenbach, Patrick Wischnewski · EPiC series in computing · 2018
In this paper we develop a sound, complete and terminating superposition calculus plus a query answering calculus for the BSH-Y2 fragment of the Bernays-Schoenfinkel Horn class of first-order logic. BSH-Y2 can be used to represent expressive ontologies. In addition to checking consistency, our calculus supports query answering for queries with arbitrary quantifier alternations. Experiments on BSH-Y2 (fragments) of several large ontologies show that our approach advances the state of the art.