G4 Prover
    
Result of the test for sequent p\/(q\/r) <--> (p\/q)\/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)\/r.
Trying to prove with threshold = 0
Succeed in proving p\/q\/r --> (p\/q)\/r (5 msec.)
pretty:1 =
                     ------- Ax
                     q --> q
------- Ax           ---------- R\/       ------- Ax
p --> p              q --> p\/q           r --> r
---------- R\/       --------------- R\/  --------------- R\/
p --> p\/q           q --> (p\/q)\/r      r --> (p\/q)\/r
--------------- R\/  ------------------------------------ L\/
p --> (p\/q)\/r               q\/r --> (p\/q)\/r
------------------------------------------------ L\/
             p\/q\/r --> (p\/q)\/r
Trying to prove with threshold = 0
Succeed in proving (p\/q)\/r --> p\/q\/r (4 msec.)
pretty:2 =
                   ------- Ax
                   q --> q
------- Ax         ---------- R\/     ------- Ax
p --> p            q --> q\/r         r --> r
------------- R\/  ------------- R\/  ---------- R\/
p --> p\/q\/r      q --> p\/q\/r      r --> q\/r
-------------------------------- L\/  ------------- R\/
        p\/q --> p\/q\/r              r --> p\/q\/r
        ------------------------------------------- L\/
                   (p\/q)\/r --> p\/q\/r
yes
fol(g4i)> quit.
yes
Exit from Sequent Calculus Prover...
Total CPU time = 13 msec.
true 


  

Back to g4-prover
   
Maintained by  Joseph Vidal-Rosset