Skip to content

Research at St Andrews

Intuitionistic decision procedures since Gentzen

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

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.
Close

Details

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

Publication series

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

Other

Otherapt13 Advances in Proof Theory
CountrySwitzerland
CityBern
Period13/12/1314/12/13
Internet address

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

View graph of relations

Related by author

  1. 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

  2. Indefinite proof and inversions of syllogisms

    Dyckhoff, R. 14 Jul 2018 (Accepted/In press) In : Bulletin of Symbolic Logic. 13 p.

    Research output: Contribution to journalArticle

  3. 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: 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