Inconsistency-tolerant description logic. Part II: A tableau algorithm for CALC~C

摘要

In the first part of this paper, we motivated and defined three systems of constructive and inconsistency-tolerant description logic. The variety of arising systems is conditioned by the variety of approaches to defining modalities in the constructive setting. We also presented sound and complete tableau calculi for the logics under consideration. Whereas these calculi were not meant to give rise to tableau algorithms, in the present second part of the paper, after providing some motivation and recalling the main definitions, we adapt methods developed by R. Dyckhoff and by I. Horrocks and U. Sattler in order to define a tableau algorithm for our basic four-valued constructive description logic CALC~C. Notice that among the three logics defined in the first part of the paper, CALC~C is the only logic which lends itself to applications, because for the other logics it is unknown whether they are elementarily decidable. The presented algorithm for CALC~C is the first example of an elementary decision procedure for a constructive description logic.