search

Deducteam / zenon_modulo

First-order automated theorem prover based on the tableau method
Other
12 stars 6 forks source link

Exception Type_error on TPTP4X-accepted tptp file #20

Open etienneparent opened 4 months ago

etienneparent commented 4 months ago

Running zenon_modulo version 0.5.0 on this tptp file, I got the following error :

zenon_modulo -itptp problem.txt
Fatal error: exception Typetptp.Type_error("Contradictory types for 'prod_0'")
Raised at Stdlib__Weak.Make.find.(fun) in file "weak.ml", line 297, characters 47-62
Called from Expr.he_merge in file "expr.ml", line 493, characters 6-19

This file is yet valid according to TPTP4X and accepted by other automated theorem provers. problem.txt

gburel commented 4 months ago

It looks like the type of prod_0 is declared twice : 

tff(prod_0_type, type, prod_0 : $tType).

and

tff(prod_0_insert, type, prod_0 : ($int * $int) > prod_0).

I suspect that the second one should declare the type of prod_0_insert.