Proofster
Before Proofster was built into a web app with several microservices and a domain layer running in the backend, the project simply exist as a series of Python scripts that I wrote to prototype the project. Some of the files were hundreds of lines. They were eventually abstracted into layers and packed into modules that forms the new architecture in the proofster project.
Demo
Implementation Details
Class: Formula, Unary, Binary, Function, Variable
Will add an UML when finished
The Preprocessor
Preprocessing includes the following procedures which are mostly implemented using recursion
Negate Conclusion
Nothing special, just adding a negation
Convert To Prenex Normal Form
Sub steps:
- Remove arrows
- Move negation inward
- Standardize variables
- Move all quantifiers to front
- Skolemization
Convert To Clauses
Sub steps:
- Drop all quantifiers
- Convert to CNF (Conjunctive Normal Form)
- Populate clauses
The Resolution Prover
Currently researching (relearning) various strategies of resolution.