Expressivity and decidability of first-order languages over feature trees

Abstract

This thesis studies feature trees as a semantic domain for various kinds of feature descriptions used in logic programming and constraint-based grammar formalisms. We show that feature trees serve as a canonical model for these descriptions which is mathematically simpler than the previously used standard interpretation, whose domain consists of feature graphs. Moreover, feature trees are the natural interpretation for the description language CFT [Smolka/Treinen94], which combines the expressivity of feature descriptions with first-order constructor terms. For this language, feature graphs do not provide the right semantics. But for the basic feature description language, we show that feature trees and feature graphs have exactly the same properties. Thus, feature trees are suitable to take over the role feature graphs have played so far. One major subject of this thesis is to investigate the expressivity of the different description languages under the feature tree interpretation. We show that the language F [Treinen93], which allows feature to be first-class values (i.e., which allows for quantification over features), is expressive enough to define functional uncertainty constraints [Kaplan/Maxwell88]. In this language one can even encode relations that are defined by the least interpretation of definite equivalences (under some restriction even those defined by the greatest interpretation). Prominent members of this class of relations are the one described by logic programs. Although a lot of different feature description languages have been introduced in the literature, there are only rare cases where the expressivity of these languages have been studied. Thus, this thesis provides a technical basis for such kinds of studies. In the rest of this thesis, we investigate decidable fragments of these languages. We will show that set of all formulae of the basic feature description language valid in the feature tree interpretation is decidable. The same holds for the language CFT. Furthermore, we show that satisfiability of positive formulae in the language of functional uncertainty constraints is decidable. This was stated as an open problem in [Kaplan/Maxwell88]. In all cases, we will present an effective decision algorithm.

Die Arbeit untersucht die formalen Grundlagen von Merkmalsbeschreibungen, die partielle Beschreibungen von abstrakten, record-ähnlichen Objekten darstellen.