Covering and disjointness constraints in type networks

First order theories with unary predicates and no function symbols are formal tools for describing the part of a knowledge base concerning the classes of objects and the semantic interdependencies among classes, such as IS-A relationships, disjointness, covering, partitioning, etc‥ In this paper we study the problems of predicate satisfiability and predicate subsumption in such theories. The former is the problem of determining if a model of a given theory exists in which a certain predicate is assigned some objects. The latter is the problem of determining if two classes are related through the IS-A relationship in a given theory. Two types of semantic interdependencies among classes are considered: disjointness and covering. Disjointness holds between two classes having no common elements, while covering, a generalization of the IS-A relationship, holds when a class is a subset of the union of other classes. The results reported in this paper show that even simple representation mechanisms can pose serious obstacles to the efficiency of the inference capabilities of knowledge representation languages.