Publication
KRIS: K-nowledge R-epresentation and I-nference S-ystem -System Description-
Franz Baader; Bernhard Hollunder
DFKI, DFKI Technical Memos (TM), Vol. 90-03, 1990.
Abstract
The knowledge representation system KL-ONE first appeared in 1977. Until 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 KL-ONE systems such as BACK, KL-TWO, LOOM, NIKL, SB-ONE 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 (and not just in toy examples). 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.