No automatic picture trasmicion , Is Automatic Theorem Prover ->Naptiapt
Naptiapt is a web-based automatic theorem prover that uses Prolog for logical reasoning. It provides an intuitive interface for defining axioms, rules, and facts, then attempts to prove theorems using logical inference.
- Interactive Theorem Proving: Define logical axioms, inference rules, and facts
- Proof Visualization: See step-by-step proof traces when theorems are proven
- Prolog Backend: Leverages Prolog's powerful logical inference engine
- Predefined Examples: Includes several built-in examples to demonstrate the system
- Responsive UI: Clean, intuitive interface for both beginners and experts
- Clone the repository:
git clone https://github.com/yourusername/naptiapt.git
cd naptiapt- Create a virtual environment and install dependencies:
python3 -m venv venv
source venv/bin/activate
pip install -r requirements.txt- Install SWI-Prolog (required for pyswip):
sudo apt-get install swi-prolog- Run the application:
uvicorn main:app --reload- Open your browser and visit: http://localhost:8000
- Define Axioms: Enter logical axioms (one per line)
- Add Rules: Create inference rules with premises and conclusions
- Specify Facts: List known facts (one per line)
- Enter Theorem: State the theorem you want to prove
- Submit: Click "Prove Theorem" to see the result
The system will either:
- Provide a step-by-step proof trace
- Show an error if the theorem can't be proven
- Display any errors in the input
Naptiapt comes with several built-in examples:
-
Socrates Mortality:
- Axioms:
human(socrates) - Rules:
human(X) → mortal(X) - Theorem:
mortal(socrates)
- Axioms:
-
Basic Arithmetic:
- Axioms:
natural(zero),add(zero, X, X) - Rules:
natural(X) → natural(succ(X))add(X, Y, Z) → add(succ(X), Y, succ(Z))
- Theorem:
natural(succ(zero))
- Axioms:
-
Logical Reasoning:
- Axioms:
p,implies(p, q) - Rules:
and(P, implies(P, Q)) → Q - Theorem:
q
- Axioms:
naptiapt/
├── main.py # FastAPI backend and Prolog interface
├── static/ # Static assets (CSS, JS, images)
│ ├── script.js # Frontend logic
│ └── styles.css # Styling
├── templates/ # HTML templates
│ └── index.html # Main UI
├── requirements.txt # Python dependencies
└── README.md # This file
- Python 3.8+
- FastAPI
- Uvicorn
- pyswip
- SWI-Prolog
This project is licensed under the GLPv3 License. See the LICENSE file for details.
Contributions are welcome! Please open an issue or submit a pull request for any improvements or bug fixes.
- Show step by step the proces of proving a theorem