Resolution for label-based formulas in hierarchical representation. New Generation Computing 23(1

Abstract Order-sorted logic includes many and partially ordered sorts as a sort-hierarchy. In the field of knowledge representation and reasoning, it is useful to develop reasoning systems for terminological knowledge, together with assertional knowledge. However, the expression of sort-hierarchies cannot sufficiently capture the lexical diversity of terminological knowledge. In addition to sorts, various kinds of symbols: constants, functions and predicates are semantically and hierarchically associated with each other. This is because natural language words identifying these symbols can be employed in the description of terminological knowledge. In this paper, we present a label-based language for consistently handling the variety of hierarchical relationships among symbol names. For this language we develop a sorted resolution system whose reasoning power is enhanced by adding hierarchical inference rules with labeled substitutions