A Terminological Knowledge Representation System with Complete Inference Algorithms

Franz BaaderFranz Baader, B. HollunderB. Hollunder

Datei:BaaderHollunder-PDK-91.ps.gz

Download

Franz Baader, B. Hollunder
A Terminological Knowledge Representation System with Complete Inference Algorithms
Proceedings of the First International Workshop on Processing Declarative Knowledge, volume 572 of Lecture Notes in Computer Science, 67-85, 1991. Springer

Details
Bibtex

KurzfassungAbstract
The knowledge representation system KLONE first appeared in 1977. Since then many systems based on the idea of KLONE have been built. The formal model-theoretic semantics which has been introduced for KLONE languages provides means for investigating soundness and completeness of inference algorithms. It turned out that almost all implemented KLONE systems such as BACK, KLTWO, LOOM, NIKL, SBONE use sound but incomplete algorithms.
Until recently, sound AND complete algorithms for the basic reasoning facilities in these systems such as consistency checking, subsumption checking (classification) and realization were only known for rather trivial languages. However, in the last two years concept languages (term subsumption languages) have been thoroughly investigated. As a result of these investigations it is now possible to provide sound and complete algorithms for relatively large concept languages. In this paper we describe KRIS, which is an implemented prototype of a KLONE system where all reasoning facilities are realized by sound and complete algorithms. This system can be used to investigate the behaviour of sound and complete algorithms in practical applications. Hopefully, this may shed a new light on the usefulness of complete algorithms for practical applications, even if their worst case complexity is NP or worse.
KRIS provides a very expressive concept language, an assertional language, and sound and complete algorithms for reasoning. We have chosen the concept language such that it contains most of the constructs used in KLONE systems, with the obvious restriction that the interesting inferences such as consistency checking, subsumption checking, and realization are decidable. The assertional language is similar to languages normally used in such systems. The reasoning component of KRIS depends on sound and complete algorithms for reasoning facilities such as consistency checking, subsumption checking, retrieval, and querying.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BaaderHollunder-PDK-91,
  address = {Kaiserslautern (Germany)},
  author = {F. {Baader} and B. {Hollunder}},
  booktitle = {Proceedings of the First International Workshop on Processing Declarative Knowledge},
  pages = {67--85},
  publisher = {Springer--Verlag},
  series = {Lecture Notes in Computer Science},
  title = {A Terminological Knowledge Representation System with Complete Inference Algorithms},
  volume = {572},
  year = {1991},
}