Skip to main content
SpringerLink
Log in

Terminating Tableaux for the Basic Fragment of Simple Type Theory

  • Conference paper
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009)

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

Abstract

We consider the basic fragment of simple type theory, which restricts equations to base types and disallows lambda abstractions and quantifiers. We show that this fragment has the finite model property and that satisfiability can be decided with a terminating tableau system. Both results are with respect to standard models.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andrews, P.B.: Classical type theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 965–1007. Elsevier Science, Amsterdam (2001)

    Chapter  Google Scholar 

  2. Farmer, W.M.: The seven virtues of simple type theory. J. Appl. Log. 6(3), 267–286 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  3. Friedman, H.: Equality between functionals. In: Parikh, R. (ed.) Proc. Logic Colloquium 1972-73. Lectures Notes in Mathematics, vol. 453, pp. 22–37. Springer, Heidelberg (1975)

    Google Scholar 

  4. Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18, 194–211 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  5. Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  6. Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    Google Scholar 

  7. Andrews, P.B., Brown, C.E.: TPS: A hybrid automatic-interactive system for developing proofs. Journal of Applied Logic 4(4), 367–395 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  8. Benzmüller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - A cooperative automatic theorem prover for classical higher-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS(LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008)

    Google Scholar 

  9. Brown, C.E.: Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church’s Type Theory. College Publications (2007)

    Google Scholar 

  10. Takahashi, M.: A proof of cut-elimination theorem in simple type theory. Journal of the Mathematical Society of Japan 19, 399–410 (1967)

    Article  MATH  MathSciNet  Google Scholar 

  11. Prawitz, D.: Hauptsatz for higher order logic. J. Symb. Log. 33, 452–457 (1968)

    Article  MATH  MathSciNet  Google Scholar 

  12. Kohlhase, M.: Higher-order tableaux. In: Baumgartner, P., Posegga, J., Hähnle, R. (eds.) TABLEAUX 1995. LNCS, vol. 918, pp. 294–309. Springer, Heidelberg (1995)

    Google Scholar 

  13. Benzmüller, C.: Extensional higher-order paramodulation and RUE-resolution. In: Ganzinger, H. (ed.) CADE 1999. LNCS(LNAI), vol. 1632, pp. 399–413. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  14. Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Saarland University, Saarbrücken, Germany

    Chad E. Brown & Gert Smolka

Authors
  1. Chad E. Brown
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gert Smolka
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Informatics, University of Oslo, Blindern, P.O. Box 1080, 0316, Oslo, Norway

    Martin Giese  & Arild Waaler  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brown, C.E., Smolka, G. (2009). Terminating Tableaux for the Basic Fragment of Simple Type Theory. In: Giese, M., Waaler, A. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2009. Lecture Notes in Computer Science(), vol 5607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02716-1_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02716-1_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02715-4

  • Online ISBN: 978-3-642-02716-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation