Sequent Calculus Prover (seqprover)

?????  (Since April 23, 2003)
Last modified: Wed May 9 16:38:50 2007 JST
  1. Please input a sequent:
    For example, (p->r)/\(q->r) <--> (p\/q)->r
  2. Please select a output style:
    To format LaTeX form output, you need proof.sty by Makoto Tatsuta.
  3. Now, press
    Process spending more than 10 seconds will be killed.
  4. Press to clear input.
  5. Please refer to guide.pdf for notations and inference rules.

Examples

Please follow the link if you want the proof.
  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. p\/(p->q)
  38. ((p->q)->p)->p
  39. 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))
  49. X@p(X) --> X#p(X)
  50. 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)))

Introduction

This small program seqprover.pl (written in SICStus Prolog) searches a cut-free proof of the given sequent of first-order logic. Of course, the proof search of first-order logic is undecidable. Therefore, this program limits the number of quantifier rules (L\forall and R\exists) for each path of the proof at most five. To format LaTeX output, you need proof.sty by Makoto Tatsuta, and please add the following lines to your LaTeX source file. 

\newcommand{\imp}{\supset}
\newcommand{\lra}{\longrightarrow}

Any comments or suggestions are appreciated.

Known Bugs

Related Links

See Linear Logic Prover (llprover) page.
Naoyuki Tamura