AN ORDER-SORTED LOGIC FOR KNOWLEDGE REPRESENTATION SYSTEMS

Hybrid knowledge representation systems (such as those of the KL-ONE family) distinguish between taxonomical information (that is represented in the T-Box) and assertional information (which is contained in the A-Box). The basic concepts that establish a particular view of the world are considered static and given, once the knowledge base is set up. and these concepts are represented in the taxonomical hierarchy of the T-Box. For some applications in natural language processing this approach is insufficient as the taxonomical hierarchy may be changed while parsing new sentences. It may thus become necessary to express the changing taxonomical information in both the taxonomical hierarchy (the T-Box) and in the assertional knowledge base (the A-Box). In this case the notorious problems of coupling the two kinds of information (i.e. the A-Box and the T-Box) within one deductive calculus become even more complex, and we distinguish two approaches: a close coupling and a loose coupling. Within the framework of an order-sorted predicate logic we present a close coupling between the taxonomic information (that is expressed in the sort hierarchy) and the axiomatic part. We give a rigorous model-theoretic semantics, and present a deduction calculus that is based on three specially tailored rules of inference (extended order-sorted resolution, subsort resolution, and elimination). These rules are shown to be sound and complete for a clausal knowledge base which represents taxonomic information partly