Intuitionistic decision procedures since Gentzen

Roy Dyckhoff

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

2 Downloads (Pure)

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.
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
Publication statusPublished - 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
Country/TerritorySwitzerland
CityBern
Period13/12/1314/12/13
Internet address

Fingerprint

Dive into the research topics of 'Intuitionistic decision procedures since Gentzen'. Together they form a unique fingerprint.

Cite this