Abstract

In this paper we define the syntax and semantics of a description logic ALCs which is the Description logic ALC combined with modal supervaluation logic for representing vague knowledge. The modal supervaluation operator which means ‘it is unequivocal that’ obeys the schemas of the logic S5. We introduce several new useful entailments in the new logic. We also present a tableau decision algorithm for ALCs. The tableau decision algorithm is based on a method introduced by Wolter and Zakharyaschev which is an elaborate combination of Wolper's tableau calculus for propositional modal logic, the standard tableau algorithm for ALC, and the method of quasimodels introduced by Wolter and Zakharyaschev. In this paper, the method is extended with Halpern's tableau calculus for propositional modal logic to handle the case of S5