Metadata-Version: 2.1
Name: mathesis
Version: 0.5.1
Summary: Formal logic library in Python for humans
Home-page: https://mathesis.readthedocs.io/
License: MIT
Keywords: logic,semantics,proof,philosophy
Author: Kentaro Ozeki
Author-email: 32771324+ozekik@users.noreply.github.com
Requires-Python: >=3.9,<4.0
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Requires-Dist: anytree (>=2.8.0,<3.0.0)
Requires-Dist: lark (>=1.1.2,<2.0.0)
Requires-Dist: prettytable (>=3.3.0,<4.0.0)
Project-URL: Repository, https://github.com/ozekik/mathesis
Description-Content-Type: text/markdown

# Mathesis

[![PyPI](https://img.shields.io/pypi/v/mathesis.svg)](https://pypi.org/project/mathesis/)
[![Documentation Status](https://readthedocs.org/projects/mathesis/badge/?version=latest)](http://mathesis.readthedocs.io/en/latest/?badge=latest)
<!-- [![PyPI downloads](https://img.shields.io/pypi/dm/mathesis.svg)](https://pypistats.org/packages/mathesis) -->

[Mathesis](//github.com/ozekik/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

```bash
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)
    * [x] Unsigned tableaux
    * [x] Signed tableaux
- **Hilbert systems**
    * [ ] Hilbert systems
- **Natural deduction**
    * [x] Generic natural deduction
    * [x] Gentzen-style natural deduction (Output)
    * [ ] Fitch-style natural deduction
- **Sequent calculi** (Gentzen-style sequent calculi)
    - [x] Two-sided sequent calculi
    - [ ] Hilbert systems in sequent calculus
    - [ ] Natural deduction in sequent calculus

### Semantics

- [x] Truth tables
- [x] Set-theoretic models
- [ ] Possible world semantics (Kripke semantics)
- [ ] Algebraic semantics
- [ ] Game-theoretic semantics
- [ ] Category-theoretic semantics

## Internals

- Parsing with [lark](https://github.com/lark-parser/lark)
- Trees with [anytree](https://github.com/c0fec0de/anytree)

## Todos

- [ ] Add tests
- [ ] Hilbert systems
- [x] Natural deduction
- [ ] Boolean algebra
- [ ] Type theory
- [ ] Metatheorems
- [ ] Output graphical representations of models
- [ ] Support tptp syntax

