Open mcodescu opened 8 years ago
Is the URL correct? I believe it should be.
for some reason pellet is not found and eprover used instead
maeder@lati:~/Hets$ curl http://localhost:8000/consistency-check/http%3A%2F%2Fontohub.org%2Fanimal_monster%2Fbear.dol?node=Bear&cons-checker=Pellet&timeout=20
[2] 11793
[3] 11794
maeder@lati:~/Hets$ cons-checker=Pellet: Befehl nicht gefunden.
<?xml version='1.0' ?>
<result state="Consistent">consistent, but could not reconstruct a model
extractModel not implemented for comorphism composition with id_OWL.NP-SIN;OWL22CASL
Satisfiable
Darwin 1.4.4
Finite Domain: setting initial domain size to 1.
Finite Domain: using non-ground splitting in preprocessing.
Parsing /tmp/bear_Bear11636.tptp ...
Calling /home/linux-bkb/bin/eprover for clausification ...
Proving ...
SZS status Satisfiable for /tmp/bear_Bear11636.tptp
MODEL (TPTP):
SZS output start FiniteModel for /tmp/bear_Bear11636.tptp
...
This is strange. On my machine eprover is also not found:
mcodescu@nuance:~$ curl http://localhost:8000/consistency-check/http%3A%2F%2Fontohub.org%2Fanimal_monster%2Fbear.dol&node=Bear&consistency-checker=eprover&timeout=20
[1] 9301
[2] 9302
[3] 9303
mcodescu@nuance:~$ consistency-checker=eprover: command not found
curl: (52) Empty reply from server
[1] Exit 52 curl http://localhost:8000/consistency-check/http%3A%2F%2Fontohub.org%2Fanimal_monster%2Fbear.dol
[2]- Done node=Bear
[3]+ Exit 127 consistency-checker=eprover
I also get a message cons-checker=eprover: Befehl nicht gefunden.
and actually Darwin 1.4.4
is used (that only internally uses eprover). (which eprover
succeeds for me.)
maeder@lati:~/Hets$ curl http://localhost:8000/consistency-checkers/http%3A%2F%2Fontohub.org%2Fanimal_monster%2Fbear.dol/?node=Bear
<?xml version='1.0' ?>
<Provers>
<consistencyCheckers>
<li>
<identifier>Pellet</identifier>
<name>Pellet</name>
</li>
<li>
<identifier>Fact</identifier>
<name>Fact</name>
</li>
<li>
<identifier>darwin-non-fd</identifier>
<name>darwin-non-fd</name>
</li>
<li>
<identifier>darwin</identifier>
<name>darwin</name>
</li>
<li>
<identifier>e-darwin</identifier>
<name>e-darwin</name>
</li>
<li>
<identifier>eprover</identifier>
<name>eprover</name>
</li>
<li>
<identifier>leo</identifier>
<name>leo</name>
</li>
<li>
<identifier>iproveropt</identifier>
<name>iproveropt</name>
</li>
<li>
<identifier>ekrh</identifier>
<name>ekrh</name>
</li>
</consistencyCheckers>
</Provers>
promises more than is kept.
It seems passing consistency-checker names was never really tested.
When doing:
curl http://localhost:8000/consistency-check/http%3A%2F%2Fontohub.org%2Fanimal_monster%2Fbear.dol&node=Bear&consistency-checker=Pellet&timeout=20
I get 'consistency-checker=Pellet: command not found' and in the command window where the server is running 'SuleCFOL2SoftFOL.transOPSYMB: unknown op: Qual_op_name http_u_uwww_uhets_ueu_uontology_uunamed_urfh_upb (Op_type Total [] Thing nullRange) nullRange'
I can prove consistency of the node Bear with Pellet via the HETS GUI, and I don't know why the translation SuleCFOL2SoftFOL should be involved if the current logic is OWL.