Skip to content

Research at St Andrews

Intuitionistic decision procedures since Gentzen

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

DOI

Open Access permissions

Open

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 - Bern, Switzerland

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

  2. 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: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  3. 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: Contribution to journalArticle

  4. Cut-elimination, substitution and normalisation

    Dyckhoff, R. 2015 Dag Prawitz on Proofs and Meaning. Wansing, H. (ed.). Springer, p. 163-187 (Outstanding Contributions to Logic; vol. 7)

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

  5. Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators

    Dyckhoff, R., Sadrzadeh, M. & Truffaut, J. Nov 2013 In : ACM Transactions on Computational Logic. 14, 4, 38 p., 34

    Research output: Contribution to journalArticle

ID: 181525710