Formal logic library in Python for humans
Project description
Mathesis
Mathesis is a formal logic/semantics/theorem proving library in Python, for humans. It is suitable for, for example:
- Students who learn logic and teachers who teach logic,
- Researchers in logic, philosophy, linguistics, computer sciences, etc.
Documentation: https://mathesis.readthedocs.io/
Key features
- Interactive theorem proving for humans (proof assistant)
- Automated theorem proving (automated reasoning)
- Define models and check validity of inferences in the models
- JupyterLab/Jupyter Notebook support
- Output formulas/proofs in LaTeX
- Customizable ASCII/Unicode syntax (e.g.
A -> B
orA → B
;A → B
and/orA ⊃ B
)
Supported logics
Propositional logics
- Classical propositional logic
- Tableaux, Sequent calculi
- Truth tables
- Many-valued logics
- Truth tables
- Modal logics
- Intuitionistic logic
- Fuzzy logics
- Substructural logics
Quantified logics (first-order or predicate logics)
- Classical first-order logic
- Many-valued logics
- Modal logics
- Intuitionistic logic
- Fuzzy logics
- Substructural logics
- Higher-order logics
Development status
Proof theories
- Tableaux (semantic tableaux, analytic tableaux)
- Unsigned tableaux
- Signed tableaux
- Hilbert systems
- Hilbert systems
- Natural deduction
- Gentzen-style natural deduction
- Fitch-style natural deduction
- Sequent calculi (Gentzen-style sequent calculi)
- Two-sided sequent calculi
- Hilbert systems in sequent calculi
- Natural deduction in sequent calculi
Semantics
- Truth tables
- Set-theoretic models
- Possible world semantics (Kripke semantics)
- Algebraic semantics
- Game-theoretic semantics
- Category-theoretic semantics
Internals
Todos
- Hilbert systems
- Natural deduction
- Boolean algebra
- Type theory
- Metatheorems
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
mathesis-0.1.1.tar.gz
(12.8 kB
view hashes)
Built Distribution
mathesis-0.1.1-py3-none-any.whl
(18.0 kB
view hashes)