-
In this paper we describe a teaching tool for proving
equivalences between propositional logic formulae, using rewrite rules such as
De Morgan's laws and double negation. This tool is based on an earlier tool for
rewriting logical formulae into disjunctive normal form (DNF). Both tools make
use of a rewrite strategy, which specifies how an exercise can be solved
stepwise. Different types of feedback can be calculated automatically from such a
strategy specification. We describe a strategy for constructing expert-like
equivalence proofs, and present two techniques for improving the proofs that are
generated by the strategy.
-
Paper, accepted at
TICTTL 2011
(© 2011, Springer-Verlag)