A COMPLETE AND RECURSIVE FEATURE THEORY

Citation
R. Backofen et G. Smolka, A COMPLETE AND RECURSIVE FEATURE THEORY, Theoretical computer science, 146(1-2), 1995, pp. 243-268
Citations number
23
Categorie Soggetti
Computer Sciences","Computer Science Theory & Methods
ISSN journal
03043975
Volume
146
Issue
1-2
Year of publication
1995
Pages
243 - 268
Database
ISI
SICI code
0304-3975(1995)146:1-2<243:ACARFT>2.0.ZU;2-M
Abstract
Various feature descriptions are being employed in logic programming l anguages and constraint-based grammar formalisms. The common notationa l primitive of these descriptions are functional attributes called fea tures. The descriptions considered in this paper are the possibly quan tified first-order formulae obtained from a signature of binary and un ary predicates called features and sorts, respectively. We establish a first-order theory FT by means of three axiom schemes, show its compl eteness, and construct three elementarily equivalent models. One of th e models consists of the so-called feature graphs, a data structure co mmon in computational linguistics. The other two models consist of the so-called feature trees, a record-like data structure generalizing th e trees corresponding to first-order terms. Our completeness proof exh ibits a terminating simplification system deciding validity and satisf iability of possibly quantified feature descriptions.