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



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)> _5580@(p(_5580)/\q(_5580))<-->_5580@p(_5580)/\_5580@q(_5580).
Trying to prove with threshold = 0 1
Succeed in proving _15658@(p(_15658)/\q(_15658)) --> _15658@p(_15658)/\_15658@q(_15658) (830 msec.)
pretty:1 =
--------------------------------- Ax    --------------------------------- Ax
p(Y),q(Y),X@(p(X)/\q(X)) --> p(Y)       p(Z),q(Z),X@(p(X)/\q(X)) --> q(Z)
---------------------------------- L/\  ---------------------------------- L/\
p(Y)/\q(Y),X@(p(X)/\q(X)) --> p(Y)      p(Z)/\q(Z),X@(p(X)/\q(X)) --> q(Z)
---------------------------------- L@   ---------------------------------- L@
     X@(p(X)/\q(X)) --> p(Y)                 X@(p(X)/\q(X)) --> q(Z)
     ------------------------- R@            ------------------------- R@
     X@(p(X)/\q(X)) --> X@p(X)               X@(p(X)/\q(X)) --> X@q(X)
     ----------------------------------------------------------------- R/\
                     X@(p(X)/\q(X)) --> X@p(X)/\X@q(X)
Trying to prove with threshold = 0 1
Succeed in proving _15658@p(_15658)/\_15658@q(_15658) --> _15658@(p(_15658)/\q(_15658)) (2510 msec.)
pretty:2 =
--------------------------- Ax  --------------------------- Ax
p(Y),X@p(X),X@q(X) --> p(Y)     X@p(X),q(Y),X@q(X) --> q(Y)
--------------------------- L@  --------------------------- L@
  X@p(X),X@q(X) --> p(Y)          X@p(X),X@q(X) --> q(Y)
  ------------------------------------------------------ R/\
               X@p(X),X@q(X) --> p(Y)/\q(Y)
               -------------------------------- R@
               X@p(X),X@q(X) --> X@(p(X)/\q(X))
               --------------------------------- L/\
               X@p(X)/\X@q(X) --> X@(p(X)/\q(X))
yes
fol(g4i)> quit.
yes
Exit from Sequent Calculus Prover...
Total CPU time = 3347 msec.
true 


  

Back to g4-prover
   
Maintained by  Joseph Vidal-Rosset