Formal logic library in Python for humans
Project description
Mathesis
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://mathesis.readthedocs.io/
Installation
pip install mathesis
Key features
- 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 ⊃ B
for the conditional)
Supported logics
Propositional logics
- Classical propositional logic: Truth table, Tableau, Sequent calculus
- Many-valued logics: Truth table
- Intuitionistic logic: Sequent calculus
In Progress
- Modal logics
- Fuzzy logics
- Substructural logics
- Epistemic, doxastic, deontic logics
- Temporal logics
First-order logics (quantified, predicate logics)
- Classical first-order logic: Tableau, Set-theoretic model
In Progress
- 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
- 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
Semantics
- Truth tables
- Set-theoretic models
- Possible world semantics (Kripke semantics)
- Algebraic semantics
- Game-theoretic semantics
- Category-theoretic semantics
Internals
Todos
- Add tests
- Hilbert systems
- Natural deduction
- Boolean algebra
- Type theory
- Metatheorems
- Output graphical representations of models
- Support tptp syntax
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.5.1.tar.gz
(19.3 kB
view hashes)
Built Distribution
mathesis-0.5.1-py3-none-any.whl
(28.0 kB
view hashes)