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 --> ~p,q
     -------------- R\/
     p->q --> ~p\/q

# Proved in 0 msec.

Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura