Yet Another Bijection Between Sequent Calculus and Natural Deduction
Author(s) -
Cecília Englander,
Gilles Dowek,
Edward Hermann Hæusler
Publication year - 2015
Publication title -
electronic notes in theoretical computer science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.242
H-Index - 60
ISSN - 1571-0661
DOI - 10.1016/j.entcs.2015.04.007
Subject(s) - natural deduction , sequent calculus , sequent , cut elimination theorem , bijection , calculus (dental) , mathematics , curry–howard correspondence , algebra over a field , proof calculus , discrete mathematics , pure mathematics , medicine , mathematical proof , geometry , dentistry
This work shows a bijection between sequent calculus and natural deduction for intuitionistic propositional logic so far as normal and cut-free derivations are concerned
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom