An efficient decision algorithm for feature logic

Abstract

Feature terms are a common denominator of basic data-structures in knowledge representation and computational linguistics. The adaptation of the usual unification algorithms for first order terms is not straightforward, because feature terms may contain logical disjunction. Expansion into disjunctive normal form would reduce the problem more or less to unification of first order terms. But for reasons of efficiency, rewriting into disjunctive normal form should not be compulsory. In this paper, a sequent calculus is defined which gives a clear formal basis for proof optimizations: inference steps which require more than one subproof, i.e. which lead towards a “disjunctive normal form”, are only performed when they are no longer unavoidable. It is shown that the calculus is sound and complete with respect to the so-called feature structure interpretations of feature terms.

This research was done while the author was granted a Monbusho-scholarship at Kyoto University. I wish to thank the researchers in Kyoto, in particular Makoto Nagao and Yuji Matsumoto, for the stimulating research environment they provided. I am in debt to Jochen Dörre and to three anonymous reviewers for pointing out deficiencies of an earlier version of this paper. The responsibility for errors resides with me.