Closed dde-cls closed 5 months ago
Hello,
We are trying to experiment with Zenon Modulo on proof obligations produced by Atelier B. Our TPTP back-end produces Typed First-order Logic formulas. Zenon modulo produces an error when reading this input, e.g.
tff(set_0_type,type,(set_0: $tType )). tff(mem0_type,type,(mem0: ( $int * set_0 ) > $o )). tff(set_1_type,type,(set_1: $tType )). ...
Are there any plans to support this logic ?
Hello,
We are trying to experiment with Zenon Modulo on proof obligations produced by Atelier B. Our TPTP back-end produces Typed First-order Logic formulas. Zenon modulo produces an error when reading this input, e.g.
Are there any plans to support this logic ?