G4 Prover
    
Result of the test for sequent p/\(q\/r) --> (p\/q)/\(p\/r) 



G4 Prover: a Prolog Prover for Roy Dyckhoff's Sequent Calculus G4
This prover is a fork made by Joseph Vidal-Rosset (joseph.vidal-rosset@gmail.com),
from seqprover.pl, the sequent prover for CL-X, written by Naoyuki Tamura (tamura@kobe-u.ac.jp).
Type "help." if you need some help.
fol(g4i)> fol(g4i).
yes
fol(g4i)> output(pretty).
yes
fol(g4i)> p/\q\/r-->(p\/q)/\p\/r.
Trying to prove with threshold = 0
Succeed in proving p/\q\/r --> (p\/q)/\p\/r (3 msec.)
pretty:1 =
--------- Ax      --------- Ax      --------- Ax      --------- Ax
p,q --> p         p,q --> p         p,r --> p         p,r --> p
------------ R\/  ------------ R\/  ------------ R\/  ------------ R\/
p,q --> p\/q      p,q --> p\/r      p,r --> p\/q      p,r --> p\/r
------------------------------ R/\  ------------------------------ R/\
     p,q --> (p\/q)/\p\/r                p,r --> (p\/q)/\p\/r
     -------------------------------------------------------- L\/
                     p,q\/r --> (p\/q)/\p\/r
                     ------------------------ L/\
                     p/\q\/r --> (p\/q)/\p\/r
yes
fol(g4i)> quit.
yes
Exit from Sequent Calculus Prover...
Total CPU time = 7 msec.
true 


  

Back to g4-prover
   
Maintained by  Joseph Vidal-Rosset