Completing sort hierarchies

AbstractThis paper discusses the structure of sort (or is-a) hierarchies. The effect of different kinds of such hierarchies on different kinds of many sorted logic is discussed both from the point of view of expressiveness and computational efficiency in resolution theorem proving. A technique for improving the computational efficiency of inference when the sort hierarchy is incompletely specified is suggested, which involves embedding the hierarchy into a complete Boolean lattice without losing information on under specified sorts. Such an embedding can be used for any poset or lattice structured hierarchy