ontologyportal/sigmakee

bug in the cache code

Closed this issue · 9 comments

How can I turn off the cache during the TPTP generation?

In the proof below, the relation ‘realization’ is AntisymmetricRelation and also not AntisymmetricRelation. The problem is the axiom 9 below that was taken from the cache:

% f: (instance realization SymmetricRelation)
% 5785 of 12452 from file /Users/ar/workspace/sumo/SUMO_Cache.kif at line 6471
% not higher order
fof(kb_SUMO_7905,axiom,(( s__instance(s__realization__m,s__SymmetricRelation) ))).

The proof outline is:

  1. s__instance(s__realization__m,s__AntisymmetricRelation)

  2. ((s__instance(X14,s__SetOrClass) & s__instance(X13,s__SetOrClass)) =>
    (s__disjoint(X14,X13) => ! [X307] : ~(s__instance(X307,X13) & s__instance(X307,X14))))

    (~s__disjoint(X1,X0) | ~s__instance(X1,s__SetOrClass) | ~s__instance(X0,s__SetOrClass) |
    ~s__instance(X2,X1) | ~s__instance(X2,X0))

    ! [X2,X0,X1] : (~s__disjoint(X1,X0) | ~s__instance(X1,s__SetOrClass) |
    ~s__instance(X0,s__SetOrClass) | ~s__instance(X2,X1) | ~s__instance(X2,X0))

  3. s__disjoint(s__SymmetricRelation,s__AntisymmetricRelation)

  4. ! [X15] : (~s__instance(s__SymmetricRelation,s__SetOrClass) | ~s__instance(s__AntisymmetricRelation,s__SetOrClass) |
    ~s__instance(X15,s__SymmetricRelation) | ~s__instance(X15,s__AntisymmetricRelation))

  5. s__instance(s__SymmetricRelation,s__SetOrClass)

  6. ! [X0] : (~s__instance(s__AntisymmetricRelation,s__SetOrClass) | ~s__instance(X0,s__SymmetricRelation) |
    ~s__instance(X0,s__AntisymmetricRelation))

  7. s__instance(s__AntisymmetricRelation,s__SetOrClass)

  8. ! [X0] : (~s__instance(X0,s__SymmetricRelation) | ~s__instance(X0,s__AntisymmetricRelation))

  9. s__instance(s__realization__m,s__SymmetricRelation) via cache ????

Complete output:

% vampire/vampire --mode casc -t 300 sumo/SUMO.tptp
% lrs-4_5:1_add=large:afr=on:afp=40000:afq=1.4:amm=off:anc=none:bs=unit_only:bsr=on:irw=on:lcm=reverse:newcnf=on:nwc=1:stl=30:sd=3:ss=axioms:st=2.0:sos=on:sac=on:updr=off_4 on SUMO
% Refutation not found, incomplete strategy
% ------------------------------
% Version: Vampire 4.4.0 (commit 2aa26454 on 2019-09-18 23:39:43 +0200)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 13176
% Time elapsed: 0.018 s
% ------------------------------
% ------------------------------
% lrs+1003_3_awrs=decay:awrsf=4:add=large:afr=on:afp=100000:afq=2.0:amm=sco:bd=off:cond=fast:fsr=off:fde=unused:gs=on:gsem=on:nm=6:nwc=1:stl=30:sd=1:ss=axioms:st=1.2:sos=on:sac=on:sp=frequency:urr=on:updr=off_4 on SUMO
% Refutation not found, incomplete strategy
% ------------------------------
% Version: Vampire 4.4.0 (commit 2aa26454 on 2019-09-18 23:39:43 +0200)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 17654
% Time elapsed: 0.024 s
% ------------------------------
% ------------------------------
% ott+11_8:1_av=off:bs=on:bce=on:fde=none:gsp=input_only:gs=on:gsem=on:irw=on:lcm=predicate:nm=6:nwc=1.5:sd=2:ss=axioms:st=1.2:sos=theory:urr=on:updr=off_7 on SUMO
% Refutation not found, incomplete strategy
% ------------------------------
% Version: Vampire 4.4.0 (commit 2aa26454 on 2019-09-18 23:39:43 +0200)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 13176
% Time elapsed: 0.025 s
% ------------------------------
% ------------------------------
% ott+1002_128_av=off:bd=off:bs=on:bsr=on:cond=on:fsr=off:nm=6:newcnf=on:nwc=1:sp=reverse_arity:updr=off_62 on SUMO
% Refutation found. Thanks to Tanya!
% SZS status Unsatisfiable for SUMO
% SZS output start Proof for SUMO
fof(f62365,plain,(
  $false),
  inference(subsumption_resolution,[],[f33649,f62341])).
fof(f62341,plain,(
  ~s__instance(s__realization__m,s__AntisymmetricRelation)),
  inference(resolution,[],[f62333,f33608])).
fof(f33608,plain,(
  s__instance(s__realization__m,s__SymmetricRelation)),
  inference(cnf_transformation,[],[f7905])).
fof(f7905,axiom,(
  s__instance(s__realization__m,s__SymmetricRelation)),
  file('sumo/SUMO.tptp',kb_SUMO_7905)).
fof(f62333,plain,(
  ( ! [X0] : (~s__instance(X0,s__SymmetricRelation) | ~s__instance(X0,s__AntisymmetricRelation)) )),
  inference(resolution,[],[f62332,f34407])).
fof(f34407,plain,(
  s__instance(s__AntisymmetricRelation,s__SetOrClass)),
  inference(cnf_transformation,[],[f3916])).
fof(f3916,axiom,(
  s__instance(s__AntisymmetricRelation,s__SetOrClass)),
  file('sumo/SUMO.tptp',kb_SUMO_3916)).
fof(f62332,plain,(
  ( ! [X0] : (~s__instance(s__AntisymmetricRelation,s__SetOrClass) | ~s__instance(X0,s__SymmetricRelation) | ~s__instance(X0,s__AntisymmetricRelation)) )),
  inference(resolution,[],[f62135,f34356])).
fof(f34356,plain,(
  s__instance(s__SymmetricRelation,s__SetOrClass)),
  inference(cnf_transformation,[],[f6175])).
fof(f6175,axiom,(
  s__instance(s__SymmetricRelation,s__SetOrClass)),
  file('sumo/SUMO.tptp',kb_SUMO_6175)).
fof(f62135,plain,(
  ( ! [X15] : (~s__instance(s__SymmetricRelation,s__SetOrClass) | ~s__instance(s__AntisymmetricRelation,s__SetOrClass) | ~s__instance(X15,s__SymmetricRelation) | ~s__instance(X15,s__AntisymmetricRelation)) )),
  inference(resolution,[],[f38072,f24380])).
fof(f24380,plain,(
  s__disjoint(s__SymmetricRelation,s__AntisymmetricRelation)),
  inference(cnf_transformation,[],[f3608])).
fof(f3608,axiom,(
  s__disjoint(s__SymmetricRelation,s__AntisymmetricRelation)),
  file('sumo/SUMO.tptp',kb_SUMO_3608)).
fof(f38072,plain,(
  ( ! [X2,X0,X1] : (~s__disjoint(X1,X0) | ~s__instance(X1,s__SetOrClass) | ~s__instance(X0,s__SetOrClass) | ~s__instance(X2,X1) | ~s__instance(X2,X0)) )),
  inference(cnf_transformation,[],[f21184])).
fof(f21184,plain,(
  ! [X0,X1] : (! [X2] : (~s__instance(X2,X0) | ~s__instance(X2,X1)) | ~s__disjoint(X1,X0) | ~s__instance(X1,s__SetOrClass) | ~s__instance(X0,s__SetOrClass))),
  inference(flattening,[],[f21183])).
fof(f21183,plain,(
  ! [X0,X1] : ((! [X2] : (~s__instance(X2,X0) | ~s__instance(X2,X1)) | ~s__disjoint(X1,X0)) | (~s__instance(X1,s__SetOrClass) | ~s__instance(X0,s__SetOrClass)))),
  inference(ennf_transformation,[],[f15918])).
fof(f15918,plain,(
  ! [X0,X1] : ((s__instance(X1,s__SetOrClass) & s__instance(X0,s__SetOrClass)) => (s__disjoint(X1,X0) => ! [X2] : ~(s__instance(X2,X0) & s__instance(X2,X1))))),
  inference(rectify,[],[f2665])).
fof(f2665,axiom,(
  ! [X13,X14] : ((s__instance(X14,s__SetOrClass) & s__instance(X13,s__SetOrClass)) => (s__disjoint(X14,X13) => ! [X307] : ~(s__instance(X307,X13) & s__instance(X307,X14))))),
  file('sumo/SUMO.tptp',kb_SUMO_2665)).
fof(f33649,plain,(
  s__instance(s__realization__m,s__AntisymmetricRelation)),
  inference(cnf_transformation,[],[f7894])).
fof(f7894,axiom,(
  s__instance(s__realization__m,s__AntisymmetricRelation)),
  file('sumo/SUMO.tptp',kb_SUMO_7894)).
% SZS output end Proof for SUMO
% ------------------------------
% Version: Vampire 4.4.0 (commit 2aa26454 on 2019-09-18 23:39:43 +0200)
% Termination reason: Refutation

% Memory used [KB]: 43112
% Time elapsed: 1.225 s
% ------------------------------
% ------------------------------
% Success in time 1.467 s

No, my config.xml contains

<preference name="cache" value="no" />

It looks like Sigma is ignoring the config file parameter. See the output

% java -Xmx7g -classpath $SIGMA_CP com.articulate.sigma.trans.SUMOKBtoTPTPKB
Info in KBmanager.initializeOnce()
Info in KBmanager.initializeOnce(): initializing with /Users/ar/workspace/work/KBs
KBmanager.readConfiguration()
KBmanager.serializedExists(): true
KBmanager.serializedOld(config):
KBmanager.serializedOld(config): save date: Thu Nov 28 14:30:02 BRST 2019
Info in KBmanager.initializeOnce(): reading from sources
Info in KBmanager.setConfiguration():
Error in KBmanager.preferencesFromXML(): Adding: sumokbname SUMO
Error in KBmanager.preferencesFromXML(): Adding: testOutputDir /Users/ar/workspace/work/KBs/tests
Error in KBmanager.preferencesFromXML(): Adding: TPTPDisplay no
Error in KBmanager.preferencesFromXML(): Adding: inferenceEngine /Users/ar/workspace/E/PROVER/e_ltb_runner
Error in KBmanager.preferencesFromXML(): Adding: inferenceTestDir /Users/ar/workspace/work/KBs/tests
Error in KBmanager.preferencesFromXML(): Adding: baseDir /Users/ar/workspace
Error in KBmanager.preferencesFromXML(): Adding: hostname localhost
Error in KBmanager.preferencesFromXML(): Adding: logLevel warning
Error in KBmanager.preferencesFromXML(): Adding: systemsDir /Users/ar/workspace/sigma/sigma
Error in KBmanager.preferencesFromXML(): Adding: userBrowserLimit 25
Error in KBmanager.preferencesFromXML(): Adding: adminBrowserLimit 200
Error in KBmanager.preferencesFromXML(): Adding: https false
Error in KBmanager.preferencesFromXML(): Adding: SemRewrite /Users/ar/workspace/sumo/WordNetMappings/SemRewrite.txt
Error in KBmanager.preferencesFromXML(): Adding: eproverPath /Users/workspace/E/EPROVER/eprover
Error in KBmanager.preferencesFromXML(): Adding: nlpTools yes
Error in KBmanager.preferencesFromXML(): Adding: graphWidth 600
Error in KBmanager.preferencesFromXML(): Adding: typePrefix yes
Error in KBmanager.preferencesFromXML(): Adding: graphDir graph
Error in KBmanager.preferencesFromXML(): Adding: TPTP yes
Error in KBmanager.preferencesFromXML(): Adding: cache no
Error in KBmanager.preferencesFromXML(): Adding: editorCommand
Error in KBmanager.preferencesFromXML(): Adding: graphVizDir /usr/bin
Error in KBmanager.preferencesFromXML(): Adding: kbDir /Users/ar/workspace/work/KBs
Error in KBmanager.preferencesFromXML(): Adding: loadCELT no
Error in KBmanager.preferencesFromXML(): Adding: celtdir
Error in KBmanager.preferencesFromXML(): Adding: lineNumberCommand
Error in KBmanager.preferencesFromXML(): Adding: prolog
Error in KBmanager.preferencesFromXML(): Adding: port 8080
Error in KBmanager.preferencesFromXML(): Adding: tptpHomeDir /Users/ar/workspace/sigma/sigma
Error in KBmanager.preferencesFromXML(): Adding: showcached no
Error in KBmanager.preferencesFromXML(): Adding: leoExecutable
Error in KBmanager.preferencesFromXML(): Adding: holdsPrefix no
Error in KBmanager.preferencesFromXML(): Adding: logDir /Users/ar/workspace/work/logs
Error in KBmanager.preferencesFromXML(): Bad tag: kb
KBmanager.loadKB(): add constituent /Users/ar/workspace/sumo/Merge.kif to SUMO
INFO in KB.addConstituent(): /Users/ar/workspace/sumo/Merge.kif
........................................................................................................................................................................................INFO in KB.addConstituent(): added 5043 formulas and 1207 terms.
INFO in KB.addConstituent(): /Users/ar/workspace/sumo/Merge.kif loaded in seconds: 0
KBmanager.buildCaches(): buildInsts seconds: 0
KBmanager.buildCaches(): buildRelationsSet seconds: 0
KBmanager.buildCaches(): buildTransitiveRelationsSet seconds: 0
KBmanager.buildCaches(): buildParents seconds: 0
KBmanager.buildCaches(): buildChildren seconds: 0
KBmanager.buildCaches(): collectDomains seconds: 0
KBmanager.buildCaches(): buildInstTransRels seconds: 0
KBmanager.buildCaches(): buildDirectInstances seconds: 0
KBmanager.buildCaches(): addTransitiveInstances seconds: 0
INFO in KBcache.buildTransInstOf(): f: (instance exhaustiveAttribute Predicate)
INFO in KBcache.buildTransInstOf(): f: (instance exhaustiveAttribute VariableArityRelation)
KBmanager.buildCaches(): buildTransInstOf seconds: 0
KBmanager.buildCaches(): buildExplicitDisjointMap seconds: 0
buildDisjointMap():  0.15 seconds to process 344432 entries
KBmanager.buildCaches(): buildDisjointMap seconds: 0
KBmanager.buildCaches(): buildFunctionsSet seconds: 0
INFO in KBcache.writeCacheFile(): SUMO_Cache.kif
KBcache.writeCacheFile(): done writing cache file, in seconds: 0
INFO in KB.addConstituent(): /Users/ar/workspace/sumo/SUMO_Cache.kif
..............................................................................................................................................................................................................................................INFO in KB.addConstituent(): added 7409 formulas and 1190 terms.
INFO in KB.addConstituent(): /Users/ar/workspace/sumo/SUMO_Cache.kif loaded in seconds: 0
KBcache.writeCacheFile(): add cache file, in seconds: 0
KBmanager.buildCaches(): writeCacheFile seconds: 0
INFO in KBcache.buildCaches(): size: 523
INFO in KB.checkArity(): Performing Arity Check
KBmanager.loadKB(): seconds: 1

sorry, you're right, it's ignored now and I forget I changed that. Many things other than TPTP translation depend on caching. But I should be able to make that switch work for TPTP. I'll check back in a few hours

there's a very easy fix. I've pushed new code (untested) so that if caching is not set to yes, then TPTP code won't be generated. Please do a pull and let me know if it works for you

won't be generated for the cached axiom I mean

OK, the new TPTP output does not contain the obvious contradiction found previously by Vampire. But the code for computing the SUMO_Cache.kif has a bug. Can we use this issue to track this bug?

% grep realization SUMO_Cache.kif
(instance realization AntisymmetricRelation)
...
(instance realization SymmetricRelation)

checking into it....

fix with df5e04f