search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

consistency check with different checkers gives contradictory results #1260

Open sternk opened 10 years ago

sternk commented 10 years ago

Reported by mcodescu and assigned to maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1260

With the specification (should be inconsistent, the axiom adds confusion on a free type)

spec S = 
 free type Int ::= 0 | suc(Int) | pre(Int)
 . suc(pre(0)) = 0

I get that S is inconsistent when using ekrh, darwin-non-fd and eprover and that S is consistent when using Pellet and Fact (darwin timeouts). If the reason is that the theory goes beyond what Pellet and Fact can check, should they be made unavailable by a sublogic analysis mechanism?

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/1260#comment:1

I could reproduce the behavior. The comorphism CASL2OWL simply does not translate normal sentences like "suc(pre(0)) = 0". We have no CASL sublogic description for this yet.