My first successful results of the mapping from Discrete Math rules of inference to ProofPower are attached in case they are useful to anyone else working on a similar project.

a mapping from discrete math "rules of inference" to ProofPower <https://www.dropbox.com/s/mtdejdpgzziz6g5/mapping_rules_of_inference.pdf?dl=0> On Sat, Feb 28, 2015 at 11:47 PM, David Topham <dtop...@ohlone.edu> wrote: > The first successful results of the mapping from Discrete Math rules of > inference to ProofPower are attached in case they are useful to anyone else > working on a similar project. > > On Thu, Feb 5, 2015 at 9:00 AM, <proofpower-requ...@lemma-one.com> wrote: > >> Send Proofpower mailing list submissions to >> proofpower@lemma-one.com >> >> To subscribe or unsubscribe via the World Wide Web, visit >> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com >> or, via email, send a message with subject or body 'help' to >> proofpower-requ...@lemma-one.com >> >> You can reach the person managing the list at >> proofpower-ow...@lemma-one.com >> >> When replying, please edit your Subject line so it is more specific >> than "Re: Contents of Proofpower digest..." >> >> >> Today's Topics: >> >> 1. Re: ProofPower and Discrete Math (David Topham) >> 2. Re: ProofPower and Discrete Math (Rob Arthan) >> >> >> ---------------------------------------------------------------------- >> >> Message: 1 >> Date: Wed, 4 Feb 2015 12:49:47 -0800 >> From: David Topham <dtop...@gmail.com> >> To: Roger Bishop Jones <postmas...@rbjones.com> >> Cc: ProofPower List <proofpower@lemma-one.com> >> Subject: Re: [ProofPower] ProofPower and Discrete Math >> Message-ID: >> < >> cad034bgcumtxj3nkvjjpcxdspsd5s_7ipw+tli0mfu6htwo...@mail.gmail.com> >> Content-Type: text/plain; charset="utf-8" >> >> 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 >> > >> > >> > >> > >> > >> -------------- next part -------------- >> An HTML attachment was scrubbed... >> URL: < >> http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20150204/341a13e6/attachment-0001.html >> > >> >> ------------------------------ >> >> Message: 2 >> Date: Thu, 5 Feb 2015 09:26:35 +0000 >> From: Rob Arthan <r...@lemma-one.com> >> To: ProofPower List <proofpower@lemma-one.com> >> Subject: Re: [ProofPower] ProofPower and Discrete Math >> Message-ID: <168c72a1-7647-431d-a430-1fb91781b...@lemma-one.com> >> Content-Type: text/plain; charset="utf-8" >> >> >> 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. >> >> -------------- next part -------------- >> An HTML attachment was scrubbed... >> URL: < >> http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20150205/8527c9fb/attachment-0001.html >> > >> >> ------------------------------ >> >> Subject: Digest Footer >> >> _______________________________________________ >> Proofpower mailing list >> Proofpower@lemma-one.com >> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com >> >> >> ------------------------------ >> >> End of Proofpower Digest, Vol 90, Issue 3 >> ***************************************** >> > >

_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com