DFKI Research Report-92-30



Language: English

by Rolf Backofen, Gert Smolka

A Complete and Recursive Feature Theory

32 Pages


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.

DFKI-Bibliothek (bib@dfki.uni-kl.de)

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.