Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

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

# Proved in 0 msec.

Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura