[opentheory-users] arguments to eqMp

[Ramana Kumar]

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
>>>
>>
>