[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

On completeness theorems for feature logics

  • Published:
Annals of Mathematics and Artificial Intelligence Aims and scope Submit manuscript

    We’re sorry, something doesn't seem to be working properly.

    Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Abstract

We formulate a sequent calculusF and prove that it is sound, and complete in a strong sense with respect to a class offeature 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 underappropriateness conditions. This establishes various completeness theorems from the literature as applications of the results here. To demonstrate the generality of our results, we also prove, with 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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. R. Carpenter, A logic of typed feature structures, unpublished draft of monograph (1990).

  2. A. Dewar and K. Vijay-Shanker, A three-valued interpretation of negation in feature structure descriptions, in:27th Annual Meeting of the Association for Computational Linguistics (1991).

  3. D. Gabbay,Sematical Investigations in Heyting's Intuitionistic Logic (Reidel, 1981).

  4. G. Gentzen, Investigations into logical deduction, in:The Collected Papers of Gerhard Gentzen, ed. M.E. Szabo (North-Holland, Amsterdam, 1958).

    Google Scholar 

  5. J.-Y. Girard, Linear logic, Theor. Comp. Sci. 50 (1987).

  6. M. Johnson, Attribute-value logic and the theory of grammar, Ph.D. Thesis, Stanford University (1987).

  7. L. Karttunen, Features and structures, in:Proc. 10th Int. Conf. on Computational Linguistics: COLING 84 (1984).

  8. R.T. Kasper and W.C. Rounds, The logic of feature structures, Language and Philosophy 13(1) (1990).

  9. J.P. King, A logical formalism for HPSG, Ph.D. Thesis, University of Manchester (1989).

  10. M. D. Moshier and W.C. Rounds, A logic for partially specified data structures, in:Proc. 14th ACM Symp. on the Principles of Programming Languages (1987).

  11. M.A. Moshier, Extensions to unification grammar for the description of programming languages, Ph.D. Thesis, University of Michigan (1988).

  12. L.S. Moss, Completeness theorems for logics of feature structures, in:Proc. MSRI Workshop on Logic from Computer Science, ed. Y.N. Moschovakis (Springer, 1991).

  13. F.C.N. Pereira and S.M. Shieber, The semantics of grammar formalisms seen as computer languages, in:Proc. 10th Int. Conf. on Computational Linguistics: COLING 84 (1984).

  14. C. Pollard and I.A. Sag,Information-based Syntax and Semantics, Vol. 1, CSLI Lecture Notes (CSLI, 1987).

  15. H. Rasiowa,An Algebraic Approach to Non-Classical Logics, Vol. 78 ofStudies in Logic (North-Holland, 1976).

  16. W.C. Rounds and R.T. Kasper, A complete logical calculus for record structures representing 1c information, in:Proc. 15th Annual Meeting of the Symp. on Logic in Computer Science (1986).

  17. D. Scott, Completeness and axiomatizability in many valued logic, in:Proc. Tarski Symp., ed. L. Henkin et al. (1974).

  18. D. Scott, Domains for denotational semanics, in:Automata, Languages and Programming, Vol. 140, Lecture Notes in Computer Science (Springer, 1982).

  19. G. Smolka, A feature logic with subsorts, Technical Report No. LILOG-33, IBM-Deutschland (1988).

  20. G. Takeuti,Proof Theory, 2nd ed. (North-Holland, 1987).

Download references

Author information

Authors and Affiliations

  1. Program in Computing, University of California, Los Angeles, CA, USA

    M. Andrew Moshier

Authors
  1. M. Andrew Moshier
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

This research was supported by the National Science Foundation, Grant No. IRI-8806913.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Moshier, M.A. On completeness theorems for feature logics. Ann Math Artif Intell 8, 175–213 (1993). https://doi.org/10.1007/BF02451553

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02451553

Keywords

Search

Navigation