Why is this useful?
Well, sometimes it is more efficient to use a computer in order to obtain CNF/DNFs for simplifying formulas using different methods of simplification in boolean algebra (Veitch, Karnaugh, Quine–McCluskey, Moisil's method, etc...).
Who would be interested in such a tool?
Anyone who does not want to waste time simplifying formulas, especially students who have to "deal" with Computation Logic in college.
What can it do so far?
- solve implications such as p→q or (p→q)→(r→t)
- detect Conjunctive/Disjunctive Normal Forms, identifying their clauses/cubes, number of variables, unary and binary operations
- solve double negations using De Morgan's laws
What is next?
- prove inconsistency of a formula using the Semantic Tableaux Method - graphical approach
- bring formulas to their simplest forms using boolean algebra graphical simplifications methods: Veitch and Karnaugh Diagrams
