[opentheory-users] Wrong certificates

[Chantal Keller]

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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.art
Type: image/x-jg
Size: 801 bytes
Desc: not available
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20121119/dd356a38/attachment.art>