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, <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. V_cancel_rule alpha-conversion error (David Topham)
>    2. Re: V_cancel_rule alpha-conversion error
>       (m...@proof-technologies.com)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Fri, 11 Mar 2016 00:53:45 -0800
> From: David Topham <dtop...@ohlone.edu>
> To: ProofPower List <proofpower@lemma-one.com>
> Subject: [ProofPower] V_cancel_rule alpha-conversion error
> Message-ID:
>         <CAD034BFkUpCkWrRPHjLOBk48XxSXye+XV1L=
> zjo+9_jydpo...@mail.gmail.com>
> 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: m...@proof-technologies.com
> To: ProofPower List <proofpower@lemma-one.com>
> Subject: Re: [ProofPower] V_cancel_rule alpha-conversion error
> Message-ID:
>         <7245278f69970a6c1211f108a9c92...@webmail-next.names.co.uk>
> 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
> > Proofpower@lemma-one.com
> > 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
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>
>
> ------------------------------
>
> End of Proofpower Digest, Vol 101, Issue 1
> ******************************************
>
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to