Expressive description logics via SAT
Francis Gasse, Volker Haarslev · 2009
The Boolean Satisfiability (SAT) problem is widely researched and the solvers' performances largely benefit from it. Satisfiability Modulo Theory (SMT) solvers aim to leverage these performances toward other formalisms with large propositional content. Description Logics are an expressive subset of first-order logic with high complexity reasoning (e.g. SHOQ is Exp-Time-complete) that could benefit from this approach. In this paper, we present a SMT-based DL reasoner, its reasoning technique, its implementation and some early experimental results.