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 


  

Back to g4-prover
   
Maintained by  Joseph Vidal-Rosset