search

own-pt / cl-krr

Environment for knowledge representation, reasoning, and engineering.
Apache License 2.0
4 stars 3 forks source link

superfluous axioms #27

Open arademaker opened 4 years ago

arademaker commented 4 years ago 
/*
(forall (?ROW0 ?ROW1 ?ROW2)
 (=> (and (instance ?ROW1 Class) (instance ?ROW0 Class) (instance ?ROW2 Class))
  (=>
   (and (subrelation exhaustiveDecomposition exhaustiveDecomposition)
    (and (instance exhaustiveDecomposition Predicate)
     (and (instance exhaustiveDecomposition Predicate)
      (exhaustiveDecomposition3 ?ROW0 ?ROW1 ?ROW2))))
   (exhaustiveDecomposition3 ?ROW0 ?ROW1 ?ROW2))))
*/
fof(a31410,axiom,! [ROW0,ROW1,ROW2] : (((s_instance(ROW1, s_Class) & s_instance(ROW0, s_Class) & s_instance(ROW2, s_Class)) => ((s_subrelation(s_exhaustiveDecomposition_m, s_exhaustiveDecomposition_m) & (s_instance(s_exhaustiveDecomposition_m, s_Predicate) & (s_instance(s_exhaustiveDecomposition_m, s_Predicate) & s_exhaustiveDecomposition3(ROW0, ROW1, ROW2)))) => s_exhaustiveDecomposition3(ROW0, ROW1, ROW2))))).
arademaker commented 4 years ago

Investigating this error, I found a new problem. The function that looks for predicate variables is considering that the two axioms below contain predicate variables:

(=>
 (and
  (instance ?Bond CallableBond)
  (currentAccountBalance (AccountFn ?Bond) ?Date ?Amount)
  (callDate ?Bond ?Date))
 (amountDue (AccountFn ?Bond) ?Amount ?Date))

(=>
 (albumRelease ?A ?T)
 (and
  (exists (?R1 ?DS1)
   (releaseForSale (AlbumCopiesFn ?A ?DS1) ?R1 ?T))
  (not
   (exists (?B ?R2 A?DS2)
    (and
     (before ?B ?T)
     (releaseForSale
      (AlbumCopiesFn ?A ?DS2) ?R2 ?B))))))

The problem is in the way the fuction map-fold and find-vars operate. They should maintain a context during the parsing of the axiom.

arademaker commented 4 years ago

Once this is solved, we must take care to not substitute different predicate variables in the same axiom by the same predicate symbol.