Skip to content

Research at St Andrews

Intuitionistic decision procedures since Gentzen

Research output: Research - peer-reviewChapter (peer-reviewed)


Open Access permissions



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.


Original languageEnglish
Title of host publicationAdvances in Proof Theory
EditorsR Kahle, Th Strahm, Th Studer
PublisherBirkhäuser Basel
ISBN (Electronic)9783319291987
ISBN (Print)9783319291963
StatePublished - 5 May 2016
Eventapt13 Advances in Proof Theory - Exakte Wissenschaften (ExWi), University of Bern, Bern, Switzerland
Duration: 13 Dec 201314 Dec 2013

Publication series

NameProgress in Computer Science and Applied Logic
ISSN (Print)2297-0576


Otherapt13 Advances in Proof Theory
Internet address

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Analyticity, balance and non-admissibility of Cut in Stoic Logic

    Bobzien, S. & Dyckhoff, R. 20 Apr 2018 In : Studia Logica. First Online, 23 p.

    Research output: Research - peer-reviewArticle

  2. POSIX lexing with derivatives of regular expressions (proof pearl)

    Ausaf, F., Dyckhoff, R. & Urban, C. 2016 Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Blanchette, J. C. & Merz, S. (eds.). Springer, p. 69-86 18 p. (Lecture Notes in Computer Science; vol. 9807)

    Research output: ResearchConference contribution

  3. Some remarks on proof-theoretic semantics

    Dyckhoff, R. 2016 Advances in Proof-Theoretic Semantics. Piecha, T. & Schroeder-Heister, P. (eds.). Springer, p. 79-93 15 p. (Trends in Logic; vol. 43)

    Research output: Research - peer-reviewChapter (peer-reviewed)

  4. Geometrisation of first-order logic

    Dyckhoff, R. & Negri, S. Jun 2015 In : Bulletin of Symbolic Logic. 21, 2, p. 123–163 41 p.

    Research output: Research - peer-reviewArticle

ID: 181525710