Checking DL-Lite Modularity with QBF Solvers

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.

• Type: Conference
• Year: 2008
• Where: DLOG
• Authors: Roman Kontchakov, Vladislav Ryzhikov, Frank Wolter, Michael Zakharyaschev
• Keywords: Automated Reasoning, DLOG 2008, Off-the-shelf QBF Solvers, Quantified Boolean Formulas, Typical Dl-litebool Ontologies