Tim@UPENN.CSNET (Tim Finin) (01/28/86)
LOGICAL SPECIFICATIONS FOR FEATURE
STRUCTURES IN UNIFICATION GRAMMARS
William C. Rounds and Robert Kasper, University of Michigan
3pm Tuesday, February 4, 1986
216 Moore, University of Pennsylvania
In this paper we show how to use a simple modal logic to give a complete
axiomatization of disjunctively specified feature or record structures commonly
used in unification-based grammar formalisms in computational linguistics. The
logic was originally developed as a logic to explain the semantics of
concurrency, so this is a radically different application. We prove a normal
form result based on the idea of Nerode equivalence from finite automata
theory, and we show that the satisfiability problem for our logical formulas is
NP-complete. This last result is a little surprising since our formulas do not
contain negation. Finally, we show how the unification problem for
term-rewriting systems can be expressed as the satisfiability problem for our
formulas.