Straccia U. A sequent calculus for reasoning in four-valued description logics. In: Automated Reasoning with Analytic Tableaux and Related Methods. International Conference, TABLEAUX'97 (Pont-...-Mousson, France, 1997). Proceedings, pp. 343 - 357. D. Galmiche (ed.). (Lecture Notes in Artificial Intelligence, vol. 1227). Springer, 1997. |

Abstract (English) |
Description Logics (DLs, for short) provide a logical reconstruction of the so-called frame-based knowledge representation languages. Originally, four-valued DLs have been proposed in order to develop expressively powerful DLs with tractable subsumption algorithms. Recently, four-valued DLs have been proposed as a model for (multimedia) document retrieval. In this context, the main reasoning task is instance checking. Unfortunately, the known subsumption algorithms for four-valued DLs, based on structural subsumption, do not work with respect to the semantics proposed in the DL-based approach to document retrieval. Moreover, they are unsuitable for solving the instance checking problem, as this latter problem is more general than the subsumption problem. We present an alternative decision procedure for four-valued DLs with the aim to solve these problems. The decision procedure is a sequent calculus for instance checking. Since in general the four-valued subsumption problem can be reduced to the four-valued instance checking problem, we obtain a decision procedure for the subsumption problem. Some related complexity results will be presented. | |

URL: | http://www.springerlink.com/content/w42063m42084015n/fulltext.pdf | |

Subject | Description logics I.2.4 Knowledge Representation Formalisms and Methods |

1) Download Document PDF |

Open access Restricted Private