Permutability of Proofs in Intuitionistic Sequent Calculi

Roy Dyckhoff, L Pinto

Research output: Contribution to journalArticlepeer-review

26 Citations (Scopus)

Abstract

We prove a folklore theorem, that two derivations in a cut-free sequent calculus for intuitionistic propositional logic (based on Kleene's G3) are inter-permutable (using a set of basic "permutation reduction rules" derived from Kleene's work in 1952) iff they determine the same natural deduction. The basic rules form a confluent and weakly normalising rewriting system. We refer to Schwichtenberg's proof elsewhere that a modification of this system is strongly normalising. (C) 1999-Elsevier Science B.V. All rights reserved.

Original languageEnglish
Pages (from-to)141-155
Number of pages15
JournalTheoretical Computer Science
Volume212
Issue number1-2
DOIs
Publication statusPublished - 6 Feb 1999

Keywords

  • intuitionistic logic
  • proof theory
  • natural deduction
  • sequent calculus
  • LOGIC

Fingerprint

Dive into the research topics of 'Permutability of Proofs in Intuitionistic Sequent Calculi'. Together they form a unique fingerprint.

Cite this