1. Please input a sequent in first order logic
    For example, (p-> r)/\(q-> r) <--> (p\/q)-> r or X#p(X)\/X#q(X) --> X#(p(X)\/q(X))
  2. By default the prover is in intuitionistic logic, but you can choose another logic:
  3. Please select a output style:
  4. Now, press or
If you are looking for a sequent calculus prover for first-order classical logic (LK), please check Sequent Prover (seqprover).

Examples

All the following examples are valid in classical logic. When the prover fails in proving one of these formulas below, it means that this formula is not intuitionistically valid. Then, you can test its validity in G4c in the prover above and compare the ouput with the result provided by Naoyuki Tamura's prover.
  1. p/\top <--> p
  2. p\/bot <--> p
  3. p/\bot <--> bot
  4. p\/top <--> top
  5. p/\p <--> p
  6. p\/p <--> p
  7. p/\q <--> q/\p
  8. p\/q <--> q\/p
  9. p/\q --> p
  10. p/\q --> q
  11. p --> p\/q
  12. q --> p\/q
  13. p/\(q/\r) <--> (p/\q)/\r
  14. p\/(q\/r) <--> (p\/q)\/r
  15. p/\(q\/r) <--> (p/\q)\/(p/\r)
  16. p\/(q/\r) <--> (p\/q)/\(p\/r)
  17. p/\(q\/r) --> (p\/q)/\(p\/r)
  18. (p/\q)\/(p/\r) --> p\/(q/\r)
  19. ~ ~ p <--> p
  20. p/\ ~p <--> bot
  21. p\/ ~p <--> top
  22. ~(p/\q) <--> ~p\/ ~q
  23. ~(p\/q) <--> ~p/\ ~q
  24. p-> q <--> ~p\/q
  25. ~p <--> p-> bot
  26. p-> q <--> ~q-> ~p
  27. p-> q-> r <--> q-> p-> r
  28. p-> q-> r <--> (p/\q)-> r
  29. (p-> q)/\(p-> r) <--> p-> q/\r
  30. (p-> r)/\(q-> r) <--> (p\/q)-> r
  31. p-> q, q-> r --> p-> r
  32. p --> (q-> p)
  33. (p-> (q-> r))--> (p-> q)-> (p-> r)
  34. p-> ~q --> (p-> q)-> ~p
  35. ~p-> ~q --> (~p-> q)-> p
  36. p/\(p-> q)/\(p/\q-> s)--> s
  37. top --> p\/(p-> q)
  38. ((p-> q)-> p)--> p
  39. top-->X@p(X)-> p(a)/\p(b)
  40. p(a)\/p(b) --> X#p(X)
  41. X@X@p(X) <--> X@p(X)
  42. X#X#p(X) <--> X#p(X)
  43. X@(p(X)/\q(X)) <--> X@p(X) /\ X@q(X)
  44. X#(p(X)\/q(X)) <--> X#p(X) \/ X#q(X)
  45. ~X@p(X) <--> X#(~p(X))
  46. ~X#p(X) <--> X@(~p(X))
  47. ~X@(p(X)-> q(X)) <--> X#(p(X)/\ ~q(X))
  48. ~X#(p(X)/\q(X)) <--> X@(p(X)-> ~q(X)) SLOW!
  49. X@p(X) --> X#p(X)
  50. top --> Y#X@(p(X)->p(Y))
  51. X#Y@p(X,Y) --> Y@X#p(X,Y)
  52. (p(a)/\p(b)-> q)-> X#(p(X)-> q)
  53. n(0), X@(n(X)-> n(s(X))) --> n(s(s(0)))