To support students practicing with performing proofs in logic, we have developed three systems: LogEx, LogAx and LogInd.
LogEx is an Intelligent Tutoring System (ITS) in which a student can
practice the rewriting of propositional logic formulae using standard equivalences
such as De Morgan's law or distribution. The LogEx domain reasoner calculates feedback automatically for propositional logic expressions submitted by
students when solving an exercise. For this purpose it uses domain knowledge,
such as rewrite steps, common mistakes, and procedures for solving an exercise.
LogEx is based on the Ideas framework, which supports the development of
ITSs that automatically generate feedback and help for step-wise exercises, for
a wide range of problem domains.
The LogEx system supports three different types of exercises: rewriting a
formula in disjunctive normal form, in conjunctive normal form, and proving the
equivalence of two formulae. Students enter their solution step-wise, providing
the next step and the corresponding rule name of the step, and receive feedback
after each step. LogEx points out syntax errors, it recognizes a wrongly motivated
but correct step, and it provides informative feedback if a common mistake occurs
(a so-called buggy rule). An example of the latter might be the distribution of
a conjunction over a conjunction. Although the result is an equivalent formula,
this application of distribution is incorrect. Our aim is to let the way of working
in LogEx resemble solving exercises using pen-and-paper as much as possible.
Hence, the equivalence proof component of LogEx facilitates working in two
directions. For example, a student can start rewriting the second formula, then
switch to the first formula, and go back to the second.
In LogAx [6] a student can practice with performing Hilbert-style propositional logic proofs. LogAx oers the same type of help as LogEx: informative
feedback, layered hints, next steps and complete solutions. If suitable, a first hint in LogAx will be a reachable subgoal. LogAx uses a dialog box in which a student chooses the axiom or rule she wants to apply. The actual application of the rule is performed by LogAx. In this way, the student can concentrate on the strategy, and occurrences of syntax mistakes such as missing parentheses are minimized.
To give feedback and help, we adapt the algorithm of Bolotov, which generates natural deduction proofs, to Hilbert-style axiomatic proofs. This adaptation
can generate a proof for any provable consequence of a set of formulae, and also
complete any partial proof.
Our latest tool, LogInd, is a tutoring system for practicing the structural
induction proof technique. LogInd guides a student through an inductive proof
by explicitly asking to state and prove a base step, an induction hypothesis and
the inductive steps.