Mathesis is a human-friendly Python library for computational formal logic (including mathematical, symbolic, philosophical logic), formal semantics, and theorem proving. It is particularly well-suited for:
- Students learning logic and educators teaching it
- Researchers in fields like logic, philosophy, linguistics, computer science, and many others
Documentation: https://ozekik.github.io/mathesis/
pip install mathesis- Interactive theorem proving for humans (proof assistant)
- Automated reasoning (theorem prover)
- Define models and check validity of inferences in the models
- JupyterLab/Jupyter Notebook support
- Output formulas/proofs in LaTeX
- Customizable ASCII/Unicode syntax (like
A -> B,A → B,A ⊃ Bfor the conditional)
| Truth Table | Tableau | Natural Deduction | Sequent Calculus | |
|---|---|---|---|---|
| Classical logic | ✅ | ✅ | ✅ | ✅ |
| Many-valued logics | ✅ | - | - | - |
| Intuitionistic logic | n/a | - | - | ✅ |
- Modal logics
- Fuzzy logics
- Substructural logics
- Epistemic, doxastic, deontic logics
- Temporal logics
| Model | Tableau | Natural Deduction | Sequent Calculus | |
|---|---|---|---|---|
| Classical logic | ✅ | ✅ | - | - |
- Many-valued logics
- Modal logics
- Intuitionistic logic
- Fuzzy logics
- Substructural logics
- Higher-order logics
- Tableaux (semantic tableaux, analytic tableaux)
- Unsigned tableaux
- Signed tableaux
- Hilbert systems
- Hilbert systems
- Natural deduction
- Generic natural deduction
- Gentzen-style natural deduction (Output)
- Fitch-style natural deduction
- Sequent calculi (Gentzen-style sequent calculi)
- Two-sided sequent calculi
- Hilbert systems in sequent calculus
- Natural deduction in sequent calculus
- Truth tables
- Set-theoretic models
- Possible world semantics (Kripke semantics)
- Algebraic semantics
- Game-theoretic semantics
- Category-theoretic semantics
- Add tests
- Hilbert systems
- Natural deduction
- Boolean algebra
- Type theory
- Metatheorems
- Output graphical representations of models
- Support tptp syntax