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 <postmas...@rbjones.com> wrote: > 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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com