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.




Proofpower mailing list

Reply via email to