Taxonomic reasoning with many-sorted logics

This paper provides an introduction to many-sorted logics and motivates their use for representation and reasoning. Perhaps the most important reason to be interested in many-sorted logic is that computational efficiency can be achieved because the search space can be smaller and the length of a derivation shorter than in unsorted logic. There are many possible many-sorted logics of varying degrees of expressiveness, and the dimensions in which many-sorted logics differ are outlined and logics at various points in this space described. The relationship of many-sorted logic to unsorted logic is discussed and the reason why many-sorted logics derivations may be shorter is demonstrated. The paper concludes with a discussion of some many-sorted logic programming languages and some implementation issues.