[opentheory-users] arguments to eqMp

[Ramana Kumar]

yeah it was my implementation of deductAntisym - sorry for all the noise!

On Mon, Jan 10, 2011 at 4:02 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> All right now I'm starting to suspect it's not to do with eqMp at all...
> T ⇔ (x = x)
> (T ⇔ ((x = x) ⇔ T)) ⇔ ((x = x) ⇔ T)
> Perhaps the deductAntisym documentation is wrong?
> (Or my implementation of deductAntisym is wrong - I will check now...)
>
> On Mon, Jan 10, 2011 at 3:59 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> I think it's an implementation (or package) bug, because the same
>> article file also tries to do eqMp on these:
>> T ⇔ T
>> (T ⇔ T) ⇔ (((λx. x) = (λx. x)) ⇔ T)
>>
>> On Mon, Jan 10, 2011 at 3:55 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>> There may be another bug in the documentation (or implementation) to
>>> do with eqMp.
>>> I believe bool.art from bool-1.0 tries to do an eqMp on theorems with
>>> these conclusions:
>>> x = x
>>> (T ⇔ (x = x)) ⇔ (x = x)
>>> but the second theorem is the reflection of what you would expect
>>> given the documentation.
>>> On Mon, Jan 10, 2011 at 12:17 AM, Joe Hurd <joe at gilith.com> wrote:
>>>> Hi Ramana,
>>>>
>>>> Documentation bug - now fixed. Good catch.
>>>>
>>>> Cheers,
>>>>
>>>> Joe
>>>>
>>>> On Sun, Jan 9, 2011 at 1:12 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>>>> Is the documentation of the file format here
>>>>> http://www.gilith.com/research/opentheory/article.html#eqMpCommand
>>>>> correct?
>>>>> My reader appears to be saying that the article file corresponding to
>>>>> bool-1.0 wants |- phi to be popped before |- phi' = psi
>>>>>
>>>>> _______________________________________________
>>>>> 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
>>>>
>>>
>>
>