@InProceedings{BS:Compl:ACL93-withoutfull,
  AUTHOR = 	"Rolf Backofen and Gert Smolka",
  TITLE = 	"A Complete and Recursive Feature Theory",
  booktitle = 	"Proc. of the 31$^{\it st}$ ACL",
  year = 	1993,
  pages = 	"193--200",
  organization = "Association for Computational Linguistics",
  address = 	"Columbus, Ohio"
, abstract = {Various feature descriptions are being employed in
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 formulae obtained from a
signature of features
and sorts.  We establish a complete first-order
theory FT by means of three axiom schemes
and construct three elementarily
equivalent models.
<P>
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.
<P>
Our completeness proof exhibits a terminating simplification
system deciding validity and satisfiability of possibly
quantified feature descriptions.
   }
}