Logic is the foundation of all computer science, yet almost all proofs are done with pen and paper instead of using a computer to do them automatically.
Although deciding whether a boolean formula is satisfiable is a NP-complete problem, there are more efficient algorithms than brute force to solve it. Studying and implementing such algorithms would allow to write more efficient methods to decide if a proposition is always truth and thus be able to perform some formal proofs automatically and efficiently instead of using truth tables to do so.
This project will be based around studying algorithms to decide if a proposition is always true or if a proposition is satisiable. Benchmarks and complexity analysis for such algorithms will be done to decide which algorithm has a better memory and time performance.