Roger, Thank you very much! This example got me past my mental block and I
see how to work with these proofs much better now. I appreciate your time
in helping me. Now I see one of my tasks is to map the names I use (such as
hypothetical syllogism) to the names used within ProofPower (such as
=>_trans_rule). I will work on that mapping...  -Dave

On Tue, Feb 3, 2015 at 7:29 AM, Roger Bishop Jones <>

> On 03/02/15 13:55, David Topham wrote:
> >
> >
> > I am interested in using ProofPower to aid in the teaching of Discrete
> > Math. I would like to assist the students in developing proofs using
> > specific rules of inference. e.g. in the attached proof from our
> > textbook the proof uses Hypothetical Syllogism to prove a
> > Propositional expression. I don't quite see yet from the tutorials how
> > to direct ProofPower in this way. Is it possible? Does anyone have
> > experience using ProofPower like this? If so, I would appreciate some
> > guidance. It seems so far in my observations, that pp is used by
> > selecting some "tactics" which then guide pp to find  a proof, but we
> > would need to direct each step as part of the learning process.
> > Thanks, Dave
> >
> The proof you exhibit is what we would call a "forward proof".
> The subgoal package is used for what we call "backward" (or goal
> oriented) proofs.
> A forward proof for the result you require runs like this:
> val L1 = asm_rule ¬P ´ Q®;
> val L2 = asm_rule ¬Q ´ R®;
> val L3 = ´_trans_rule L1 L2;
> val L4 = asm_rule ¬R ´ P®;
> val L5 = ¤_intro L3 L4;
> Except that the characters are a mess because I just copied
> and pasted from the xpp window which doesn't work.
> The value of L5 will be the desired result/
> I attach a proofpower document  containing the proof.
> The documentation for the inference rules is in the reference manual
> USR029 section 8.1.
> The HOL Tutorial Notes USR013 has perhaps more accessible descriptions of
> a selection of rules in Chapter 5.
> Roger Jones
Proofpower mailing list

Reply via email to