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 _15628#(p(_15628)\/q(_15628)) --> _15628#p(_15628)\/_15628#q(_15628) (3409 msec.)
pretty:1 =
------------- Ax             ------------- Ax
p(Y) --> p(Y)                q(Y) --> q(Y)
--------------- R#           --------------- R#
p(Y) --> X#p(X)              q(Y) --> X#q(X)
----------------------- R\/  ----------------------- R\/
p(Y) --> X#p(X)\/X#q(X)      q(Y) --> X#p(X)\/X#q(X)
---------------------------------------------------- L\/
           p(Y)\/q(Y) --> X#p(X)\/X#q(X)
           --------------------------------- L#
           X#(p(X)\/q(X)) --> X#p(X)\/X#q(X)
Trying to prove with threshold = 0 1
Succeed in proving _15628#p(_15628)\/_15628#q(_15628) --> _15628#(p(_15628)\/q(_15628)) (64 msec.)
pretty:2 =
------------- Ax              ------------- Ax
p(Y) --> p(Y)                 q(Z) --> q(Z)
------------------- R\/       ------------------- R\/
p(Y) --> p(Y)\/q(Y)           q(Z) --> p(Z)\/q(Z)
----------------------- R#    ----------------------- R#
p(Y) --> X#(p(X)\/q(X))       q(Z) --> X#(p(X)\/q(X))
------------------------- L#  ------------------------- L#
X#p(X) --> X#(p(X)\/q(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 = 3480 msec.
true 


  

Back to g4-prover
   
Maintained by  Joseph Vidal-Rosset