search

ontologyportal / sigmakee

Sigma Knowledge Engineering Environment
GNU General Public License v3.0
101 stars 34 forks source link

syntax error while reading generated TPTP #7

Closed fcbr closed 5 years ago

fcbr commented 8 years ago

After setting the cache to true (issue #5) and filterSimpleOnly to false (issue #6), one is able to convert SUMO to TPTP fully. However a few axioms fail to load in E. Here's the error:

e_ltb_runner: /home/fcbr/repos/sumo/sumo/SUMO.tptp:2136:(Column 165):
(just read '='): Closing bracket (')') expected, but Equal Predicate/Sign ('=') read

which comes from this line:

fof(kb_SUMO_2131,axiom,(( ( ! [V__ROW1,V__NUMBER] :
((s__instance(V__ROW1,s__Number) & s__instance(V__NUMBER,s__Quantity))
=> ((s__LeastCommonMultipleFn_1(V__ROW1) = V__NUMBER) => (!
[V__ELEMENT] : ((s__instance(V__ELEMENT,s__Quantity)) =>
(s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) =>
(s__RemainderFn(V__NUMBER,V__ELEMENT) = 0)))))) ) ))).
fcbr commented 8 years ago

Here are the four axioms that E had trouble parsing:

fof(kb_SUMO_2127,axiom,(( ( ! [V__ROW1,V__NUMBER] : ((s__instance(V__ROW1,s__Number) & s__instance(V__NUMBER,s__Quantity)) => ((s__GreatestCommonDivisorFn_1(V__ROW1) = V__NUMBER) => (! [V__ELEMENT] : ((s__instance(V__ELEMENT,s__Quantity)) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__ELEMENT,V__NUMBER) = 0)))))) ) ))).
fof(kb_SUMO_2128,axiom,(( ( ! [V__ROW1,V__NUMBER] : ((s__instance(V__ROW1,s__Number) & s__instance(V__NUMBER,s__Quantity)) => ((s__GreatestCommonDivisorFn_1(V__ROW1) = V__NUMBER) => (~ (? [V__GREATER] : (s__instance(V__GREATER,s__Quantity) & (greater(V__GREATER,V__NUMBER) & (! [V__ELEMENT] : ((s__instance(V__ELEMENT,s__Quantity)) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__ELEMENT,V__GREATER) = 0)))))))))) ) ))).
fof(kb_SUMO_2131,axiom,(( ( ! [V__ROW1,V__NUMBER] : ((s__instance(V__ROW1,s__Number) & s__instance(V__NUMBER,s__Quantity)) => ((s__LeastCommonMultipleFn_1(V__ROW1) = V__NUMBER) => (! [V__ELEMENT] : ((s__instance(V__ELEMENT,s__Quantity)) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__NUMBER,V__ELEMENT) = 0)))))) ) ))).
fof(kb_SUMO_2132,axiom,(( ( ! [V__ROW1,V__NUMBER] : ((s__instance(V__ROW1,s__Number) & s__instance(V__NUMBER,s__Quantity)) => ((s__LeastCommonMultipleFn_1(V__ROW1) = V__NUMBER) => (~ (? [V__LESS] : (s__instance(V__LESS,s__Quantity) & (less(V__LESS,V__NUMBER) & (! [V__ELEMENT] : ((s__instance(V__ELEMENT,s__Quantity)) => (s__inList(V__ELEMENT,s__ListFn_1(V__ROW1)) => (s__RemainderFn(V__LESS,V__ELEMENT) = 0)))))))))) ) ))).
fcbr commented 8 years ago

Looks like kb_SUMO_2127 and kb_SUMO_2128 came from the following SUO-KIF:

(=>
   (equal (GreatestCommonDivisorFn @ROW) ?NUMBER)
   (forall (?ELEMENT)
      (=>
         (inList ?ELEMENT (ListFn @ROW))
         (equal (RemainderFn ?ELEMENT ?NUMBER) 0))))
(=>
   (equal (GreatestCommonDivisorFn @ROW) ?NUMBER)
   (not (exists (?GREATER)
      (and
         (greaterThan ?GREATER ?NUMBER)
         (forall (?ELEMENT)
            (=>
               (inList ?ELEMENT (ListFn @ROW))
               (equal (RemainderFn ?ELEMENT ?GREATER) 0)))))))
arademaker commented 8 years ago

@fcbr , in the first comment in this issue It looks like s__RemainderFn was not recognized as a function but as a predicate !

arademaker commented 5 years ago

Kif files changed a lot since 2016. There are new issues regarding the TPTP/FOF transformation, I believe this issue is not relevant anymore.