Skip to content

Research at St Andrews

Intuitionistic decision procedures since Gentzen

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)


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
Publication statusPublished - 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., Apr 2019, In : Studia Logica. 107, 2, p. 375–397 23 p.

    Research output: Contribution to journalArticle

  2. Indefinite proof and inversions of syllogisms

    Dyckhoff, R., 2019, In : Bulletin of Symbolic Logic. 25, 2, p. 196-207 12 p.

    Research output: Contribution to journalArticle

  3. Contraction-free sequent calculi in intuitionistic logic: a correction

    Dyckhoff, R., Dec 2018, In : Journal of Symbolic Logic. 83, 4, p. 1680-1682 3 p.

    Research output: Contribution to journalArticle

  4. 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: Chapter in Book/Report/Conference proceedingConference contribution

ID: 181525710