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
forwardproof.doc.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
