Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability

In the last two decades, modal and description logics have been applied to numerous areas of computer science, including knowledge representation, formal verification, databas theory, distributed computing and, more recently, semantic web and ontologies. For this reason, the problem of automated reasoning in modal and description logics has been thoroughly investigated. In particular, many approaches have been proposed for e±ciently handling the satisfiability of the core normal modal logic Km, and of its notational variant, the description logic ALC. Although simple in structure, Km/ALC is computationally very hard to reason on, its satisfiability being PSpace-complete.In this paper we start exploring the idea of performing automated reasoning tasks in modal and description logics by encoding them into SAT, so that to be handled by state-of-the-art SAT tools; as with most previous approaches, we begin our investigation from the satisfiability in Km. We propose an efficient encoding, a...