InferenceTestSuite
Opened this issue · 10 comments
- we need a way to determine the KB to be used. This can be done in the
tq
file (as discussed in ontologyportal/sumo#218) or as a parameter for the command line, specifying one of the KBs listed in theconfig.xml
file. I would prefer the second option. - we need to avoid the loading of WN and mappings files.
OK, I managed to run
% java -Xmx7g -classpath $SIGMA_CP com.articulate.sigma.InferenceTestSuite -t SP01.kif.tq
But it gives me the output below. I see the Satisfiable
message from Vampire the CounterSatisfiable for temp-comb
reported by the InferenceTestSuite.inferenceUnitTest
but then the last line shows Failure on SP01.kif.tq
… why this failure?!
Regarding answer extraction, I suspect we should have a notation for that, right? In the SP01.kif.tq (see branch spatial in the SUMO repo) I didn’t ask for any specific answer
(query (orientation X Z Right))
But after changing it to
(query (orientation ?X C Right))
I didn't have any change in the output...
% # SZS output end Saturation.
% ------------------------------
% Version: Vampire 4.4.0 (commit 3dd0ed0c on 2020-02-04 14:57:07 +0100)
% Termination reason: Satisfiable
% Memory used [KB]: 1279
% Time elapsed: 0.015 s
% ------------------------------
% ------------------------------
% Success in time 14.681 s
Index: 4, Size: 4
InferenceTestSuite.inferenceUnitTest(): bindings: []
InferenceTestSuite.inferenceUnitTest(): bindingMap: {}
InferenceTestSuite.inferenceUnitTest(): proof: []
InferenceTestSuite.inferenceUnitTest(): answers: []
InferenceTestSuite.inferenceUnitTest(): tpp status: CounterSatisfiable for temp-comb
============================
InferenceTestSuite.cmdLineTest() : Failure on SP01.kif.tq
I get a proof for this one so it appears to be a configuration issue.
% SZS output end Proof for temp-comb
% ------------------------------
% Version: Vampire 4.4.0 (commit c41a8b5f on 2020-03-31 20:18:58 +0200)
% Termination reason: Refutation
% Memory used [KB]: 22259
% Time elapsed: 0.050 s
% ------------------------------
% ------------------------------
% Success in time 0.509 s
InferenceTestSuite.inferenceUnitTest(): bindings: []
InferenceTestSuite.inferenceUnitTest(): bindingMap: {}
InferenceTestSuite.inferenceUnitTest(): proof: [1. (not
(orientation A C Right)) [] negated_conjecture
...
I see that you have changed the query, and it asks about two constants not in the problem. I have
InferenceTestSuite.inferenceUnitTest(): ask: (orientation A C Right)
added config.xml option key "loadLexicons" with value "false" to turn off loading lexicons, in latest push 6fb4db2
I didn't understand the #60 (comment). In https://github.com/ontologyportal/sumo/blob/spatial/tests/SP01.kif.tq the constants A and C are defined. I am using Merge.kif
only.
Your first query says (query (orientation X Z Right))
try using tinySUMO.kif first to see if it works
I have
<configuration >
<preference name="sumokbname" value="tiny" />
...
<kb name="full">
...
</kb>
<kb name="toplevel" >
<constituent filename="Merge.kif" />
</kb>
<kb name="tiny">
<constituent filename="tinySUMO.kif" />
</kb>
</configuration>
But I am still getting:
java -Xmx7g -classpath $SIGMA_CP com.articulate.sigma.InferenceTestSuite -t SP01.kif.tq
...
% # SZS output end Saturation.
% ------------------------------
% Version: Vampire 4.4.0 (commit 3dd0ed0c on 2020-02-04 14:57:07 +0100)
% Termination reason: Satisfiable
% Memory used [KB]: 1279
% Time elapsed: 0.013 s
% ------------------------------
% ------------------------------
% Success in time 17.066 s
Index: 4, Size: 4
InferenceTestSuite.inferenceUnitTest(): bindings: []
InferenceTestSuite.inferenceUnitTest(): bindingMap: {}
InferenceTestSuite.inferenceUnitTest(): proof: []
InferenceTestSuite.inferenceUnitTest(): answers: []
InferenceTestSuite.inferenceUnitTest(): tpp status: CounterSatisfiable for temp-comb
============================
InferenceTestSuite.cmdLineTest() : Failure on SP01.kif.tq
please pipe your output to a file and send to me privately and I'll try to figure out what might be wrong