A domain reasoner for propositional logic

Students learn propositional logic in programs such as mathematics, philosophy, computer science, law, etc. An important topic in courses in propositional logic is rewriting propositional formulae with standard equivalences, and the application of this technique in exercises on rewriting a formula in normal form, proving the equivalence between two formulae or proving that a formula is a consequence of a set of formulae. Existing learning environments for propositional logic offer limited feedback and feed forward. This paper analyses what kind of feedback is offered by the various learning environments for rewriting propositional logic formulae, and discusses how we can provide these kinds of feedback in a learning environment. To give feedback and feed
forward, we define solution strategies for several classes of exercises. We offer an extensive description of the knowledge necessary to support solving this kind of propositional logic exercises in a learning environment. This description serves as an illustration of how to develop the artificial intelligence for a particular domain.