VirusProteinAndCellPart causes error in eprover

[kharus]

Steps to reproduce

  <kb name="SUMO" >
    <constituent filename="Merge.kif" />
    <constituent filename="VirusProteinAndCellPart.kif" />
  </kb>

JAVA_HOME/bin/java -Xmx6G -classpath "$SIGMA_SRC/build/classes:$SIGMA_SRC/build/lib/*" com.articulate.sigma.KB -ae "(subclass ?X Object)"
....
completed query with result: Problem: s__catalyst 7 != 4

$ ~/Programs/E/PROVER/e_ltb_runner --interactive ~/.sigmakee/KBs/EBatchConfig.txt ~/Programs/E/PROVER/eprover
# Parsing /home/ruslan/.sigmakee/KBs/SUMO.tptp
Problem: s__catalyst 7 != 4
e_ltb_runner: /home/ruslan/.sigmakee/KBs/SUMO.tptp:519:(Column 289):s__catalyst used with arity 7, but registered with arity 4
$  awk 'NR==519' /home/ruslan/.sigmakee/KBs/SUMO.tptp
fof(kb_SUMO_246,axiom,(( ( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__ROW2,V__NUMBER,V__CLASS] : (((s__instance(V__NUMBER,s__PositiveInteger) & s__instance(V__CLASS,s__SetOrClass)) => (((s__domain(s__catalyst__m,V__NUMBER,V__CLASS) & s__instance(s__catalyst__m,s__Predicate) & s__catalyst(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)) => (s__instance(s__ListOrderFn(s__ListFn__6Fn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8),V__NUMBER),V__CLASS))))) ) ) ))).
$ awk 'NR==519' /home/ruslan/.sigmakee/KBs/SUMO.tptp | cut -b 289-
s__catalyst(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)) => (s__instance(s__ListOrderFn(s__ListFn__6Fn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8),V__NUMBER),V__CLASS))))) ) ) ))).

Vampire works fine, maybe the issue is in eprover itself.

[kharus]

Similar issue with Media.kif

  <kb name="SUMO" >
    <constituent filename="Media.kif" />
    <constituent filename="Merge.kif" />
  </kb>

$ ~/Programs/E/PROVER/e_ltb_runner --interactive ~/.sigmakee/KBs/EBatchConfig.txt ~/Programs/E/PROVER/eprover
# Parsing /home/ruslan/.sigmakee/KBs/SUMO.tptp
Problem: s__holdsDuring 7 != 2
e_ltb_runner: /home/ruslan/.sigmakee/KBs/SUMO.tptp:1909:(Column 352):s__holdsDuring used with arity 7, but registered with arity 2
$ awk 'NR==1909' /home/ruslan/.sigmakee/KBs/SUMO.tptp
fof(kb_SUMO_1513,axiom,(( ( ! [V__ARG] : ((s__instance(V__ARG,s__PositiveInteger) => (((s__exactCardinality(s__holdsDuring__m,V__ARG,n__1) & s__instance(s__holdsDuring__m,s__Predicate)) => (( ? [V__X, V__ARGS2, V__ARGS3, V__ARGS4, V__ARGS5, V__ARGS6, V__ARGS7, V__ARGS8] : ((s__instance(V__ARGS2,s__TimePosition) & s__instance(V__ARGS3,s__Formula) & (s__holdsDuring(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7,V__ARGS8) & (V__X = s__ListOrderFn(s__ListFn__6Fn__7Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7,V__ARGS8),V__ARG)) & ~(( ? [V__Y] : (((V__Y = s__ListOrderFn(s__ListFn__6Fn__7Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7,V__ARGS8),V__ARG)) & ~((V__X = V__Y)))))))))))))) ) ) ))).
$ awk 'NR==1909' /home/ruslan/.sigmakee/KBs/SUMO.tptp | cut -b 352-
s__holdsDuring(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7,V__ARGS8) & (V__X = s__ListOrderFn(s__ListFn__6Fn__7Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7,V__ARGS8),V__ARG)) & ~(( ? [V__Y] : (((V__Y = s__ListOrderFn(s__ListFn__6Fn__7Fn(V__ARGS2,V__ARGS3,V__ARGS4,V__ARGS5,V__ARGS6,V__ARGS7,V__ARGS8),V__ARG)) & ~((V__X = V__Y)))))))))))))) ) ) ))).

[apease]

EProver is being more strict and Vampire more forgiving. In TPTP relations with a different number of arguments cannot have the same name. Sigma relies on declarations of the number of arguments in SUO-KIF to know how many arguments are allowed in the translation to TPTP. The virus ontology was missing that statement for 'catalyst' (instance catalyst BinaryRelation) . I'm puzzled by the issue with holdDuring however, since it's defined in Merge.kif and the axioms above are TPTP translations of axioms from Merge.kif and not Media.kif . holdsDuring is also defined as a BinaryRelation http://sigma.ontologyportal.org:8080/sigma/Browse.jsp?kb=SUMO&lang=EnglishLanguage&flang=SUO-KIF&term=holdsDuring

[arademaker]

I was curious so I tried to confirm using first a very naive approach. I search for all uses of holdsDuring.

(defparameter sumo (reduce (lambda (res fn) 
			     (append res (with-open-file (in fn)
					   (loop for frm = (read in nil nil)
						 while frm
						 collect (cons frm fn))))) 
			   (directory "sumo/*.kif") :initial-value nil))


(defun find-in-tree (item tree &key (test #'eql) (key #'identity))
  (labels ((find-in-tree-aux (tree)
	     (when (consp tree)
	       (when (funcall test item (funcall key tree))
		 (return-from find-in-tree tree))
	       (find-in-tree-aux (car tree))
	       (find-in-tree-aux (cdr tree)))))
    (find-in-tree-aux tree)))

(remove-if (lambda (p) (> (length (car p)) 2)) 
	   (remove-if (lambda (p) (null (car p)))
		      (mapcar (lambda (n)
				(cons (find-in-tree 'holdsduring (car n) :key #'car) (cdr n)))
			      sumo)))

This code basically confirmed that in all occurrences in the kif files the holdsDuring is receiving two arguments. Next I confirmed that our lisp transformation (https://github.com/own-pt/cl-krr) only produces one predicate for the holdDuring, the s_holdsDuring. So it recognizes that it is fixed arity relation, binary one.

[apease]

yes, holdDuring is in fact binary. However, it shouldn't appear at all in the TPTP output since it's a relation that takes a Formula as an argument, which is beyond first order, and therefore can't appear in TPTP. My code should be trapping it.

[apease]

one additional clarification @kharus is that the holdDuring axiom that you're seeing is generated automatically by expanding a rule with a variable in the predicate position, and then expanding row variables so that rule doesn't actually appear in any SUO-KIF source file. But it does indicate a bug in the code that translates to TPTP (and one that I must have introduced relatively recently since Vampire was happily doing proofs with the TPTP output previously). Good bug report!