Automated Theorem Prover for Classical and Non-Classical Logics
Note: This project was intended to be used in an artificial general intelligence system, but given that I've quite changed my mind on how to implement such a system, this repository is no longer being worked on and remains largely unfinished (even though the individual logics which are checked are completely functional and autonomous).
Automated Theorem Prover based on Analytic Tableaux for:
- classical propositonal logic, ✅
- classical logic with quantification, ✅
- normal modal logic, ✅
- normal modal logic with quantification, ⬜
- conditional logic, ⬜
- intuitionistic logic, ⬜
- many-valued logic, ⬜
- relevant logic, ⬜
- fuzzy logic ⬜
Theory behind the systems: An Introduction to Non-Classical Logic: From If to Is - Graham Priest