Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

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

# Proved in 0 msec.

Trying to prove with threshold = 0

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

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura