Checking DL-Lite modularity with QBF solvers
Roman Kontchakov, Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev · 2008
Abstract. We show how the reasoning tasks of checking various versions of conservativity for the description logic DL-Litebool can be reduced to satisfiability of quantified Boolean formulas and how off-the-shelf QBF solvers perform on a number of typical DL-Litebool ontologies. 1