proposition v1.0.3

Usage

$ node main.js "<Proposition>"

BNF of Proposition

    <Proposition>::= <Premise>? "|-" <Imply>
    <Premise>    ::= <Imply> ("," <Imply>)*
    <Imply>      ::= <Or> ("->" <Or>)*
    <Or>         ::= <And> ("+" <And>)*
    <And>        ::= <Atom> ("*" <Atom>)*
    <Atom>       ::= [A-Z] | "(" <Imply> ")"

Axiom

Primal:
    1) (A->(B->A))
    2) ((A->(B->C))->((A->B)->(A->C)))
Minimal:
    3) ((A*B)->A)
    4) ((A*B)->B)
    5) (A->(B->(A*B)))
    6) (A->(A+B))
    7) (B->(A+B))
    8) ((A->C)->((B->C)->((A+B)->C)))
Intuitionistic:
    9) (F->A)
Classical:
   10) (((A->F)->A)->A)

Theorem

    |- (A->A)

Rule of Inference

     A, A->B
    ---------
        B