Intuitionistic decision procedures since Gentzen

Roy Dyckhoff

doi:10.1007/978-3-319-29198-7_6

Intuitionistic decision procedures since Gentzen

Roy Dyckhoff

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

14 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 language	English
Title of host publication	Advances in Proof Theory
Editors	R Kahle, Th Strahm, Th Studer
Publisher	Birkhäuser Basel
Pages	245-267
ISBN (Electronic)	9783319291987
ISBN (Print)	9783319291963
DOIs	https://doi.org/10.1007/978-3-319-29198-7_6
Publication status	Published - 5 May 2016
Event	apt13 Advances in Proof Theory - Exakte Wissenschaften (ExWi), University of Bern, Bern, Switzerland Duration: 13 Dec 2013 → 14 Dec 2013 http://apt13.unibe.ch/

Publication series

Name	Progress in Computer Science and Applied Logic
Volume	28
ISSN (Print)	2297-0576

Other

Other	apt13 Advances in Proof Theory
Country/Territory	Switzerland
City	Bern
Period	13/12/13 → 14/12/13
Internet address	http://apt13.unibe.ch/

Access to Document

10.1007/978-3-319-29198-7_6

BernPaper14
© 2016, Springer International Publishing Switzerland. This work is made available online in accordance with the publisher’s policies. This is the author created, accepted version manuscript following peer review and may differ slightly from the final published version. The final published version of this work is available at link.springer.com / https://dx.doi.org/10.1007/978-3-319-29198-7_6
Accepted author manuscript, 393 KB

Cite this

@inbook{dcce496cacb149f382697ce3bff4688c,

title = "Intuitionistic decision procedures since Gentzen",

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

author = "Roy Dyckhoff",

year = "2016",

month = may,

day = "5",

doi = "10.1007/978-3-319-29198-7_6",

language = "English",

isbn = "9783319291963",

series = "Progress in Computer Science and Applied Logic",

publisher = "Birkh{\"a}user Basel",

pages = "245--267",

editor = "R Kahle and Th Strahm and Th Studer",

booktitle = "Advances in Proof Theory",

note = "apt13 Advances in Proof Theory ; Conference date: 13-12-2013 Through 14-12-2013",

url = "http://apt13.unibe.ch/",

}

TY - CHAP

T1 - Intuitionistic decision procedures since Gentzen

AU - Dyckhoff, Roy

PY - 2016/5/5

Y1 - 2016/5/5

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

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

U2 - 10.1007/978-3-319-29198-7_6

DO - 10.1007/978-3-319-29198-7_6

M3 - Chapter (peer-reviewed)

SN - 9783319291963

T3 - Progress in Computer Science and Applied Logic

SP - 245

EP - 267

BT - Advances in Proof Theory

A2 - Kahle, R

A2 - Strahm, Th

A2 - Studer, Th

PB - Birkhäuser Basel

T2 - apt13 Advances in Proof Theory

Y2 - 13 December 2013 through 14 December 2013

ER -

Intuitionistic decision procedures since Gentzen

Abstract

Publication series

Other

Access to Document

Fingerprint

Cite this