Need of AssignmentFn

[nordlow]

Why is AssignmentFn at all needed in axioms such as

(=>
   (and
      (range ?FUNCTION ?CLASS)
      (equal (AssignmentFn ?FUNCTION @ROW) ?VALUE))
   (instance ?VALUE ?CLASS))

instead of plain (?FUNCTION @ROW) when there's already the two axioms

(=>
  (and
    (instance ?FUNCTION UnitOfMeasureMultiplier)
    (instance ?UNIT CompositeUnitOfMeasure))
  (instance (?FUNCTION ?UNIT) CompositeUnitOfMeasure))

(=>
  (and
    (instance ?FUNCTION UnitOfMeasureMultiplier)
    (instance ?UNIT NonCompositeUnitOfMeasure))
  (instance (?FUNCTION ?UNIT) NonCompositeUnitOfMeasure))

using ?FUNCTION ?UNIT instead of (AssignmentFn ?FUNCTION ?UNIT) when predicate variables all are applied using the direct syntax (?REL ...) as in

(=>
   (instance ?REL SymmetricRelation)
   (forall (?INST1 ?INST2)
      (=>
         (?REL ?INST1 ?INST2)
         (?REL ?INST2 ?INST1))))

And why is this function called AssignmentFn instead of, as I would expect, ApplyFn?

[arademaker]

The first one looks more general and the two others are more specific. Anyway, AssignmentFn is used a few times in SUMO, only for giving partial definitions of OneToOneFunctions, AssociativeFunction, and CommutativeFunction. Partial because OneToOneFunction is defined only for unary functions and associative/commutative only for binary functions.

See http://sigma.ontologyportal.org:8080/sigma/Browse.jsp?kb=SUMO&lang=EnglishLanguage&flang=SUO-KIF&term=AssignmentFn

But you are right, the first could possibly be written as below but that would introduce yet another complication in the transformations for TPTP. Variables in the position of functions. We do have variables as predicates, but not as functions. Maybe that is the reason for the AssignmentFn, a similar solution would be the holds predicate used previous.

(=>
   (and
      (range ?FUNCTION ?CLASS)
      (equal (?FUNCTION @ROW) ?VALUE))
   (instance ?VALUE ?CLASS))

or more directly

(=>
  (range ?FUNCTION ?CLASS)
  (instance (?FUNCTION @ROW) ?CLASS))

[nordlow]

But you are right, the first could possibly be written as below but that would introduce yet another complication in the transformations for TPTP.

Can you elaborate on what you mean by this "complication"?

Isn't

(?FUNCTION @ROW)

directly translatable to TPTP? If wo, why? Is there some theoretical motvation for this?

[arademaker]

It depends on what you mean by "directly translatable"... ;-) In this paper (Section 6 Figure 5) you will see that only predicate variable is mentioned. I am not sure if the translation can deal with a variable in the position of function symbol. Maybe @apease can add something here.

[apease]

only Predicate(s) are allows for predicate variables (therefore, not Function(s) ). The use of "holds" was an older solution (roughly 15 years old) that I've abandoned, because most theorem provers give special indexing status to the predicate, so using holds results in poor inference performance. Sigma substitutes all predicates that fit the type constraints in an axiom. However, it should be possible to expand Sigma's KIF to TPTP translation to allow for function substitution, at least if there were a strong motivation to do this, given that it would take some time to implement. It haven't given that a great deal of thought yet however.

[nordlow]

Can you explain what you mean by "Giving special indexing status to the predicate"? I assume you are talking about hash tables of some sort. If so, what are the key types and value types in those tables?

[arademaker]

He is just saying that theorem provers usually index all axioms they load by the predicates mentioned on them. This is for fast performance once they need to select the axiom to use on each resolution step. But the use of holds predicate breaks the indexing heuristics.

[nordlow]

I see. Thanks!

[arademaker]

So we need to be concrete here. The assingmentFn is not an error. It could be avoided if my interpretation is right, allowing variables in functional symbols position. As @apease said, we need good arguments for introducing variables as functions. So I vote to close this issue for now.