A complete and recursive feature theory. (English) Zbl 0873.68024
Summary: Various feature descriptions are being employed in logic programming languages and constraint-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 the so-called feature graphs, a data structure common in computational linguistics. The other two models consist of the 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.
References:
| [1] | Aït-Kaci, H., A lattice-theoretic approach to computation based on a calculus of partially ordered type structures, (Ph.D. Thesis (1984), University of Pennsylvenia: University of Pennsylvenia Philadelphia, PA) |
| [2] | Aït-Kaci, H., An algebraic semantics approach to the effective resolution of type equations, Theoret. Comput. Sci., 45, 293-351 (1986) · Zbl 0628.68010 |
| [3] | Aït-Kaci, H.; Nasr, R., LOGIN: A logic programming language with built-in inheritance, J. Logic Programming, 3, 185-215 (1986) · Zbl 0599.68013 |
| [4] | Aït-Kaci, H.; Nasr, R., Integrating logic and functional programming, Lisp Symbolic Computation, 2, 51-89 (1989) |
| [5] | Aït-Kaci, H.; Podelski, A., Towards a meaning of LIFE, J. Logic Programming, 16, 195-234 (1993) · Zbl 0782.68022 |
| [6] | Aït-Kaci, H.; Podelski, A.; Smolka, G., A feature-based constraint system for logic programming with entailment, Theoret. Comput. Sci., 122, 263-283 (1994) · Zbl 0801.68023 |
| [7] | Baader, F.; Bürckert, H. J.; Nebel, B.; Nutt, W.; Smolka, G., On the expressivity of feature logics with negation, functional uncertainty, and sort equations, J. Logic, Language Inform., 2, 1-18 (1993) · Zbl 0788.68131 |
| [8] | Carpenter, B., The Logic of Typed Feature Structures; with Applications to Unification Grammars, Logic Programs and Constraint Resolution, (Cambridge Tracts in Theoretical Computer Science (1992), Cambridge University Press: Cambridge University Press Cambridge, UK) · Zbl 0765.68006 |
| [9] | Colmerauer, A., Prolog and infinite trees, (Clark, K. L.; Tärnlund, S.-A., Logic Programming (1982), Academic Press: Academic Press New York), 153-172 |
| [10] | Colmerauer, A., Equations and inequations on finite and infinite trees, (Proc. 2nd Internat. Conf. on Fifth Generation Computer Systems (1984)), 85-99 |
| [11] | Johnson, M., Attribute-Value Logic and the Theory of Grammar, (CSLI Lecture Notes 16 (1988), Center for the Study of Language and Information, Stanford University: Center for the Study of Language and Information, Stanford University CA) |
| [12] | Johnson, M., Logic and feature structures, (Proc. of IJCAI-91. Proc. of IJCAI-91, Sydney, Australia (1991)) · Zbl 0757.03012 |
| [13] | Kaplan, R. M.; Bresnan, J., Lexical-functional grammar: A formal system for grammatical representation, (Bresnan, J., The Mental Representation of Grammatical Relations (1982), MIT Press: MIT Press Cambridge, MA), 173-381 |
| [14] | Kasper, R. T.; Rounds, W. C., The logic of unification in grammar, (Linguistics and Philosophy (1990)), 35-58 · Zbl 0715.03014 |
| [15] | Kasper, R. T.; Rounds, W. C., A logical semantics for feature structures, (Proc. 24th Ann. Meeting of the ACL, Columbia University. Proc. 24th Ann. Meeting of the ACL, Columbia University, New York, NY (1986)), 257-265 |
| [16] | Kay, M., Functional grammar, (Proc. Fifth Ann. Meeting of the Berkeley Linguistics Society. Proc. Fifth Ann. Meeting of the Berkeley Linguistics Society, Berkeley, CA (1979), Berkeley Linguistics Society) |
| [17] | Lassez, J.-L.; Maher, M. J.; Marriott, K., Unification revisted, (Minker, J., Foundations of Deductive Databases and Logic Programming (1988), Morgan Kaufmann: Morgan Kaufmann Los Altos, CA) · Zbl 0645.68046 |
| [18] | Maher, M. J., Complete axiomatizations of the algebras of finite, rational and infinite trees, (Proc. 3rd Ann. Symp. on Logic in Computer Science (1988)), 348-457, Edinburgh, Scotland |
| [19] | Moss, L. S., Completeness theorems for logics of feature structures, (Moschovakis, Y. N., Logic from Computer Science (1992), Springer: Springer Berlin), 387-403 · Zbl 0759.03016 |
| [20] | Rounds, W. C.; Kasper, R. T., A complete logical calculus for record structures representing linguistic information, (Proc. 1st IEEE Symp. on Logic in Computer Science. Proc. 1st IEEE Symp. on Logic in Computer Science, Boston, MA (1986)), 38-43 |
| [21] | Shieber, S. M., An Introduction to Unification-Based Approaches to Grammar, (Volume 4 of CSLI Lecture Notes (1986), Center for the Study of Language and Information, Stanford University: Center for the Study of Language and Information, Stanford University CA) · Zbl 0770.68008 |
| [22] | Smolka, G., Feature constraint logics for unification grammars, J. Logic Programming, 12, 51-87 (1992) · Zbl 0754.68108 |
| [23] | Smolka, G.; Treinen, R., Records for logic programming, (J. Logic Programming, 18 (1994)), 229-258 · Zbl 0803.68021 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
