This is an web interface for a g3*p-based prover written by
Enrico Tassi and
Stefano Zacchiroli
to play with the g3*p calculus during the course
of advanced logic / demonstration theory.
For more infos look at the
course page.
There are some handouts
too.
Here you can find the sources of the prover released under GPL.
The syntax is the following one:
An example of a valid sequent is:
a -> b, (b /\ a) -> c => a -> c
You can choose both pdf and tex format, but for compiling the tex you need bussproof.sty