g3*p

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.

Instructions & Syntax

The syntax is the following one:

not

!

or

\/ (note, these are a \ and a / not an uppercase V)

and

/\ (the same note for the or, these are slashes)

implies

->

absurd

_|_

iff

<->

variables

a..z

formulae separator

,

sequent

=>

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

Try it