pesca: Proof Editor for Sequent Calculus

[ compilers-interpreters, program, theorem-provers ] [ Propose Tags ]

Pesca is a program that helps in the construction of proofs in sequent calculus. It works both as a proof editor and as an automatic theorem prover. Proofs constructed in Pesca can both be seen on the terminal and printed into LaTeX files.

The user of Pesca can choose among different versions of classical and intuitionistic proposition and predicate calculi, and extend them by systems of nonlogical axioms. The implementation of Pesca is written in the functional programming language Haskell.

[Skip to Readme]

Downloads

pesca-4.0.1.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

Package maintainers

GwernBranwen, dpeteler

For package maintainers and hackage trustees

edit package information

Candidates

No Candidates

Versions [RSS]	4, 4.0.1
Dependencies	base (>3), process [details]
License	LicenseRef-GPL
Author	Aarne Ranta
Maintainer	Aarne Ranta <http://www.cs.chalmers.se/~aarne/>
Category	Theorem Provers, Compilers/Interpreters
Home page	http://www.cs.chalmers.se/~aarne/pesca/
Uploaded	by GwernBranwen at 2008-05-20T20:12:01Z
Distributions	NixOS:4.0.1
Reverse Dependencies	1 direct, 0 indirect [details]
Executables	pesca
Downloads	2078 total (14 in the last 30 days)
Rating	(no votes yet) [estimated by Bayesian average]
Your Rating	λ λ λ
Status	Docs not available [build log] All reported builds failed as of 2017-01-03 [all 8 reports]

Readme for pesca-4.0.1

[back to package description]

PESCA = Proof Editor for Sequent Calculus

(Companion to the book Structural Proof Theory by Sara Negri and Jan von Plato,
to appear at Cambridge University Press)

(c) Aarne Ranta 24/3/2000.

To run under Unix, type

  ./pesca

To the PESCA prompt |-, type

  ?

to see the available commands, or

  m

to see the manual (the latter assumes latex and xdvi are on your path).

The pesca shell script assumes the Haskell interpreter hugs is on your path.
You can also compile the Haskell source code by hbc or ghc; the Main module is
in the file Editor.hs.

http://www.cs.chalmers.se/~aarne/pesca/