[opentheory-users] Wrong certificates

[Ramana Kumar]

Hi Chantal,

I haven't looked at your article yet, but one possibility that comes to
mind is that the two "x"s on the left hand side of the theorem are distinct.
What is your interpretation that satisfies the assumptions but not the
theorem?
Does it still work if the x under the binder has a variable type (while the
x in the body has type bool)?

Ramana


On Mon, Nov 19, 2012 at 1:46 PM, Chantal Keller
<chantal.keller at wanadoo.fr>wrote:

> Dear OpenTheory users and developers,
>
> It appears to me that opentheory checks as correct wrong certificates.
>
> Attached is an example. opentheory answers:
>
> 2 input type operators: -> bool
> 2 input constants: = T
> 1 assumption:
>   |- x <=> T
> 1 theorem:
>   |- (\x. x) = \x. T
>
> But I think this should be forbidden: there is an interpretation of the
> variables that satisfies the assumptions but not the theorems.
>
> Perhaps you should restrict assumptions to close terms, or add a side
> condition to the absThm rule?
>
> Thanks,
>
> --
> Chantal KELLER.
>
> _______________________________________________
> 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/20121119/05df7aa5/attachment.html>