# Mathesis
[](https://pypi.org/project/mathesis/)
[](http://mathesis.readthedocs.io/en/latest/?badge=latest)
<!-- [](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
Raw data
{
"_id": null,
"home_page": "https://mathesis.readthedocs.io/",
"name": "mathesis",
"maintainer": null,
"docs_url": null,
"requires_python": "<4.0,>=3.9",
"maintainer_email": null,
"keywords": "logic, semantics, proof, philosophy",
"author": "Kentaro Ozeki",
"author_email": "32771324+ozekik@users.noreply.github.com",
"download_url": "https://files.pythonhosted.org/packages/ec/df/de83fa677fbd7324ae2580fdf359aee5bd0c18e5b52e63fb6f73e6c04cf4/mathesis-0.5.1.tar.gz",
"platform": null,
"description": "# Mathesis\n\n[](https://pypi.org/project/mathesis/)\n[](http://mathesis.readthedocs.io/en/latest/?badge=latest)\n<!-- [](https://pypistats.org/packages/mathesis) -->\n\n[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.\nIt is particularly well-suited for:\n\n- Students learning logic and educators teaching it\n- Researchers in fields like logic, philosophy, linguistics, computer science, and many others\n\n**Documentation:** <https://mathesis.readthedocs.io/>\n\n## Installation\n\n```bash\npip install mathesis\n```\n\n## Key features\n\n- Interactive theorem proving for humans (proof assistant)\n- Automated reasoning (theorem prover)\n- Define models and check validity of inferences in the models\n- JupyterLab/Jupyter Notebook support\n- Output formulas/proofs in LaTeX\n- Customizable ASCII/Unicode syntax (like `A -> B`, `A \u2192 B`, `A \u2283 B` for the conditional)\n\n## Supported logics\n\n### Propositional logics\n\n- **Classical propositional logic:** Truth table, Tableau, Sequent calculus\n- **Many-valued logics:** Truth table\n- **Intuitionistic logic:** Sequent calculus\n\n#### In Progress\n\n- Modal logics\n- Fuzzy logics\n- Substructural logics\n- Epistemic, doxastic, deontic logics\n- Temporal logics\n\n### First-order logics (quantified, predicate logics)\n\n- **Classical first-order logic:** Tableau, Set-theoretic model\n\n#### In Progress\n\n- Many-valued logics\n- Modal logics\n- Intuitionistic logic\n- Fuzzy logics\n- Substructural logics\n- Higher-order logics\n\n## Development status\n\n### Proof theories\n\n- **Tableaux** (semantic tableaux, analytic tableaux)\n * [x] Unsigned tableaux\n * [x] Signed tableaux\n- **Hilbert systems**\n * [ ] Hilbert systems\n- **Natural deduction**\n * [x] Generic natural deduction\n * [x] Gentzen-style natural deduction (Output)\n * [ ] Fitch-style natural deduction\n- **Sequent calculi** (Gentzen-style sequent calculi)\n - [x] Two-sided sequent calculi\n - [ ] Hilbert systems in sequent calculus\n - [ ] Natural deduction in sequent calculus\n\n### Semantics\n\n- [x] Truth tables\n- [x] Set-theoretic models\n- [ ] Possible world semantics (Kripke semantics)\n- [ ] Algebraic semantics\n- [ ] Game-theoretic semantics\n- [ ] Category-theoretic semantics\n\n## Internals\n\n- Parsing with [lark](https://github.com/lark-parser/lark)\n- Trees with [anytree](https://github.com/c0fec0de/anytree)\n\n## Todos\n\n- [ ] Add tests\n- [ ] Hilbert systems\n- [x] Natural deduction\n- [ ] Boolean algebra\n- [ ] Type theory\n- [ ] Metatheorems\n- [ ] Output graphical representations of models\n- [ ] Support tptp syntax\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "Formal logic library in Python for humans",
"version": "0.5.1",
"project_urls": {
"Homepage": "https://mathesis.readthedocs.io/",
"Repository": "https://github.com/ozekik/mathesis"
},
"split_keywords": [
"logic",
" semantics",
" proof",
" philosophy"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "d012a5b769f1f5efe7b8f3bfdc2c99e624abdef3b7ba5830f2f6db56fc97ff84",
"md5": "d249d9c0babeb9f6f2594eaf05c5b369",
"sha256": "9c75d3d1dd2ae2a043c615e953a1f6f3b0fd5139ec0090ef4141fe7ff0c075fc"
},
"downloads": -1,
"filename": "mathesis-0.5.1-py3-none-any.whl",
"has_sig": false,
"md5_digest": "d249d9c0babeb9f6f2594eaf05c5b369",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": "<4.0,>=3.9",
"size": 28023,
"upload_time": "2024-04-23T17:33:27",
"upload_time_iso_8601": "2024-04-23T17:33:27.356828Z",
"url": "https://files.pythonhosted.org/packages/d0/12/a5b769f1f5efe7b8f3bfdc2c99e624abdef3b7ba5830f2f6db56fc97ff84/mathesis-0.5.1-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "ecdfde83fa677fbd7324ae2580fdf359aee5bd0c18e5b52e63fb6f73e6c04cf4",
"md5": "ba101e26d1b78904bb6ca6e82c746aa1",
"sha256": "faec26c2f08e26e5429be17073490875065e8269efb336d9dde4e7d1a64c3ac2"
},
"downloads": -1,
"filename": "mathesis-0.5.1.tar.gz",
"has_sig": false,
"md5_digest": "ba101e26d1b78904bb6ca6e82c746aa1",
"packagetype": "sdist",
"python_version": "source",
"requires_python": "<4.0,>=3.9",
"size": 19329,
"upload_time": "2024-04-23T17:33:29",
"upload_time_iso_8601": "2024-04-23T17:33:29.182716Z",
"url": "https://files.pythonhosted.org/packages/ec/df/de83fa677fbd7324ae2580fdf359aee5bd0c18e5b52e63fb6f73e6c04cf4/mathesis-0.5.1.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-04-23 17:33:29",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "ozekik",
"github_project": "mathesis",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "mathesis"
}
JSON
