TPTP transformation: can't prove that component is a Predicate

[arademaker]

% f: (instance component BinaryPredicate)
% 13271 of 34530 from file /Users/ar/workspace/sumo/Merge.kif at line 1001
% not higher order
% f: (instance component BinaryRelation)
% 13272 of 34530 from file /Users/ar/workspace/sumo/SUMO_Cache.kif at line 14359
% not higher order
fof(kb_SUMO_4653,axiom,(( s__instance(s__component__m,s__BinaryRelation) ))).

It looks like the SUMO_Cache.kif file is being used to make all instances of BinaryPredicate instances only of BinaryRelation. Is it the right thing to do? I am not sure.

[arademaker]

even after removing the SUMO_Cache.kif file from the repository, the result remains. I can't prove that component is a BinaryPredicate.

[arademaker]

Hi @apease any words about it?

[apease]

I made some changes to the TFF translation that I have to finish testing before I can check this one...

[apease]

works in TFF with Merge.kif -

tff(f2070,axiom,(
  s__instance(s__component__m,s__BinaryRelation)),
  file('/home/apease/.sigmakee/KBs/SUMO.tff',kb_SUMO_2070)).
tff(f5102,conjecture,(
  s__instance(s__component__m,s__BinaryRelation)),
  file('/home/apease/.sigmakee/KBs/SUMO.tff',kb_SUMO_conj)).
tff(f5103,negated_conjecture,(
  ~s__instance(s__component__m,s__BinaryRelation)),
  inference(negated_conjecture,[],[f5102])).
tff(f5141,plain,(
  ~s__instance(s__component__m,s__BinaryRelation)),
  inference(flattening,[],[f5103])).
tff(f7692,plain,(
  ~s__instance(s__component__m,s__BinaryRelation)),
  inference(cnf_transformation,[],[f5141])).
tff(f10593,plain,(
  s__instance(s__component__m,s__BinaryRelation)),
  inference(cnf_transformation,[],[f2070])).
tff(f13534,plain,(
  $false),
  inference(subsumption_resolution,[],[f7692,f10593])).
% SZS output end Proof for SUMO
% ------------------------------
% Version: Vampire 4.2.2 (commit 6588b35 on 2018-07-19 13:39:17 +0200)
% Termination reason: Refutation

% Memory used [KB]: 19061
% Time elapsed: 0.065 s
% ------------------------------
% ------------------------------
% Success in time 0.154 s

[arademaker]

Sorry, what was your query/conjecture?

[apease]

from above -

tff(f5103,negated_conjecture,(
~s__instance(s__component__m,s__BinaryRelation)),
inference(negated_conjecture,[],[f5102])).

but maybe I misunderstood you and you're trying to prove
s__instance(s__component__m,s__BinaryPredicate)

is that the issue?

[arademaker]

My conjecture is

tff(kb_SUMO_999998,conjecture,(s__instance(s__component,s__Predicate)) ).

[arademaker]

For that, I had to add

tff(kb_SUMO_99997,axiom,(s__component = s__component__m) ).

[apease]

we have to keep s__component and s__component__m distinct as I recall since a relation can't be a term in TPTP so I wouldn't suggest making those statements. What you want as a query is tff(kb_SUMO_999998,conjecture,(s__instance(s__component__m,s__Predicate)) )..

In the conversion code in Sigma I translate "component" to s__component__m when it appears as an argument

[apease]

but there does seem to be a problem that a conversion isn't occurring that should be

% f: (instance component BinaryPredicate)
% 6406 of 13113 from file /home/apease/.sigmakee/KBs/Merge.kif at line 1013
% not higher order

(instance component BinaryPredicate) isn't getting translated so I'll have to track down why

[arademaker]

Yep. That was my first comment on this issue!! ;-) The code does not produce this axiom in the TPTP transformation nor in the TFF transformation.

Making the symbols s__component and s__component__m equal doesn't cause any error for Vampire. But my intuition about a possible problem of having those two distinct symbols maybe be wrong and you are probably right on saying that transformation being consistent does not block any reasoning. I will investigate further from my side.

[apease]

sorry you're giving me so many good bug reports I'm losing track a little bit and should slow down and read them more carefully :-)