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://digitalformallogic.github.io/mathesis/

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

	Truth Table	Tableau	Natural Deduction	Sequent Calculus
Classical logic	✅	✅	✅	✅
Many-valued logics	✅	-	-	-
Intuitionistic logic	n/a	-	-	✅

In Progress

Modal logics
Fuzzy logics
Substructural logics
Epistemic, doxastic, deontic logics
Temporal logics

First-order logics (quantified, predicate logics)

	Model	Tableau	Natural Deduction	Sequent Calculus
Classical logic	✅	✅	✅	-

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

Parsing with lark
Trees with anytree

Roadmap

Add tests (WIP)
Hilbert systems
Natural deduction
Boolean algebra
Type theory
Metatheorems
Output graphical representations of models
Support tptp syntax

Metadata

Release files for mathesis 0.7.2

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Source distribution (sdist)

Source distribution for mathesis 0.7.2
File	Size	Uploaded
mathesis-0.7.2.tar.gz	22.4 kB	Dec 13, 2025	Details

Built distribution (wheel)

Table of built distributions (wheels) for mathesis 0.7.2
File	Interpreter	ABI	Platform	Reset
mathesis-0.7.2-py3-none-any.whl 34.5 kB Dec 13, 2025	Python 3	none	any	Details

Total release size: 56.9 kB

Release files / mathesis-0.7.2.tar.gz

Download URL	mathesis-0.7.2.tar.gz
Size	22.4 kB
Tags	Source
SHA-256 checksum How to use checksums	`a91c89659d65b23946c4b8cfb20bdce47d8c9f144c181a99144774b6f238d76a`
BLAKE2b-256 checksum How to use checksums	`c93beffeaf3f4011f642f8c7442b6f9b1ad5bd3c09f6dcc7e8699be1c6b35afa`
Upload date	Dec 13, 2025
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`poetry/2.2.0 CPython/3.13.7 Darwin/23.6.0`

Release files / mathesis-0.7.2-py3-none-any.whl

Download URL	mathesis-0.7.2-py3-none-any.whl
Size	34.5 kB
Tags	Python 3
SHA-256 checksum How to use checksums	`3fe9190f853fcefd7c1284d3d47a882c847b290d5654285f8dc3f463d4bea219`
BLAKE2b-256 checksum How to use checksums	`cea830dd68c356cf1ac09d27e934066b88ec6ae51d4050dc0adf37da3e604ddb`
Upload date	Dec 13, 2025
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`poetry/2.2.0 CPython/3.13.7 Darwin/23.6.0`