Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

------- Ax
p --> p
----------- Rbot
p --> p,bot
------------- R->
 --> p,p->bot
------------- L~
~p --> p->bot

# Proved in 0 msec.

Trying to prove with threshold = 0

------- Ax  ---------- Lbot
p --> p     p,bot --> 
---------------------- L->
    p,p->bot --> 
    ------------- R~
    p->bot --> ~p

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura