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

Attachment: forwardproof.doc.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to