LogEx: Proving the equivalence of two logical formulae

LogEx is an Intelligent Tutoring System (ITS) in which a student can practice the rewriting of propositional logical formulae using standard equivalences such as De Morgan’s law or distribution. Automated feedback is calculated by the LogEx domain reasoner for propositional logic, which provides domain knowledge, such as rewrite steps, common mistakes, and procedures for solving an exercise, for these exercise classes. The system is based on the Ideas framework, which supports the development of ITSs that automatically generate feedback and help for step-wise exercises.