Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

&: Automated natural deduction

  • Conference paper
  • First Online:
Automated Deduction—CADE-11 (CADE 1992)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 607))

Included in the following conference series:

Abstract

In this paper we describe a sequent calculus-based theorem prover called −5. The underlying logic of & is that of Zermelo set theory. In addition to the usual rules of first-order sequent based systems, the logic contains inference rules to handle set abstraction terms, including the ability to unify formulae involving such terms, and the ability to introduce new abstraction terms as instantiations. & also has novel derived rules and heuristics for making choices in the course of the proof of a theorem.

This paper is based on work supported by the National Science Foundation under award number ISI-8701133, and by Swarthmore College through a summer research award to Andrew Merrill and through the college's Research Support Fund.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. S.C. Bailin and D. Barker-Plummer. Automated Deduction in Set Theory. Technical Report NSF/ISI-90006.

    Google Scholar 

  2. S.C. Bailin. A λ unifiability test for set theory. Journal of Automated Reasoning, 4(3), September 1988.

    Google Scholar 

  3. S.C. Bailin and D. Barker-Plummer. Z-match: An inference rule for incrementally finding set instantiations. Submitted to the Journal of Automated Reasoning.

    Google Scholar 

  4. W.W. Bledsoe and G. Feng. Completeness of set-var. Technical Report ATP104, University of Texas at Austin, Department of Computer Sciences, Austin, Texas, 78712, December 1990.

    Google Scholar 

  5. W.W. Bledsoe. A maximal method for set variables in automatic theorem proving. In Machine Intelligence 9, pages 53–100. Ellis Harwood, Ltd., Chichester, 1979.

    Google Scholar 

  6. W.W. Bledsoe and M. Tyson. The Ut interactive prover. Memo ATP-17, Mathematics Department, University of Texas, May 1975.

    Google Scholar 

  7. G.P. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science 1, pages 27–57, 1974.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Swarthmore, College, 19081, Swarthmore, PA

    Dave Barker-Plummer & Andrew S. Merrill

  2. CTA, INCORPORATED, 6116 Executive Blvd, 20852, Rockville, Maryland

    Sidney C. Bailin

Authors
  1. Dave Barker-Plummer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sidney C. Bailin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andrew S. Merrill
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Deepak Kapur

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barker-Plummer, D., Bailin, S.C., Merrill, A.S. (1992). &: Automated natural deduction. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_210

Download citation

  • DOI: https://doi.org/10.1007/3-540-55602-8_210

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55602-2

  • Online ISBN: 978-3-540-47252-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation