@article{Backofen:95,
author = {Backofen, Rolf},
title = {A Complete Axiomatization of a Theory with
         Feature and Arity Constraints},
journal = {Journal of Logic Programming},
year = {1995},
doi = {10.1016/0743-1066(95)00033-G},
volume = {24},
pages = {37-72},
abstract = {CFT is a recent constraint system providing records as a logical data
            structure for logic programming and for natural language processing.
            It combines the rational tree system as defined for logic programming
            with the feature tree system as used in natural language processing.
            
            The formulae considered in this paper are all first-order-logic
            formulae over a signature of binary and unary predicates called
            features and arities, respectively.  We establish the theory CFT by
            means of seven axiom schemes and show its completeness.
            
            Our completeness proof exhibits a terminating simplification
            system deciding validity and satisfiability of possibly
            quantified record descriptions.}
}