Computational isomorphisms in classical logic

Vincent Danos, Jean-Baptiste Joinet, Harold Schellinx

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

All standard ‘linear’ boolean equations are shown to be computationally realized within a suitable classical sequent calculus . Specifically, can be equipped with a cut-elimination compatible equivalence on derivations based upon reversibility properties of logical rules. So that any pair of derivations, without structural rules, of F⇒G and G⇒F, where F,G are first-order formulas ‘without any qualities’, defines a computational isomorphism.
Original languageEnglish
Pages (from-to)353 - 378
Number of pages26
JournalTheoretical Computer Science
Issue number3
Publication statusPublished - Feb 2003

Keywords / Materials (for Non-textual outputs)

  • Classical logic
  • Proof theory
  • Linear logic


Dive into the research topics of 'Computational isomorphisms in classical logic'. Together they form a unique fingerprint.

Cite this