ON SETS OF TERMS: A STUDY OF A GENERALISATION RELATION AND OF ITS ALGORITHMIC PROPERTIES

Signatures, as introduced to cope with semantics of programming languages, provide an interesting framework for knowledge representation. They allow structured and recursive properties that attribute representation does not permit, and at the same time seem to be algorithmically treatable. We recall how a generalisation relation on terms can be introduced by means of the classical special symbol Ω, whose meaning is “indeterminate”, and the partial order inductively defined on the terms. This formalism can nevertheless not take into account negation or disjunction. We provide in this paper a generalisation relation on sets of terms to withdraw these restrictions. This relation has different definitions (syntactical, set-theoretic, and based on a closed world assumption) that are proved to be equivalent for specific classes of signatures. They yield an equivalence relation whose canonical form is studied. We also study the combinatorial and algorithmic issues of the generalisation relation: the following problems are proved to be decidable (on finite data) but generally at least NP-complete: Does set A generalise set B? Are sets A and B equivalent? Is set B the canonical form of set A? Compute the negation of set A.... In the case where one of the sets contains only terms maximal for the generalisation relation, the first three problems are shown to be polynomial.