Skip to main content
SpringerLink
Log in

A Natural Proof System for Herbrand’s Theorem

  • Conference paper
  • First Online:
Logical Foundations of Computer Science (LFCS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10703))

Included in the following conference series:

Abstract

The reduction of undecidable first-order logic to decidable propositional logic via Herbrand’s theorem has long been of interest to theoretical computer science, with the notion of a Herbrand proof motivating the definition of expansion proofs. The problem of building a natural proof system around expansion proofs, with composition of proofs and cut-free completeness, has been approached from a variety of different angles. In this paper we construct a simple deep inference system for first-order logic, , based around the notion of expansion proofs, as a starting point to developing a rich proof theory around this foundation. Translations between proofs in this system and expansion proofs are given, retaining much of the structure in each direction.

This research has been supported by EPSRC Project EP/K018868/1 Efficient and Natural Proof Systems and ANR project FISP ANR-15-CE25-0014-01.

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 EPUB and 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

References

  1. Alcolei, A., Clairambault, P., Hyland, M., Winskel, G.: The true concurrency of Herbrand’s theorem (2017, submitted)

    Google Scholar 

  2. Aler Tubella, A.: A study of normalisation through subatomic logic. University of Bath (2016)

    Google Scholar 

  3. Aler Tubella, A., Guglielmi, A.: Subatomic proof systems: splittable systems. arXiv preprint arXiv:1703.10258 (2017)

  4. Aler Tubella, A., Guglielmi, A., Ralph, B.: Removing cycles from proofs. In: Goranko, V., Dam, M. (eds.) 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Stockholm, Sweden 2017. Leibniz International Proceedings in Informatics (LIPIcs), pp. 9:1–9:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)

    Google Scholar 

  5. Brünnler, K.: Deep inference and symmetry in classical proofs. Logos Verlag (2003)

    Google Scholar 

  6. Brünnler, K.: Two restrictions on contraction. Logic J. IGPL 11(5), 525–529 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  7. Brünnler, K.: Cut elimination inside a deep inference system for classical predicate logic. Stud. Logica. 82(1), 51–71 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  8. Buss, S.R.: On Herbrand’s theorem. In: Leivant, D. (ed.) LCC 1994. LNCS, vol. 960, pp. 195–209. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60178-3_85

    Chapter  Google Scholar 

  9. Chaudhuri, K., Hetzl, S., Miller, D.: A multi-focused proof system isomorphic to expansion proofs. J. Logic Comput. 26(2), 577–603 (2016). https://doi.org/10.1093/logcom/exu030

    Article  MathSciNet  MATH  Google Scholar 

  10. Guglielmi, A., Gundersen, T., Parigot, M.: A proof calculus which reduces syntactic bureaucracy. In: Proceedings of the 21st International Conference on Rewriting Techniques and Applications (Rta 2010), vol. 6, pp. 135–150 (2010). https://doi.org/10.4230/LIPIcs.RTA.2010.135

  11. Gundersen, T.E.: A general view of normalisation through atomic flows. University of Bath (2009)

    Google Scholar 

  12. Heijltjes, W.: Classical proof forestry. Ann. Pure Appl. Logic 161(11), 1346–1366 (2010). https://doi.org/10.1016/j.apal.2010.04.006

    Article  MathSciNet  MATH  Google Scholar 

  13. Herbrand, J., Goldfarb, W.D.: Logical Writings. Springer, Dordrecht (1971). https://doi.org/10.1007/978-94-010-3072-4

    Book  Google Scholar 

  14. Hetzl, S., Weller, D.: Expansion trees with cut. arXiv preprint arXiv:1308.0428 (2013)

  15. McKinley, R.: A sequent calculus demonstration of Herbrand’s theorem. arXiv preprint arXiv:1007.3414 (2010)

  16. McKinley, R.: Proof nets for Herbrand’s theorem. ACM Trans. Comput. Logic (TOCL) 14(1), 1–31 (2013). https://doi.org/10.1145/2422085.2422090

    Article  MathSciNet  MATH  Google Scholar 

  17. Miller, D.A.: A compact representation of proofs. Stud. Logica. 46(4), 347–370 (1987). https://doi.org/10.1007/BF00370646

    Article  MathSciNet  MATH  Google Scholar 

  18. Straßburger, L.: Some observations on the proof theory of second order propositional multiplicative linear logic. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 309–324. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02273-9_23

    Chapter  Google Scholar 

  19. Straßburger, L.: Deep inference, expansion trees, and proof graphs for second order propositional multiplicative linear logic, vol. RR-9071, p. 38. Inria Saclay Ile de France (2017)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Bath, Bath, UK

    Benjamin Ralph

Authors
  1. Benjamin Ralph
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Benjamin Ralph .

Editor information

Editors and Affiliations

  1. City University of New York, New York, New York, USA

    Sergei Artemov

  2. Cornell University, Ithaca, New York, USA

    Anil Nerode

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ralph, B. (2018). A Natural Proof System for Herbrand’s Theorem. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2018. Lecture Notes in Computer Science(), vol 10703. Springer, Cham. https://doi.org/10.1007/978-3-319-72056-2_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-72056-2_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-72055-5

  • Online ISBN: 978-3-319-72056-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation