Interactive and Automated Theorem Prover
Welcome to AFGProver, an interactive and automated theorem prover built and developed in Java. Aim of this small one-man project is to create a fun and neat pocket-sized interactive and automated theorem prover for FOL.
Requirements:
- Minimal: Java SDK 17.0.12 (https://www.oracle.com/java/technologies/javase/jdk17-archive-downloads.html)
- Recommended: Java SDK 23.0.2 (https://www.oracle.com/java/technologies/downloads/#java23)
Installation:
- Download and install Java SDK. Make sure to include javaw.exe to path!
- Download the repository and extract
- Double click on AFGProver.jar
Currently, the only implemented feature is the interactive prover for propositional and first order logic based on Gentzens Natural Deduction system. Plans for other logic systems, as well as simple automated prover for first order logic are underway and this project will be updated accordingly. Planned features:
- Equality rules
- Naming lemmas, assumptions
- Adding Substition/Cut rules
- Importing files
- Custom rules
- Types
- Induction
- Set theory
- Interactive prover for Modal logics
- Interactive provers in other systems like: Sequent calculus, Analytical tabloux, ...
- Automated prover for FOL
- Automated importing of TPTP problems
- UI overhaul
- Re-writing the core elements in a faster language and other optimizations
Fully detailed documentation can be found in the AFG Prover.pdf file: Documentation
