DFKI Research Report-92-30
by Rolf Backofen, Gert Smolka
A Complete and Recursive Feature Theory
Various feature descriptions are being employed in logic programming languages and constrained-based grammar formalisms. The common notational primitive of these descriptions are functional attributes called features. The descriptions considered in this paper are the possibly quantified first-order formular obtained from a signature of binary and unary predicates called features and sorts, respectively. We establish a first-order theory FT by means of three axiom schemes, show its completeness, and construct three elementarily equivalent models.One of the models consists of so-called feature graphs, a data structure common in computational linguistics. The other two models consist of so-called feature trees, a record-like data structure generalizing the trees corresponding to first-order terms. Our completeness proof exhibits a terminating simplification system deciding validity and satisfiability of possibly quantified feature descriptions.
This document is available as Postscript.
The next abstract is here, and the previous abstract is here.
Note: This page was written to look best with CSS stylesheet support Level 1 or higher. Since you can see this, your browser obviously doesn't support CSS, or you have turned it off. We highly recommend you use a browser that supports and uses CSS, and review this page once you do. However, don't fear, we've tried to write this page to still work and be readable without CSS.