[opentheory-users] deductAntisym and eqMp

[Joe Leslie-Hurd]

OpenTheory theorem hypotheses are indeed supposed to be represented by a
set of terms modulo alpha-equivalence: I've added a note to that effect in
the description of the thm type in

http://www.gilith.com/research/opentheory/article.html

Cheers,

Joe


On Thu, Dec 5, 2013 at 2:33 PM, Ramana Kumar <ramana at member.fsf.org> wrote:

> I believe they are intended to be interpreted modulo alpha-convertibility,
> indeed.
> (There's also a note at the top of the article specification saying Thm
> objects are interchangeable if terms in them are alpha-convertible.)
> HOL4 also uses sets-up-to-alpha for the assumptions on a sequent.
>
>
> On Thu, Dec 5, 2013 at 2:18 PM, Rob Arthan <rda at lemma-one.com> wrote:
>
>> The specifications of deductAntisym and eqMp use set operations on the
>> assumptions. Are these intended to be interpreted modulo
>> alpha-convertibility? (ProofPower and HOL Light both treat the assumptions
>> as ordered sets  using  alpha-convertibility as the equality test when
>> inserting and deleting elements, but I don't know about HOL4.) If the
>> answer is no, then a reader for ProofPower or HOL Light is going to have to
>> use some fairly horrid tricks.
>>
>> Regards,
>>
>> Rob.
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131206/5cb3a91f/attachment.html>