Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs

Thomas Powell

doi:10.1007/978-3-030-20447-1_14

Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs

Thomas Powell

Technische Universität Darmstadt

Research output: Chapter or section in a book/report/conference proceeding › Chapter or section

1 Citation (SciVal)

Abstract

The problem of giving a computational meaning to classical reasoning lies at the heart of logic. This article surveys three famous solutions to this problem – the epsilon calculus, modified realizability and the Dialectica interpretation – and re-examines them from a modern perspective, with a particular emphasis on connections with algorithms and programming.

Original language	English
Title of host publication	Mathesis Universalis, Computability and Proof
Editors	Stefania Centrone, Sara Negri, Deniz Sarikaya, Peter M. Schuster
Publisher	Springer International Publishing
Pages	255-290
ISBN (Electronic)	978-3-030-20447-1
ISBN (Print)	978-3-030-20446-4
DOIs	https://doi.org/10.1007/978-3-030-20447-1_14
Publication status	Published - 2019

Publication series

Name	Synthese Library
Volume	412

Access to Document

10.1007/978-3-030-20447-1_14

http://link.springer.com/10.1007/978-3-030-20447-1_14

Cite this

Powell, T. (2019). Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs. In S. Centrone, S. Negri, D. Sarikaya, & P. M. Schuster (Eds.), Mathesis Universalis, Computability and Proof (pp. 255-290). Article Chapter 14 (Synthese Library; Vol. 412). Springer International Publishing. https://doi.org/10.1007/978-3-030-20447-1_14

Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs. / Powell, Thomas.
Mathesis Universalis, Computability and Proof. ed. / Stefania Centrone; Sara Negri; Deniz Sarikaya; Peter M. Schuster. Springer International Publishing, 2019. p. 255-290 Chapter 14 (Synthese Library; Vol. 412).

Research output: Chapter or section in a book/report/conference proceeding › Chapter or section

@inbook{311dfeb41da144b9b15239e3b1925cdb,

title = "Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs",

abstract = "The problem of giving a computational meaning to classical reasoning lies at the heart of logic. This article surveys three famous solutions to this problem – the epsilon calculus, modified realizability and the Dialectica interpretation – and re-examines them from a modern perspective, with a particular emphasis on connections with algorithms and programming.",

author = "Thomas Powell",

year = "2019",

doi = "10.1007/978-3-030-20447-1_14",

language = "English",

isbn = "978-3-030-20446-4",

series = "Synthese Library",

publisher = "Springer International Publishing",

pages = "255--290",

editor = "Stefania Centrone and Sara Negri and Deniz Sarikaya and Schuster, {Peter M.}",

booktitle = "Mathesis Universalis, Computability and Proof",

address = "Switzerland",

}

TY - CHAP

T1 - Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs

AU - Powell, Thomas

PY - 2019

Y1 - 2019

N2 - The problem of giving a computational meaning to classical reasoning lies at the heart of logic. This article surveys three famous solutions to this problem – the epsilon calculus, modified realizability and the Dialectica interpretation – and re-examines them from a modern perspective, with a particular emphasis on connections with algorithms and programming.

AB - The problem of giving a computational meaning to classical reasoning lies at the heart of logic. This article surveys three famous solutions to this problem – the epsilon calculus, modified realizability and the Dialectica interpretation – and re-examines them from a modern perspective, with a particular emphasis on connections with algorithms and programming.

U2 - 10.1007/978-3-030-20447-1_14

DO - 10.1007/978-3-030-20447-1_14

M3 - Chapter or section

SN - 978-3-030-20446-4

T3 - Synthese Library

SP - 255

EP - 290

BT - Mathesis Universalis, Computability and Proof

A2 - Centrone, Stefania

A2 - Negri, Sara

A2 - Sarikaya, Deniz

A2 - Schuster, Peter M.

PB - Springer International Publishing

ER -

Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs

Abstract

Publication series

Access to Document

Fingerprint

Cite this