@inbook{96bbc64713a34a62a2dd0adf33d8d218,
title = "Cut-elimination, substitution and normalisation",
abstract = "We present a proof (of the main parts of which there is a formal version, checked with the Isabelle proof assistant) that, for a G3-style calculus covering all of intuitionistic zero-order logic, with an associated term calculus, and with a particular strongly normalising and confluent system of cut-reduction rules, every reduction step has, as its natural deduction translation, a sequence of zero or more reduction steps (detour reductions, permutation reductions or simplifications). This complements and (we believe) clarifies earlier work by (e.g.) Zucker and Pottinger on a question raised in 1971 by Kreisel.",
keywords = "Intuitionistic logic, Minimal logic, Sequent calculus, Natural deduction, Cut-elimination, Substitution, Normalisation",
author = "Roy Dyckhoff",
note = "Date of Acceptance: 01/2015",
year = "2015",
doi = "10.1007/978-3-319-11041-7_7",
language = "English",
isbn = "9783319110400",
series = "Outstanding Contributions to Logic",
publisher = "Springer",
pages = "163--187",
editor = "Heinrich Wansing",
booktitle = "Dag Prawitz on Proofs and Meaning",
address = "Netherlands",
}