A Complete and Recursive Feature Theory
<|reference_start|>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 formulae 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.<|reference_end|>
@article{backofen1994a,
    title={A Complete and Recursive Feature Theory},
    author={Rolf Backofen, Gert Smolka},
    journal={arXiv preprint arXiv:cmp-lg/9406019},
    year={1994},
    number={RR-92-30},
    archivePrefix={arXiv},
    eprint={cmp-lg/9406019},
    primaryClass={cmp-lg cs.CL}
}