ProofBuilder, a Nifty Tool for Facilitating Students' Construction of Proofs
Proposer:
Hugh McGuire
Grand Valley State University;
1 Campus Drive; Allendale, MI 49401-9403
telephone: (616) 331-2915; FAX: (616) 331-2106
mcguire@cis.gvsu.edu ;
http://www.cis.gvsu.edu/~mcguire/
Note: I presented this in a poster at SIGCSE'07.
Abstract
ProofBuilder is a computer program
that facilitates construction of proofs
of logic formulas such as
[(P ∨ Q) ⇒ R] ⇒ [(P ⇒ R) ∧ (Q ⇒ R)]
and
(∀n)[10^n mod 3 = 1],
providing strategic as well as deductive operations
for constructing proofs such as
rewriting formulas using logical equivalencies,
eliminating quantifiers,
separating implications into hypotheses and (desired) conclusions,
forward reasoning (a.k.a. proving directly),
backward reasoning,
proving by contradiction,
proving by cases,
substituting using equations,
and applying stepwise or strong induction.
This software is designed for student users to learn to construct proofs,
so it does not do automated deduction:
a student user must do the 'high-level'
deductive planning and reasoning necessary in constructing a proof.
But
this software helps students by
(i) providing a framework that clarifies the construction of proofs,
e.g. showing whether hypotheses have or haven't been used yet;
(ii) doing
the work of performing
menial
symbolic manipulations such as substituting "0"
and "n+1" where appropriate when applying
stepwise
induction;
and (iii) enforcing soundness of deductive steps.
ProofBuilder is written in Java, so
it is usable
on essentially all
common modern
platforms (Microsoft Windows,
LINUX,
Apple Macintosh,
UNIX, etc.);
it has
a graphical user interface,
including
capabilities for copying and pasting
formulas from other convenient sources such as Web pages;
it uses Unicode characters such as "∀" and "⊆";
and
it provides
to-the-millisecond timestamps which enable detection of
copying (i.e. cheating).
An option for output is HTML,
which
can then be displayed or saved in
other
formats such as PDF
by
Web-browsing software.