Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

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

# Proved in 0 msec.

Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura