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