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

Reply via email to