Metadata-Version: 2.1
Name: proofproposition
Version: 0.0.1
Summary: Proposition Logic
Home-page: https://github.com/HappyMayzhang/proofproposition
Author: may.xiaoya.zhang
Author-email: may.xiaoya.zhang@gmail.com
Classifier: Programming Language :: Python :: 3
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Requires-Python: >=3.11.3
Description-Content-Type: text/markdown
Requires-Dist: TatSu>=5.12.0

# Install
`$ pip3 install -U proofproposition`

# Description
```
### BNF of Proposition:
    Expr
        = [Premise] '|-' Imply
        ;
    Premise
        = Imply {',' Imply}*
        ;
    Imply
        = Or {'->' Or}*
        ;
    Or
        = And {'+' And}*
        ;
    And
        = Atom {'*' Atom}*
        ;
    Atom
        = token
        | '(' Imply ')'
        ;
    token
        = /\w+/
        ;

### Axiom of Primal:
    1) A->(B->A)
    2) (A->(B->C))->((A->B)->(A->C))

### Axiom of 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))

### Axiom of Intuitionistic:
    9) False->A

### Axiom of Classical:
   10) ((A->False)->A)->A

### Theorem:
    |- A->A

### Rule of Inference:
     A, A->B
    ---------
        B
```

# Command
`$ proof "A |- B->A"`

# Contact us
<may.xiaoya.zhang@gmail.com>
