@TechReport{Moshier:1993,
AUTHOR = {Moshier, M. Andrew},
TITLE = {On Completeness Theorems for Feature Logics},
YEAR = {1993},
MONTH = {April},
NUMBER = {31},
ADDRESS = {Saarbrücken},
TYPE = {CLAUS-Report},
INSTITUTION = {Universität des Saarlandes},
ABSTRACT = {We formulate a sequent calculus K and prove that it is sound and complete in a strong sense with respect to a class of feature structures. The proof of completeness involves proving, first, a general characterization of the conditions under which any sequent calculus (that permits unrestricted use of Gentzen's structural rules) is strongly complete with respect to a semantical interpretation. With this general characterization, we prove completeness of the sequent calculus as well as a uniform relativization of strong completeness under appropriateness conditions. This establishes various completeness theorems from the literature as applications of the results here. To demonstrate the generality of our result, we also prove, by exactly the same technique, the completeness of an intuitionistic version of the calculus with respect to a class of Kripke structures. We next turn to a proof theoretic result that is intimately related to completeness: cut elimination. We prove a version of cut elimination for the classical calculus under appropriateness conditions, and as a corollary that various fragments of the calculus are also sound and strongly complete. Finally, completeness of the fragments allows us to investigate a correspondence between certain information systems and certain calculi. With this, we show that Pereira and Shieber's Domain of Descriptions is sound and complete, but only in a weak sense, with respect to its intended semantics.}
}
|
