Class PARTICIPANT-FUNCTION

• Defined in theory: Cml
• Source code: cml.lisp

Slots on this class:

Documentation:

A participant function is a unary function from model fragments to entities.

Instance-Of: Class

Subclass-Of: Unary-function

Domain-Of: Participant-function-total-on

Range-Of: Has-participant-function

---

Slots on instances of this class:

Domain: Model-fragment

Range: Entity

Equivalence Axioms:

(<=> (Participant-Function ?F)
     (And (Unary-Function ?F)
          (Domain ?F Model-Fragment)
          (Range ?F Entity)))

Axioms:

(Unary-Function ?F)

Other Related Axioms:

(<= (Range $X Entity) (Participant-Function $X))

(<= (Domain $X Model-Fragment) (Participant-Function $X))

(<=> (Participant-Function ?F)
     (And (Unary-Function ?F)
          (Domain ?F Model-Fragment)
          (Range ?F Entity)))

(=> (Has-Participant-Function $X $Y) (Participant-Function $Y))

(=> (Participant-Function-Total-On $X $Y) (Participant-Function $X))

(<=> (Participant-Function-Total-On ?Function ?Class)
     (And (Participant-Function ?Function)
          (Class ?Class)
          (Total-On ?Function ?Class)))