Thank you Mark. I appreciate you taking the time to help me out--that worked perfectly. -Dave
On Fri, Mar 11, 2016 at 9:00 AM, <[email protected]> wrote: > Send Proofpower mailing list submissions to > [email protected] > > 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 > [email protected] > > You can reach the person managing the list at > [email protected] > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Proofpower digest..." > > > Today's Topics: > > 1. V_cancel_rule alpha-conversion error (David Topham) > 2. Re: V_cancel_rule alpha-conversion error > ([email protected]) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 11 Mar 2016 00:53:45 -0800 > From: David Topham <[email protected]> > To: ProofPower List <[email protected]> > Subject: [ProofPower] V_cancel_rule alpha-conversion error > Message-ID: > <CAD034BFkUpCkWrRPHjLOBk48XxSXye+XV1L= > [email protected]> > Content-Type: text/plain; charset="utf-8" > > I am trying to do a forward proof using hypothetical syllogism > (V_cancel_Rule) > of this form: ~q v r, q |- r > but get an alpha-conversion error. > (sorry for the hard to read format here, but I know I can't post images or > pdf files here, so what other way is there to show the extended chars of > ProofPower? I did > ascii-conv to get this format) > > val L1 = p %thm% p: THM > val L2 = p %implies% q %thm% p %implies% q: THM > val L3 = p %implies% q, p %thm% q: THM > val L4 = %not% q %or% r %thm% %not% q %or% r: THM > > Exception Fail * ? q ? r ? ? q ? r and p ? q, p ? q are not of the form: > `?1 ? > t1 ? t2' and `?2 ? ?t3' where ?t3? is ?-convertible to ?t1? or ?t2? > [?_cancel_rule.7050] * raised > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20160311/2ddae95b/attachment-0001.html > > > > ------------------------------ > > Message: 2 > Date: Fri, 11 Mar 2016 14:06:27 +0000 > From: [email protected] > To: ProofPower List <[email protected]> > Subject: Re: [ProofPower] V_cancel_rule alpha-conversion error > Message-ID: > <[email protected]> > Content-Type: text/plain; charset="utf-8" > > Hi Dave, > > With this rule, the theorems need to precisely match up with how they > are described in the manual, so you need to have the conclusion of the > 2nd theorem as the logical negation of the LHS of the "or" in the 1st > thm (not vice versa). So just use the double logical negation > introduction rule on the 2nd theorem, and then it works. > > Perhaps using good old ASCII versions of the logical symbols a good > idea. This is what the HOL4 and HOL Light use. So there's: > disjunction: \/ > conjuntion: /\ > logical negation: ~ > implication: ==> > logical equivalence: <=> > universal quantification: ! > existential quantification: ? > unique existential quantification: ?! > > Mark. > > On 11/03/2016 08:53, David Topham wrote: > > > I am trying to do a forward proof using hypothetical syllogism > (V_cancel_Rule) > > of this form: ~q v r, q |- r > > but get an alpha-conversion error. > > (sorry for the hard to read format here, but I know I can't post images > or pdf files here, so what other way is there to show the extended chars of > ProofPower? I did > > ascii-conv to get this format) > > > > val L1 = p %thm% p: THM > > val L2 = p %implies% q %thm% p %implies% q: THM > > val L3 = p %implies% q, p %thm% q: THM > > val L4 = %not% q %or% r %thm% %not% q %or% r: THM > > > > Exception Fail * ? q ? r ? ? q ? r and p ? q, p ? q are not of the form: > `?1 ? > > t1 ? t2' and `?2 ? ?t3' where ?t3(R) is ?-convertible to ?t1(R) or ?t2(R) > > [?_cancel_rule.7050] * raised > > _______________________________________________ > > Proofpower mailing list > > [email protected] > > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20160311/300dfdc9/attachment-0001.html > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Proofpower mailing list > [email protected] > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > > ------------------------------ > > End of Proofpower Digest, Vol 101, Issue 1 > ****************************************** >
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
