# ND-Prover
An interactive Fitch-style natural deduction proof checker, implemented in Python.
Supports propositional, first-order, and modal logics (K, T, S4, S5) via a command-line interface.
## Logic Checklist
- [x] Propositional logic (TFL)
- [x] First-order logic (FOL)
- [x] Modal logic K (MLK)
- [x] Modal logic T (MLT)
- [x] Modal logic S4 (MLS4)
- [x] Modal logic S5 (MLS5)
## Example Usage
```
$ python -m nd_prover
Select logic (TFL, FOL, MLK, MLT, MLS4, MLS5): TFL
Enter premises (separated by "," or ";"): P -> Q, P
Enter conclusion: Q
1 | P → Q PR
2 | P PR
|---
1 - Add a new line
2 - Begin a new subproof
3 - End the current subproof
4 - End the current subproof and begin a new one
5 - Delete the last line
Select action: 1
Enter line: Q ; ->E, 1,2
1 | P → Q PR
2 | P PR
|---
3 | Q →E, 1,2
Proof complete! 🎉
```
A proof of the law of excluded middle (LEM) using ND-Prover:
```
Proof of ∴ P ∨ ¬P
------------------
1 | | ¬(P ∨ ¬P) AS
| |-----------
2 | | | P AS
| | |---
3 | | | P ∨ ¬P ∨I, 2
4 | | | ⊥ ¬E, 1,3
5 | | ¬P ¬I, 2-4
6 | | P ∨ ¬P ∨I, 5
7 | | ⊥ ¬E, 1,6
8 | P ∨ ¬P IP, 1-7
Proof complete! 🎉
```
A proof that identity is symmetric:
```
Proof of ∴ ∀x∀y(x = y → y = x)
-------------------------------
1 | | a = b AS
| |-------
2 | | a = a =I
3 | | b = a =E, 1,2
4 | a = b → b = a →I, 1-3
5 | ∀y(a = y → y = a) ∀I, 4
6 | ∀x∀y(x = y → y = x) ∀I, 5
Proof complete! 🎉
```
A proof in modal logic S5:
```
Proof of ♢□A ∴ □A
-----------------
1 | ♢□A PR
|-----
2 | ¬□¬□A Def♢, 1
3 | | ¬□A AS
| |-----
4 | | | □ AS
| | |---
5 | | | ¬□A R5, 3
6 | | □¬□A □I, 4-5
7 | | ⊥ ¬E, 2,6
8 | □A IP, 3-7
Proof complete! 🎉
```
Raw data
{
"_id": null,
"home_page": null,
"name": "nd-prover",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.10",
"maintainer_email": null,
"keywords": "python, math, logic, proof checker, natural deduction, fitch, fitch proofs, modal logic",
"author": null,
"author_email": "Daniyal Akif <daniyalakif@gmail.com>",
"download_url": "https://files.pythonhosted.org/packages/7b/06/88a7cb762f10b4cd159c3a6ae6bb2bb82ed84379e5c0625992dd23abbe10/nd_prover-0.1.0.tar.gz",
"platform": null,
"description": "# ND-Prover\r\n\r\nAn interactive Fitch-style natural deduction proof checker, implemented in Python.\r\n\r\nSupports propositional, first-order, and modal logics (K, T, S4, S5) via a command-line interface.\r\n\r\n\r\n## Logic Checklist\r\n\r\n- [x] Propositional logic (TFL)\r\n- [x] First-order logic (FOL)\r\n- [x] Modal logic K (MLK)\r\n- [x] Modal logic T (MLT)\r\n- [x] Modal logic S4 (MLS4)\r\n- [x] Modal logic S5 (MLS5)\r\n\r\n\r\n## Example Usage\r\n\r\n```\r\n$ python -m nd_prover\r\nSelect logic (TFL, FOL, MLK, MLT, MLS4, MLS5): TFL\r\nEnter premises (separated by \",\" or \";\"): P -> Q, P\r\nEnter conclusion: Q\r\n\r\n 1 | P \u2192 Q PR\r\n 2 | P PR\r\n |---\r\n\r\n1 - Add a new line\r\n2 - Begin a new subproof\r\n3 - End the current subproof\r\n4 - End the current subproof and begin a new one\r\n5 - Delete the last line\r\n\r\nSelect action: 1\r\nEnter line: Q ; ->E, 1,2\r\n\r\n 1 | P \u2192 Q PR\r\n 2 | P PR\r\n |---\r\n 3 | Q \u2192E, 1,2\r\n\r\nProof complete! \ud83c\udf89\r\n```\r\n\r\nA proof of the law of excluded middle (LEM) using ND-Prover: \r\n\r\n```\r\nProof of \u2234 P \u2228 \u00acP\r\n------------------\r\n\r\n 1 | | \u00ac(P \u2228 \u00acP) AS\r\n | |----------- \r\n 2 | | | P AS\r\n | | |--- \r\n 3 | | | P \u2228 \u00acP \u2228I, 2\r\n 4 | | | \u22a5 \u00acE, 1,3\r\n 5 | | \u00acP \u00acI, 2-4\r\n 6 | | P \u2228 \u00acP \u2228I, 5\r\n 7 | | \u22a5 \u00acE, 1,6\r\n 8 | P \u2228 \u00acP IP, 1-7\r\n\r\nProof complete! \ud83c\udf89\r\n```\r\n\r\nA proof that identity is symmetric: \r\n\r\n```\r\nProof of \u2234 \u2200x\u2200y(x = y \u2192 y = x)\r\n-------------------------------\r\n\r\n 1 | | a = b AS\r\n | |-------\r\n 2 | | a = a =I\r\n 3 | | b = a =E, 1,2\r\n 4 | a = b \u2192 b = a \u2192I, 1-3\r\n 5 | \u2200y(a = y \u2192 y = a) \u2200I, 4\r\n 6 | \u2200x\u2200y(x = y \u2192 y = x) \u2200I, 5\r\n\r\nProof complete! \ud83c\udf89\r\n```\r\n\r\nA proof in modal logic S5: \r\n\r\n```\r\nProof of \u2662\u25a1A \u2234 \u25a1A\r\n-----------------\r\n\r\n 1 | \u2662\u25a1A PR\r\n |----- \r\n 2 | \u00ac\u25a1\u00ac\u25a1A Def\u2662, 1\r\n 3 | | \u00ac\u25a1A AS\r\n | |----- \r\n 4 | | | \u25a1 AS\r\n | | |--- \r\n 5 | | | \u00ac\u25a1A R5, 3\r\n 6 | | \u25a1\u00ac\u25a1A \u25a1I, 4-5\r\n 7 | | \u22a5 \u00acE, 2,6\r\n 8 | \u25a1A IP, 3-7\r\n\r\nProof complete! \ud83c\udf89\r\n```\r\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "An interactive Fitch-style proof checker",
"version": "0.1.0",
"project_urls": {
"Homepage": "https://github.com/daniyal1249/nd-prover",
"Repository": "https://github.com/daniyal1249/nd-prover"
},
"split_keywords": [
"python",
" math",
" logic",
" proof checker",
" natural deduction",
" fitch",
" fitch proofs",
" modal logic"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "68208ffb84e2b600774e6a7d8ded82275dd24fec8da86805913f71250477fc24",
"md5": "5f9f906cb7fe4f3cfdcf960c5f80ff3c",
"sha256": "b764b80395f705499c00230a6ac2d31361660de9c75af8aeb21cf1b8ab992592"
},
"downloads": -1,
"filename": "nd_prover-0.1.0-py3-none-any.whl",
"has_sig": false,
"md5_digest": "5f9f906cb7fe4f3cfdcf960c5f80ff3c",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.10",
"size": 11913,
"upload_time": "2025-08-04T23:54:17",
"upload_time_iso_8601": "2025-08-04T23:54:17.083857Z",
"url": "https://files.pythonhosted.org/packages/68/20/8ffb84e2b600774e6a7d8ded82275dd24fec8da86805913f71250477fc24/nd_prover-0.1.0-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "7b0688a7cb762f10b4cd159c3a6ae6bb2bb82ed84379e5c0625992dd23abbe10",
"md5": "ef598b8a788ff667180c63d95e22686b",
"sha256": "ac06f59865ebd34feb504b4e8d91d1cfde6395b2a226a0d9668ec759a55f76d8"
},
"downloads": -1,
"filename": "nd_prover-0.1.0.tar.gz",
"has_sig": false,
"md5_digest": "ef598b8a788ff667180c63d95e22686b",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.10",
"size": 11925,
"upload_time": "2025-08-04T23:54:18",
"upload_time_iso_8601": "2025-08-04T23:54:18.615827Z",
"url": "https://files.pythonhosted.org/packages/7b/06/88a7cb762f10b4cd159c3a6ae6bb2bb82ed84379e5c0625992dd23abbe10/nd_prover-0.1.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-08-04 23:54:18",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "daniyal1249",
"github_project": "nd-prover",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "nd-prover"
}
JSON
