© 2003 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Original Article |
Proof Nets for Classical Logic
Department of Computer Science, Queen Mary, University of London, London E1 4NS, UK. E-mail: E.P.Robinson{at}dcs.qmul.ac.uk
This paper introduces a notion of proof net for classical logic, provides a static correctness condition for these nets, and analyses theconnection between nets and conventional sequent calculus. The main surprise of the paper is that there are no surprises at the static level. Subsequent work reveals that there are few at the dynamic either.
Keywords: Classical logic, sequent calculus, proof nets.
Received 5 February 2002.