Skip to main content
SpringerLink
Log in

A Focused Sequent Calculus for Higher-Order Logic

  • Conference paper
Automated Reasoning (IJCAR 2014)

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

Included in the following conference series:

Abstract

We present a focused intuitionistic sequent calculus for higher-order logic. It has primitive support for equality and mixes λ-term conversion with equality reasoning. Classical reasoning is enabled by extending the system with rules for reductio ad absurdum and the axiom of choice. The resulting system is proved sound with respect to Church’s simple type theory. The soundness proof has been formalized in Agda. A theorem prover based on bottom-up search in the calculus has been implemented. It has been tested on the TPTP higher-order problem set with good results. The problems for which the theorem prover performs best require higher-order unification more frequently than the average higher-order TPTP problem. Being strong at higher-order unification, the system may serve as a complement to other theorem provers in the field.

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. Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–362 (2009)

    Article  MATH  Google Scholar 

  2. Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. Journal of Formalized Reasoning 3(1), 1–27 (2010)

    MATH  MathSciNet  Google Scholar 

  3. Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda — a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73–78. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Lindblad, F.: Higher-order proof construction based on first-order narrowing. Electron. Notes Theor. Comput. Sci. 196, 69–84 (2008)

    Article  Google Scholar 

  5. Middeldorp, A., Okui, S., Ida, T.: Lazy narrowing: Strong completeness and eager variable elimination. Theoretical Computer Science 167, 95–130 (1995)

    Article  MathSciNet  Google Scholar 

  6. Herbelin, H.: A lambda-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 61–75. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  7. Lengrand, S., Dyckhoff, R., McKinna, J.: A focused sequent calculus framework for proof search in pure type systems. Logical Methods in Computer Science 7(1) (2011)

    Google Scholar 

  8. Andreoli, J.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2, 297–347 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  9. Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51(12), 125–157 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  10. Girard, J.Y.: A new constructive logic: Classical logic. Mathematical Structures in Computer Science 1(3), 255–296 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  11. Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15(2), 81–91 (1950)

    Article  MATH  MathSciNet  Google Scholar 

  12. Lindblad, F.: AgsyHOL source code and Agda formalization (2012), https://github.com/frelindb/agsyHOL

  13. Lengrand, S.: Normalisation & Equivalence in Proof Theory & Type Theory. PhD thesis, Université Paris 7 & University of St Andrews (2006)

    Google Scholar 

  14. Lindblad, F.: Property directed generation of first-order test data. In: Trends in Functional Programming. Intellect, vol. 8, pp. 105–123 (2008)

    Google Scholar 

  15. Hanus, M.: Curry: An integrated functional logic language. Language report (March 2006), http://www.informatik.uni-kiel.de/~curry/report.html

Download references

Author information

Authors and Affiliations

  1. Chalmers University of Technology, University of Gothenburg, Gothenburg, Sweden

    Fredrik Lindblad

Authors
  1. Fredrik Lindblad
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS,, New York University &amp, USA

    Stéphane Demri

  2. Department of Computer Science, University of New Mexico, 87131-0001, Albuquerque, NM, USA

    Deepak Kapur

  3. Max Planck Institute for Informatics, Campus E1 4, 66123, Saarbrücken, Germany

    Christoph Weidenbach

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Lindblad, F. (2014). A Focused Sequent Calculus for Higher-Order Logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds) Automated Reasoning. IJCAR 2014. Lecture Notes in Computer Science(), vol 8562. Springer, Cham. https://doi.org/10.1007/978-3-319-08587-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08587-6_5

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08586-9

  • Online ISBN: 978-3-319-08587-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation