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 <div class="gmail_extra"> <div class="gmail_quote">On Mon, Nov 19, 2012 at 1:46 PM, Chantal Keller <<a href="mailto:chantal.keller@wanadoo.fr" target="_blank">chantal.keller@wanadoo.fr</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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 <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </blockquote></div> </div>