DFKI Research Report-94-35
by Rolf Backofen
A Complete Axiomatization of a Theory with Feature and Arity Constraints
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.
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.