Academic
Publications
Inconsistency-tolerant description logic. Part II: A tableau algorithm for CACLC

Inconsistency-tolerant description logic. Part II: A tableau algorithm for CACLC,10.1016/j.jal.2007.06.001,Journal of Applied Logic,Sergei P. Odintsov

Inconsistency-tolerant description logic. Part II: A tableau algorithm for CACLC   (Citations: 8)
BibTex | RIS | RefWorks Download
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 CALCC. Notice that among the three logics defined in the first part of the paper, CALCC 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 CALCC is the first example of an elementary decision procedure for a constructive description logic.
Journal: Journal of Applied Logic , vol. 6, no. 3, pp. 343-360, 2008
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: