# G4 Prover

### Result of the test for sequent ~X#p(X) <--> X@(~p(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)<-->_5580@(~p(_5580)). Trying to prove with threshold = 0 1 Succeed in proving ~_15900#p(_15900) --> _15900@(~p(_15900)) (1027 msec.) pretty:1 = ------------------------------ Ax bot,p(Y),X@(p(X)->bot) --> bot ------------------------------------ L0->1 p(Y),p(Y)->bot,X@(p(X)->bot) --> bot ------------------------------------ L@ p(Y),X@(p(X)->bot) --> bot -------------------------- R~ X@(p(X)->bot) --> ~p(Y) --------------------------- R@ X@(p(X)->bot) --> X@(~p(X)) --------------------------- L#-> X#p(X)->bot --> X@(~p(X)) ------------------------- L~def ~X#p(X) --> X@(~p(X)) Trying to prove with threshold = 0 Succeed in proving _15900@(~p(_15900)) --> ~_15900#p(_15900) (1 msec.) pretty:2 = ------------------ Ax bot,X#p(X) --> bot -------------------------- L0->1 X#p(X),X#p(X)->bot --> bot -------------------------- L~def X#p(X),~X#p(X) --> bot ------------------------ L~def X#p(X),X@(~p(X)) --> bot ------------------------ R~ X@(~p(X)) --> ~X#p(X) yes fol(g4i)> quit. yes Exit from Sequent Calculus Prover... Total CPU time = 1033 msec. true