Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

--------- Ax   --------- Ax
p,p --> p      p --> q,p
---------- R~  ---------- L~   --------- Ax   --------- Ax
p --> ~p,p     p,~q --> p      p,q --> p      q --> q,p
------------------------- L->  ---------- R~  ---------- L~
     p,~p-> ~q --> p           q --> ~p,p     q,~q --> p
     ---------------- R~       ------------------------- L->
     ~p-> ~q --> ~p,p               q,~p-> ~q --> p
     ---------------------------------------------- L->
                  ~p->q,~p-> ~q --> p
                  ---------------------- R->
                  ~p-> ~q --> (~p->q)->p
                  -------------------------- R->
                   --> (~p-> ~q)->(~p->q)->p

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura