Metadata-Version: 2.4
Name: nd-prover
Version: 3.1.0
Summary: Natural deduction proof generator & checker
Author-email: Daniyal Akif <daniyalakif@gmail.com>
License-Expression: Apache-2.0
Project-URL: Homepage, https://ndprover.org
Project-URL: Repository, https://github.com/daniyal1249/nd-prover
Keywords: python,math,logic,theorem proving,prover,fitch,natural deduction,modal logic,theorem prover,fitch proofs,proof checker,cvc5
Classifier: Development Status :: 5 - Production/Stable
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Operating System :: OS Independent
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: cvc5==1.3.4
Dynamic: license-file

# ND-Prover

A Fitch-style natural deduction proof generator and checker, implemented in Python.

It is based on the natural deduction system presented in [*forall x: Calgary*](https://forallx.openlogicproject.org).

![ND-Prover demo](nd-prover.gif)

Try ND-Prover online at [ndprover.org](https://ndprover.org).

## Supported Logics

- Propositional logic
- First-order logic
- Modal logic (K, T, S4, S5)
- First-order modal logic

## Features

- Support for both classical and intuitionistic logics
- Argument validity checking
- Automated proof generation for valid arguments
- Countermodel generation for invalid arguments
- Verification of user-provided proofs
- Plain-text and LaTeX proof export

## Package Installation

ND-Prover can be installed using pip:

    pip install nd-prover

or by directly cloning the git repository:

    git clone https://github.com/daniyal1249/nd-prover.git

and running the following in the cloned repo:

    pip install .

## Package Example Usage

```
$ nd-prover
Select logic (TFL, FOL, MLK, MLT, MLS4, MLS5, FOMLK, FOMLT, FOMLS4, FOMLS5): TFL
Enter premises (separated by "," or ";"), or "NA" if none: 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 edit: 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! 🎉
```
