On 3 Feb 2015, at 21:16, Roger Bishop Jones <r...@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. > For the record, here it is in Unicode: 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; > 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. > Another way of finding all the forward inference rules provided is to browse the entries for “rule”, “elim”, “intro” and “conv" in the keyword in context index. > The HOL Tutorial Notes USR013 has perhaps more accessible descriptions of > a selection of rules in Chapter 5. Indeed. Regards, Rob.
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
