PESCA - a Proof Editor for Sequent Calculus

Companion to the book Structural Proof Theory by Sara Negri and Jan von Plato, Cambridge University Press, 2001 (paperback edition 2008).


13/5/2008 Pesca sources made available in hackage by Gwern Branwen.

9/4/2003 PESCA*, an extension of PESCA by Gyrd Brændeland. PESCA* implements a mechanical proof search in elementary number theory, using cuts, which are not present in plain PESCA.

1/11/2002. PESCA ported to the Zaurus PDA. See here.

24/11/2000. Fixed some more problems detected by Roy Dyckhoff. As suggested by him, added the command w, which shows the current proof tree together with the subnode numbering. Added a SunOS binary compiled by hbc.

14/11/2000. Fixed a problem detected by Roy Dyckhoff, due to an inefficiency in PSequent.pFormula. At the same time, corrected an error in the natural deduction translation of the L-> rule in Natural.proof2natproof, as well as a bug in naming my*.tex files, which created double suffixes.

Program and documentation can be downloaded here.

A Sun binary is now available.

Comments, contributions, and bug reports can be sent to the author, Aarne Ranta.