Step by step generator for CNF in propositional logic?
I am looking for software like Symbolab except for propositional logic.
When given a formula in propositional logic the software should output steps for converting the formula into Conjunctive Normal Form (CNF).
below is the output of this imaginary program when given the formula:
$$(a \lor b)\implies (\lnot a \implies b) $$
The software can be in any language.