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

Intuitionistic Decision Procedures Since Gentzen

  • Chapter
  • First Online:
Advances in Proof Theory

Part of the book series: Progress in Computer Science and Applied Logic ((PCS,volume 28))

Abstract

Gentzen solved the decision problem for intuitionistic propositional logic in his doctoral thesis [31]; this paper reviews some of the subsequent progress. Solutions to the problem are of importance both for general philosophical reasons and because of their use in implementations of proof assistants (such as Coq [4], widely used in software verification) based on intuitionistic logic.

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

Access this chapter

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

eBook
USD 15.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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

Similar content being viewed by others

Notes

  1. 1.

    A referee points out that this paper gave a classical provability interpretation of intuitionistic logic and an early syntactic proof of its faithfulness, a result conjectured by Gödel (and proved semantically by McKinsey and Tarski), as could usefully have been mentioned in [20].

  2. 2.

    The final “p” in the name indicates “propositional”.

  3. 3.

    He commented “Unfortunately, this method does not work for the second problem.”.

  4. 4.

    As established using a cut of the conclusion with \(D, D\!\rightarrow \!P \Longrightarrow P\) and a cut with \(C, D\!\rightarrow \!P, P\!\rightarrow \!B \Longrightarrow (C \!\rightarrow \!D) \!\rightarrow \!B\).

  5. 5.

    As realised by the author after too long a delay.

References

  1. P. Abate, R. Goré, The Tableaux Work Bench, in Proceedings of IJCAR 2003. LNCS, vol. 2796 (Springer, 2003), pp. 230–236

    Google Scholar 

  2. R. Antonsen, A. Waaler, A labelled system for IPL with variable splitting, in Proceedings of CADE 2007. LNAI, vol. 4603 (Springer, 2007), pp. 132–146

    Google Scholar 

  3. A. Avellone, G. Fiorino, U. Moscato, An implementation of a \(O(n\ log\ n)\)-SPACE decision procedure for propositional intuitionistic logic, in 3rd International Workshop on the Implementation of Logics (Tbilisi, Georgia, Oct 2002)

    Google Scholar 

  4. B. Barras, S. Boutin, et al., The Coq proof assistant reference manual, version 6.2.1. Technical Report, INRIA (2000). http://www.ftp.inria.fr

  5. E.W. Beth, The Foundations of Mathematics (North-Holland, 1959)

    Google Scholar 

  6. M. Bezem, T. Coquand, Automating coherent logic, in Proceedings of LPAR 2005. LNCS, vol. 3835 (Springer, 2005), pp. 246–260

    Google Scholar 

  7. K. Brünnler, M. Lange, Cut-free sequent systems for temporal logic. J. Logic Algebraic Program. 76, 216–225 (2008)

    Google Scholar 

  8. J. Caldwell, Decidability extracted: synthesizing “correct-by-construction” decision procedures from constructive proofs. Ph.D. dissertation (Cornell University, 1998)

    Google Scholar 

  9. L. Catach, TABLEAUX: a general theorem prover for modal logics. J. Autom. Reason. 7, 489–510 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  10. G. Corsi, G. Tassi, Intuitionistic logic freed of all metarules. J. Symb. Logic 72, 1204–1218 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  11. H. Curry, Foundations of Mathematical Logic (Dover Publications, 1963)

    Google Scholar 

  12. K. Dos̆en, A note on Gentzen’s decision procedure for intuitionistic propositional logic. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 33, 453–456 (1987)

    Google Scholar 

  13. A.G. Dragalin, Mathematical Intuitionism, Translations of Mathematical Monographs 67 (Trans. E. Mendelson). (American Mathematical Society, Providence, R.I., 1988)

    Google Scholar 

  14. R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic. J. Symb. Logic 57, 795–807 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  15. R. Dyckhoff, Yet Another Proof Engine, MS (available from the author) (2014)

    Google Scholar 

  16. R. Dyckhoff, D. Kesner, S. Lengrand, Strong cut-elimination systems for Hudelmaier’s depth-bounded sequent calculus for implicational logic, in IJCAR 2006 Proceedings. LNCS, vol. 4130, pp. 347–361 (2006)

    Google Scholar 

  17. R. Dyckhoff, S. Lengrand, LJQ: a strongly focused calculus for intuitionistic logic, in Proceedings of Computability in Europe 2006. LNCS, vol. 3988 (Springer, 2006), pp. 173–185

    Google Scholar 

  18. R. Dyckhoff, S. Negri, Admissibility of structural rules for contraction-free systems of intuitionistic logic. J. Symb. Logic 65, 1499–1518 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  19. R. Dyckhoff, S. Negri, Decision methods for linearly ordered Heyting algebras. Arch. Math. Log. 45, 411–422 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  20. R. Dyckhoff, S. Negri, Proof analysis for intermediate logics. Arch. Math. Log. 51, 71–92 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  21. R. Dyckhoff, S. Negri, Geometrisation of first-order logic, B. Symb. Logic 21, 123–163 (2015) Geometrisation of First-order Formulae, Submitted June 2014

    Google Scholar 

  22. R. Dyckhoff, S. Negri, Coherentisation of accessibility conditions in labelled sequent calculi, in Extended Abstract (2 pp.), Gentzen Systems and Beyond 2014, Informal Proceedings, ed. by R. Kuznets & G. Metcalfe. Vienna Summer of Logic, July 2014

    Google Scholar 

  23. U. Egly, S. Schmitt, On intuitionistic proof transformations, their complexity, and application to constructive program synthesis. Fundamenta Informaticae 39, 59–83 (1999)

    Google Scholar 

  24. M. Ferrari, C. Fiorentini, G. Fiorino, Simplification rules for intuitionistic propositional tableaux. ACM Trans. Comput. Log. 13, 14:1–14:23 (2012)

    Google Scholar 

  25. M. Ferrari, C. Fiorentini, G. Fiorino, Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models. J. Autom. Reason. 51, 129–149 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  26. G. Fiorino, Decision procedures for propositional intermediate logics. Ph.D. thesis (Milan University, 2000)

    Google Scholar 

  27. M. Fitting, Intuitionistic Logic, Model Theory and Forcing (North-Holland, 1969)

    Google Scholar 

  28. M. Fitting, Proof Methods for Modal and Intuitionistic Logic (Reidel, 1983)

    Google Scholar 

  29. T. Franzén, Algorithmic aspects of intuitionistic propositional logic, I and II, SICS Research Reports R870X and R8906, 1987 and 1989

    Google Scholar 

  30. D. Garg, V. Genovese, S. Negri, Countermodels from sequent calculi in multi-modal logics, in Proceedings of LICS 2012 (IEEE, 2012), pp. 315–324

    Google Scholar 

  31. G. Gentzen, Untersuchungen über das logische Schliessen. Math. Zeitschrift 39, 176–210, 405–431 (1935)

    Google Scholar 

  32. R. Goré, Tableau methods for modal and temporal logics, in Handbook of Tableau Methods (Kluwer, 1999), pp. 297–396

    Google Scholar 

  33. R. Goré, J. Thomson, BDD-based automated reasoning in propositional non-classical logics: progress report, in Proceedings of PAAR-2012, EPiC Series 21 (EasyChair, 2013), pp 43–57

    Google Scholar 

  34. R. Goré, J. Thomson, J. Wu, A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description, in Proceedings of IJCAR 2014. LNAI, vol. 8562 (Springer, 2014), pp. 262–268

    Google Scholar 

  35. J. Goubault-Larrecq, Implementing tableaux by decision diagrams, Unpublished note, Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, 47 pp. (1996)

    Google Scholar 

  36. H. Herbelin, Séquents qu’on calcule. Thèse de Doctorat, Université Paris 7 (1995)

    Google Scholar 

  37. A. Heuerding, M. Seyfried, H. Zimmermann, Efficient loop-check for backward proof search in some non-classical logics, in Proceedings of Tableaux 1996. LNAI, vol. 1071 (Springer, 1996), pp. 210–225

    Google Scholar 

  38. J. Howe, Two loop-detection mechanisms: a comparison, in Proceedings of Tableaux 1997. LNCS, vol. 1227 (Springer, 1997), pp. 188–200

    Google Scholar 

  39. J. Hudelmaier, A Prolog program for intuitionistic propositional logic, SNS-Bericht 88–28, Tübingen (1988)

    Google Scholar 

  40. J. Hudelmaier, Bounds for cut elimination in intuitionistic propositional logic. Arch. Math. Logic 31, 331–353 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  41. J. Hudelmaier, An \(O(n\ log\ n)\)-SPACE decision procedure for intuitionistic propositional logic. J. Logic Comput. 3, 63–76 (1993)

    Google Scholar 

  42. O. Ketonen, Untersuchungen zum Prädikatenkalkül. Annales Acad. Sci. Fenn, Ser. A.I. 23 (1944)

    Google Scholar 

  43. S.C. Kleene, Introduction to Metamathematics (North-Holland, 1952)

    Google Scholar 

  44. D. Larchey-Wendling, D. Mery, D. Galmiche, STRIP: structural sharing for efficient proof-search, in Proceedings of IJCAR 2001. LNCS, vol. 2083 (Springer, 2001), pp. 696–700

    Google Scholar 

  45. P. Lincoln, A. Scedrov, N. Shankar, Linearizing intuitionistic implication. Ann. Pure Appl. Logic 60, 151–177 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  46. O. Gasquet, A. Herzig, D. Longin, M. Sahade, LoTREC: logical tableaux research engineering companion, in Proceedings of Tableaux 2005. LNCS, vol. 3702 (Springer, 2005), pp. 318–322

    Google Scholar 

  47. S. Maehara, Eine Darstellung der Intuitionistischen Logik in der Klassischen. Nagoya Math. J. 7, 45–64 (1954)

    MathSciNet  MATH  Google Scholar 

  48. S.Yu. Maslov, An inverse method of establishing deducibility in the classical predicate calculus. Dokl. Akad. Nauk. SSSR 159, 17–20 (translated as Soviet Math. Dokl. 5, 1420) (1964)

    Google Scholar 

  49. S. McLaughlin, F. Pfenning, Imogen: focusing the polarized inverse method for intuitionistic propositional logic, in Proceedings of LPAR’08. LNCS, vol. 5330 (Springer, 2008), pp. 174–181

    Google Scholar 

  50. G. Mints, Gentzen-type systems and resolution rule. Part I. LNCS 417, 198–231 (1990)

    MathSciNet  MATH  Google Scholar 

  51. G. Mints, Complexity of subclasses of the intuitionistic propositional calculus, Programming Logic (ed. by B. Nordström). BIT 31, 64–69 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  52. G. Mints, A Short Introduction to Intuitionistic Logic, CSLI Stanford Lecture Notes (Springer, 2000)

    Google Scholar 

  53. S. Negri, Proofs and countermodels in non-classical logics. Logica Universalis 8, 25–60 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  54. K. Ono, Logische Untersuchungen über die Grundlagen der Mathematik. J. Fac. Sci. Imperial Univ. Tokyo. Section I. Math. Astron. Phys. Chem. 3, 329–389 (1938)

    MATH  Google Scholar 

  55. J. Otten, Clausal connection-based theorem proving in intuitionistic first-order logic, in Proceedings of Tableaux 2005. LNCS, vol. 3702 (Springer, 2005), pp 245–261

    Google Scholar 

  56. J. Otten, The ILTP Library. http://www.cs.uni-potsdam.de/ti/iltp/

  57. L. Pinto, R. Dyckhoff, Loop-free construction of counter-models for intuitionistic propositional logic, Symposia Gaussiana, Conf. A, ed. by M. Behara, R. Fritsch, R.G. Lintz (Walter de Gruyter & Co, Berlin, 1995), pp. 225–232

    Google Scholar 

  58. J. von Plato, Saved from the Cellar: Gerhard Gentzen’s Shorthand Notes on Logic and Foundations of Mathematics Springer (to appear, 2016)

    Google Scholar 

  59. S.L. Read, Semantic Pollution and Syntactic Purity, R. Symb. Logic 8, 649–691 (2015)

    Google Scholar 

  60. D. Sahlin, T. Franzén, S. Haridi, An intuitionistic predicate logic theorem prover. J. Logic Comput. 2, 619–656 (1992)

    Google Scholar 

  61. G. Sambin, S. Valentini, The modal logic of provability. The sequential approach. J. Philos. Logic 11, 311–342 (1982)

    Google Scholar 

  62. R. Schmidt, D. Tishkovsky, Automated synthesis of tableau calculi. Logical Methods Comput. Sci. 7, 32 (2011)

    Google Scholar 

  63. K. Schütte, Vollstandige Systeme modaler und intuitionistischer Logik, Ergebnisse der Mathematik (Springer, 1968)

    Google Scholar 

  64. W. Sieg, S. Cittadini, Normal natural deduction proofs (in non-classical logics), in LNAI 2605 (Springer, 2005), pp. 169–191

    Google Scholar 

  65. R. Statman, Intuitionistic propositional logic is polynomial-space complete. Theoret. Comput. Sci. 9, 67–72 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  66. T. Tammet, A resolution theorem prover for intuitionistic logic, in CADE-13. LNCS, vol. 1104 (Springer, 1996), pp. 2–16

    Google Scholar 

  67. N. Tennant, Autologic (Edinburgh University Press, 1992)

    Google Scholar 

  68. A.S. Troelstra, H. Schwichtenberg, Basic Proof Theory (Cambridge, 2001)

    Google Scholar 

  69. J. Underwood, A constructive completeness proof for intuitionistic propositional calculus, TR 90–1179, Department of Computer Science, Cornell University, 1990; also in Proceedings of the Workshop on Analytic Tableaux (Marseille, 1993)

    Google Scholar 

  70. N.N. Vorob’ev, The derivability problem in the constructive propositional calculus with strong negation. Doklady Akademii Nauk SSSR 85, 689–692 (1952)

    MathSciNet  Google Scholar 

  71. N.N. Vorob’ev, A new algorithm for derivability in the constructive propositional calculus. AMS Transl. Ser. 2(94), 37–71 (1970)

    MATH  Google Scholar 

  72. A. Waaler, L. Wallen, Tableaux methods in intuitionistic logic, in Handbook of Tableaux Methods, ed. by M. D’Agostino, D.M. Gabbay, R. Hähnle, J. Posegga (Kluwer, Dordrecht, 1999), pp. 255–296

    Google Scholar 

  73. K. Weich, Improving proof search in intuitionistic propositional logic. Munich Ph.D. thesis, also from Logos Verlag Berlin (2001)

    Google Scholar 

  74. K. Weich, Decision procedures for intuitionistic propositional logic by program extraction, in Proceedings of Tableaux 1998. LNCS, vol. 1397 (Springer, 1998), pp. 292–306

    Google Scholar 

Download references

Acknowledgments

Thanks are especially due to Gerhard Jäger and Helmut Schwichtenberg, whose scientific encouragement over the years has been substantial; and to Grisha Mints, now, alas, no longer with us, for helpful comments on historical matters—regrettably not all incorporated (thanks to a failure of technology).

Author information

Authors and Affiliations

  1. University of St. Andrews, St. Andrews, UK

    Roy Dyckhoff

Authors
  1. Roy Dyckhoff
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Roy Dyckhoff .

Editor information

Editors and Affiliations

  1. Campus de Caparica DM FCT, Univ Nova de Lisboa, Caparica, Portugal

    Reinhard Kahle

  2. Inst.of Computer Sci. applied math., University of Bern, Bern, Switzerland

    Thomas Strahm

  3. Institute of Computer Science and A, University of Berne, Berne, Switzerland

    Thomas Studer

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Dyckhoff, R. (2016). Intuitionistic Decision Procedures Since Gentzen. In: Kahle, R., Strahm, T., Studer, T. (eds) Advances in Proof Theory. Progress in Computer Science and Applied Logic, vol 28. Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-29198-7_6

Download citation

Publish with us

Policies and ethics

Search

Navigation