Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

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