# Mathesis
[](https://pypi.org/project/mathesis/)
[](https://ozekik.github.io/mathesis/)
<!-- [](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://ozekik.github.io/mathesis/>
## 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
| | 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)
* [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)
## Roadmap
- [ ] 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://ozekik.github.io/mathesis/",
"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/40/24/12e823d242384e84c9de7c21d2c6cd66fc9a2b22f08d56f0d136a187b163/mathesis-0.5.3.tar.gz",
"platform": null,
"description": "# Mathesis\n\n[](https://pypi.org/project/mathesis/)\n[](https://ozekik.github.io/mathesis/)\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://ozekik.github.io/mathesis/>\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| | Truth Table | Tableau | Natural Deduction | Sequent Calculus |\n|---:|:---:|:---:|:---:|:---:|\n| Classical logic | \u2705 | \u2705 | \u2705 | \u2705 |\n| Many-valued logics | \u2705 | - | - | - |\n| Intuitionistic logic | n/a | - | - | \u2705 |\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| | Model | Tableau | Natural Deduction | Sequent Calculus |\n|---:|:---:|:---:|:---:|:---:|\n| Classical logic | \u2705 | \u2705 | - | - |\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## Roadmap\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.3",
"project_urls": {
"Homepage": "https://ozekik.github.io/mathesis/",
"Repository": "https://github.com/ozekik/mathesis"
},
"split_keywords": [
"logic",
" semantics",
" proof",
" philosophy"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "f298b70d148f5f1faa7daadee0a13372fdbb79d6b494939797fff156c128e217",
"md5": "4a3d7cece3997d2d89bb1e356fc99abe",
"sha256": "2083813f759156c6887b3da706470384bce82c8c0944cfba26d4cff64bcaddda"
},
"downloads": -1,
"filename": "mathesis-0.5.3-py3-none-any.whl",
"has_sig": false,
"md5_digest": "4a3d7cece3997d2d89bb1e356fc99abe",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": "<4.0,>=3.9",
"size": 31648,
"upload_time": "2024-07-18T17:33:38",
"upload_time_iso_8601": "2024-07-18T17:33:38.245471Z",
"url": "https://files.pythonhosted.org/packages/f2/98/b70d148f5f1faa7daadee0a13372fdbb79d6b494939797fff156c128e217/mathesis-0.5.3-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "402412e823d242384e84c9de7c21d2c6cd66fc9a2b22f08d56f0d136a187b163",
"md5": "ae6ae213ae51d6a2b8198e38339401f7",
"sha256": "67a0d844828d8668b2b63d7aca6a5f9abcfd8c9bdb12691c79fe32bc438543b5"
},
"downloads": -1,
"filename": "mathesis-0.5.3.tar.gz",
"has_sig": false,
"md5_digest": "ae6ae213ae51d6a2b8198e38339401f7",
"packagetype": "sdist",
"python_version": "source",
"requires_python": "<4.0,>=3.9",
"size": 21966,
"upload_time": "2024-07-18T17:33:39",
"upload_time_iso_8601": "2024-07-18T17:33:39.792917Z",
"url": "https://files.pythonhosted.org/packages/40/24/12e823d242384e84c9de7c21d2c6cd66fc9a2b22f08d56f0d136a187b163/mathesis-0.5.3.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-07-18 17:33:39",
"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
