Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
A Survey on Ordinal Notations Around the Bachmann-Howard Ordinal Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Intuitionistic Decision Procedures Since Gentzen

verfasst von : Roy Dyckhoff

Erschienen in: Advances in Proof Theory

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Machine-Checked Proof-Theory for Propositional Modal Logics
Nächstes Kapitel The Operational Perspective: Three Routes
Fußnoten
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
The final “p” in the name indicates “propositional”.
 
3
He commented “Unfortunately, this method does not work for the second problem.”.
 
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
As realised by the author after too long a delay.
 
Literatur
1.
P. Abate, R. Goré, The Tableaux Work Bench, in Proceedings of IJCAR 2003. LNCS, vol. 2796 (Springer, 2003), pp. 230–236
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
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)
4.
5.
E.W. Beth, The Foundations of Mathematics (North-Holland, 1959)
6.
M. Bezem, T. Coquand, Automating coherent logic, in Proceedings of LPAR 2005. LNCS, vol. 3835 (Springer, 2005), pp. 246–260
7.
K. Brünnler, M. Lange, Cut-free sequent systems for temporal logic. J. Logic Algebraic Program. 76, 216–225 (2008)
8.
J. Caldwell, Decidability extracted: synthesizing “correct-by-construction” decision procedures from constructive proofs. Ph.D. dissertation (Cornell University, 1998)
9.
10.
11.
H. Curry, Foundations of Mathematical Logic (Dover Publications, 1963)
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)
13.
A.G. Dragalin, Mathematical Intuitionism, Translations of Mathematical Monographs 67 (Trans. E. Mendelson). (American Mathematical Society, Providence, R.I., 1988)
14.
15.
R. Dyckhoff, Yet Another Proof Engine, MS (available from the author) (2014)
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)
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
18.
R. Dyckhoff, S. Negri, Admissibility of structural rules for contraction-free systems of intuitionistic logic. J. Symb. Logic 65, 1499–1518 (2000)MathSciNetCrossRefMATH
19.
20.
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
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
23.
U. Egly, S. Schmitt, On intuitionistic proof transformations, their complexity, and application to constructive program synthesis. Fundamenta Informaticae 39, 59–83 (1999)
24.
M. Ferrari, C. Fiorentini, G. Fiorino, Simplification rules for intuitionistic propositional tableaux. ACM Trans. Comput. Log. 13, 14:1–14:23 (2012)
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)MathSciNetCrossRefMATH
26.
G. Fiorino, Decision procedures for propositional intermediate logics. Ph.D. thesis (Milan University, 2000)
27.
M. Fitting, Intuitionistic Logic, Model Theory and Forcing (North-Holland, 1969)
28.
M. Fitting, Proof Methods for Modal and Intuitionistic Logic (Reidel, 1983)
29.
T. Franzén, Algorithmic aspects of intuitionistic propositional logic, I and II, SICS Research Reports R870X and R8906, 1987 and 1989
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
31.
G. Gentzen, Untersuchungen über das logische Schliessen. Math. Zeitschrift 39, 176–210, 405–431 (1935)
32.
R. Goré, Tableau methods for modal and temporal logics, in Handbook of Tableau Methods (Kluwer, 1999), pp. 297–396
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
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
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)
36.
H. Herbelin, Séquents qu’on calcule. Thèse de Doctorat, Université Paris 7 (1995)
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
38.
J. Howe, Two loop-detection mechanisms: a comparison, in Proceedings of Tableaux 1997. LNCS, vol. 1227 (Springer, 1997), pp. 188–200
39.
J. Hudelmaier, A Prolog program for intuitionistic propositional logic, SNS-Bericht 88–28, Tübingen (1988)
40.
41.
J. Hudelmaier, An \(O(n\ log\ n)\)-SPACE decision procedure for intuitionistic propositional logic. J. Logic Comput. 3, 63–76 (1993)
42.
O. Ketonen, Untersuchungen zum Prädikatenkalkül. Annales Acad. Sci. Fenn, Ser. A.I. 23 (1944)
43.
S.C. Kleene, Introduction to Metamathematics (North-Holland, 1952)
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
45.
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
47.
S. Maehara, Eine Darstellung der Intuitionistischen Logik in der Klassischen. Nagoya Math. J. 7, 45–64 (1954)MathSciNetMATH
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)
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
50.
51.
G. Mints, Complexity of subclasses of the intuitionistic propositional calculus, Programming Logic (ed. by B. Nordström). BIT 31, 64–69 (1992)MathSciNetCrossRefMATH
52.
G. Mints, A Short Introduction to Intuitionistic Logic, CSLI Stanford Lecture Notes (Springer, 2000)
53.
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
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
56.
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
58.
J. von Plato, Saved from the Cellar: Gerhard Gentzen’s Shorthand Notes on Logic and Foundations of Mathematics Springer (to appear, 2016)
59.
S.L. Read, Semantic Pollution and Syntactic Purity, R. Symb. Logic 8, 649–691 (2015)
60.
D. Sahlin, T. Franzén, S. Haridi, An intuitionistic predicate logic theorem prover. J. Logic Comput. 2, 619–656 (1992)
61.
G. Sambin, S. Valentini, The modal logic of provability. The sequential approach. J. Philos. Logic 11, 311–342 (1982)
62.
R. Schmidt, D. Tishkovsky, Automated synthesis of tableau calculi. Logical Methods Comput. Sci. 7, 32 (2011)
63.
K. Schütte, Vollstandige Systeme modaler und intuitionistischer Logik, Ergebnisse der Mathematik (Springer, 1968)
64.
W. Sieg, S. Cittadini, Normal natural deduction proofs (in non-classical logics), in LNAI 2605 (Springer, 2005), pp. 169–191
65.
66.
T. Tammet, A resolution theorem prover for intuitionistic logic, in CADE-13. LNCS, vol. 1104 (Springer, 1996), pp. 2–16
67.
N. Tennant, Autologic (Edinburgh University Press, 1992)
68.
A.S. Troelstra, H. Schwichtenberg, Basic Proof Theory (Cambridge, 2001)
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)
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
71.
N.N. Vorob’ev, A new algorithm for derivability in the constructive propositional calculus. AMS Transl. Ser. 2(94), 37–71 (1970)MATH
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
73.
K. Weich, Improving proof search in intuitionistic propositional logic. Munich Ph.D. thesis, also from Logos Verlag Berlin (2001)
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
Metadaten
Titel
Intuitionistic Decision Procedures Since Gentzen
verfasst von
Roy Dyckhoff
Copyright-Jahr
2016
Buch
Advances in Proof Theory

Print ISBN: 978-3-319-29196-3

Electronic ISBN: 978-3-319-29198-7

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-29198-7_6