(define-theory Assessment (Top-Level))
(in-theory 'Assessment)


(DEFINE-RELATION ABSENT-IN (?A ?B) :DEF
 (AND (OR (NOT (PART-OF ?A ?B))
          (NOT (LOCATED ?A ?B))
          (NOT (REFERENCE-LOCATION ?A ?B)))
      (NOT (_INTEGRAL ?B TRUE))
      (ASSESSMENT-RELATION ?A ?B)
      (EXISTS (?C) (AND (CONTEXT ?A ?C) (UNEXPECTED ?C ?B)))))
(DEFINE-RELATION APPROVED-BY (?A ?B) :IFF-DEF
 (AND (= (INVERSE APPROVES) APPROVED-BY) (ENTITY ?A) (*AGENT ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE APPROVED-BY *AGENT)
      (DOMAIN APPROVED-BY ENTITY)))
(DEFINE-RELATION APPROVES (?A ?B)
 "The approval of an entity e is the 
acknowledgement of e made by an expert or a reliable entity."
 :DEF (AND (ASSESSMENT-RELATION ?A ?B) (EVALUATES ?A ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE APPROVES ENTITY)
      (DOMAIN APPROVES SOCIAL-OBJECT)))
(DEFINE-FUNCTION CAUGHT-AT (?A) :-> ?B
 "Relation for talking of something occurring 'subjectively' 
at time t."
 :DEF
 (AND (EXISTS ?X (AND (*AGENT ?X) (AWARE-OF ?X ?A))) (HAPPENS-AT ?A ?B)))
(DEFINE-RELATION CERTIFIED-BY (?A ?B) :IFF-DEF
 (AND (= (INVERSE CERTIFIES) CERTIFIED-BY) (ENTITY ?A) (*AGENT ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE CERTIFIED-BY *AGENT)
      (DOMAIN CERTIFIED-BY ENTITY)))
(DEFINE-RELATION CERTIFIES (?A ?B) :DEF (APPROVES ?A ?B))
(DEFINE-RELATION COMPETES-WITH (?A ?B)
 "Relation for talking of something which allows an 
assessment of competition between two events or situations. Specialized axioms still lack."
 :DEF (PROBABILITY-RELATION ?A ?B) :AXIOM-CONSTRAINTS
 (AND (RANGE COMPETES-WITH TEMPORALIZED-ENTITY)
      (DOMAIN COMPETES-WITH TEMPORALIZED-ENTITY)))
(DEFINE-RELATION CONVENTIONAL-WITHIN (?A ?B)
 "Something is conventional within some cultural domain." :DEF
 (AND (ASSESSMENT-RELATION ?A ?B) (ENTITY ?A) (TOPIC ?B)))
(DEFINE-RELATION CONVENTIONALLY-ASSOCIATED (?A ?B) :IFF-DEF
 (AND (ASSESSMENT-RELATION ?A ?B)
      (EXISTS (?C)
       (AND (CONVENTIONAL-WITHIN ?A ?C) (THE-CONVENTIONAL-DOMAIN ?C ?B)))))
(DEFINE-RELATION EVIDENTIATED-BY (?A ?B) :IFF-DEF
 (= (INVERSE EVIDENTIATES) EVIDENTIATED-BY))
(DEFINE-RELATION EVIDENTIATES (?A ?B)
 "Relation for talking of something which allows an 
assessment of actuality of an event, situation or object."
 :DEF
 (AND (EXISTS ?A (AND (*AGENT ?A) (EXPECTS ?A ?A ?B)))
      (ASSESSMENT-RELATION ?A ?B)))
(DEFINE-RELATION EXCLUDED-BY (?A ?B) :IFF-DEF
 (= (INVERSE EXCLUDES) EXCLUDED-BY))
(DEFINE-RELATION EXCLUDES (?A ?B)
 "Relation for talking of something which allows an assessment 
of exclusion of an event or situation. This is a form of negative dependence: if x then not y."
 :DEF
 (AND (=> (HAS-EXISTENCE ?A TRUE) (NOT (HAS-EXISTENCE ?B TRUE)))
      (PROBABILITY-RELATION ?A ?B))
 :AXIOM-CONSTRAINTS (RANGE EXCLUDES TEMPORALIZED-ENTITY))
(DEFINE-RELATION EXPECTED-FOR (?A ?B) :IFF-DEF
 (= (INVERSE THE-EXPECTED) EXPECTED-FOR))
(DEFINE-RELATION EXPECTS (?A ?B ?C) :DEF
 (AND (CONTEXT-OF ?C ?B) (AWARE-OF ?A ?B) (STRUCTURING-TERNARY ?A ?B ?C))
 :CONSTRAINTS (AND (*AGENT ?A) (ENTITY ?B)) :AXIOM-DEF
 (AND (ARITY EXPECTS 3) (TERNARY EXPECTS)) :AXIOM-CONSTRAINTS
 (RANGE EXPECTS SITUATION))
(DEFINE-FUNCTION HAPPENS-AT (?A) :-> ?B
 "Relation for talking of something occurring 'objectively' 
at time t. It might be redundant, since, for most uses, the function trueime-value' in 
theory:time should be enough."
 :DEF (AND (EXISTS ?U (THE-TIME-UNIT ?U ?B)) (TIME-VALUE ?A ?B)))
(DEFINE-RELATION HAS-ABSENCE (?A ?B) :IFF-DEF
 (= (INVERSE ABSENT-IN) HAS-ABSENCE))
(DEFINE-RELATION HAS-COMPETITOR (?A ?B) :IFF-DEF
 (= (INVERSE COMPETES-WITH) HAS-COMPETITOR))
(DEFINE-RELATION HAS-ISSUE (?A ?B) :IFF-DEF
 (= (INVERSE ISSUE-IN) HAS-ISSUE))
(DEFINE-RELATION HAS-PRESENCE (?A ?B) :IFF-DEF
 (= (INVERSE PRESENT-IN) HAS-PRESENCE))
(DEFINE-RELATION HAS-UNEXPECTED-SITUATION (?A ?B) :IFF-DEF
 (= (INVERSE UNEXPECTED) HAS-UNEXPECTED-SITUATION))
(DEFINE-RELATION ISSUE-IN (?A ?B)
 "Is an issue in or a point of discussion, study, debate, or 
dispute."
 :DEF (ASSESSMENT-RELATION ?A ?B))
(DEFINE-RELATION MADE-LIKELY-BY (?A ?B) :IFF-DEF
 (= (INVERSE MAKES-LIKELY) MADE-LIKELY-BY))
(DEFINE-RELATION MAKES-LIKELY (?A ?B)
 "Relation for talking of something which allows an 
assessment of likelihood of an event or situation. Specialized axioms still lack."
 :DEF (AND (_ACTUAL ?A TRUE) (_EPISTEMIC ?B TRUE) (PROBABILITY-RELATION ?A ?B))
 :AXIOM-CONSTRAINTS (RANGE MAKES-LIKELY TEMPORALIZED-ENTITY))
(DEFINE-RELATION MEASURED-BY (?A ?B) :IFF-DEF
 (= (INVERSE MEASURES) MEASURED-BY))
(DEFINE-RELATION MEASURES (?A ?B)
 "Ascertains or marks the dimensions, quantity, degree, 
or capacity of."
 :DEF (ASSESSMENT-RELATION ?A ?B) :AXIOM-DEF
 (MAPPING MEASURES
  "Entry from USN. This is a metonymic notion, meaning that some
activity helps (analogical) measuring of some entity.")
 :AXIOM-CONSTRAINTS
 (AND (RANGE MEASURES ENTITY)
      (DOMAIN MEASURES ACTIVITY)))
(DEFINE-RELATION PRESENT-IN (?A ?B) :DEF
 (AND (OR (PART-OF ?A ?B) (LOCATED ?A ?B) (REFERENCE-LOCATION ?A ?B))
      (ASSESSMENT-RELATION ?A ?B)
      (EXISTS (?C) (AND (CONTEXT ?A ?C) (UNEXPECTED ?C ?B)))))
(DEFINE-RELATION RELEVANCE-DOMAIN-OF (?A ?B) :IFF-DEF
 (AND (= (INVERSE RELEVANT-FOR) RELEVANCE-DOMAIN-OF)
      (ENTITY ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE RELEVANCE-DOMAIN-OF ENTITY)
      (DOMAIN RELEVANCE-DOMAIN-OF ENTITY)))
(DEFINE-RELATION RELEVANT-FOR (?A ?B)
 "Something is relevant for something else when they are 
interpreted by someone within a cultural domain."
 :DEF (AND (ASSESSMENT-RELATION ?A ?B) (CONVENTIONALLY-ASSOCIATED ?A ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE RELEVANT-FOR ENTITY)
      (DOMAIN RELEVANT-FOR ENTITY)))
(DEFINE-RELATION REPORTED-BY (?A ?B) :IFF-DEF
 (= (INVERSE REPORTS) REPORTED-BY))
(DEFINE-RELATION REPORTS (?A ?B)
 "The reporting of a given situation s is the description 
of s made in a text."
 :DEF (ASSESSMENT-RELATION ?A ?B) :AXIOM-CONSTRAINTS
 (AND (RANGE REPORTS SITUATION)
      (DOMAIN REPORTS TEXT)))
(DEFINE-RELATION THE-CONVENTIONAL-DOMAIN (?A ?B) :IFF-DEF
 (= (INVERSE CONVENTIONAL-WITHIN) THE-CONVENTIONAL-DOMAIN))
(DEFINE-FUNCTION THE-EXPECTATION-OF (?A ?B) :-> ?C
 "This is defined as the functional counterpart of
'expects'. It can be used when a situation is epistemically subjective (cf Searle)."
 :DEF (EXPECTS ?A ?B ?C) :AXIOM-DEF
 (AND (ARITY THE-EXPECTATION-OF 3)
      (FUNCTION THE-EXPECTATION-OF)
      (TERNARY THE-EXPECTATION-OF)))
(DEFINE-FUNCTION THE-EXPECTED (?A) :-> ?B
 "This function can be used when a situation is 
epistemically objective (cf Searle), or when we can consider it so (say, neutralizing 
the interpreter). This should be read as truehe expected state of affairs of the
entity is the situation such and such'."
 :DEF
 (AND (NOT (EXISTS ?Z (AND (*AGENT ?Z) (NOT (EXPECTS ?Z ?A ?B)))))
      (TYPICALITY-RELATION ?A ?B))
 :AXIOM-DEF (FUNCTION THE-EXPECTED) :AXIOM-CONSTRAINTS
 (AND (RANGE THE-EXPECTED SITUATION)
      (DOMAIN THE-EXPECTED ENTITY)))
(DEFINE-RELATION TIME-OF-CATCHING-OF (?A ?B) :IFF-DEF
 (= (INVERSE CAUGHT-AT) TIME-OF-CATCHING-OF))
(DEFINE-RELATION TIME-OF-HAPPENING-OF (?A ?B) :IFF-DEF
 (= (INVERSE HAPPENS-AT) TIME-OF-HAPPENING-OF))
(DEFINE-RELATION UNEXPECTED (?A ?B) :DEF
 (AND (EXISTS ?Z
       (AND (SITUATION ?A)
            (SITUATION ?Z)
            (DIFFERENT ?A ?Z)
            (EXPECTED-FOR ?Z ?B)))
      (TYPICALITY-RELATION ?A ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE UNEXPECTED ENTITY)
      (DOMAIN UNEXPECTED SITUATION)))
(DEFINE-RELATION _ABORTED (?A ?B)
 "A process aborts when it does not reach a certain 
expected result."
 :DEF
 (AND (NOT (EXISTS (?Y ?Z)
            (AND (ENTITY ?Y)
                 (SITUATION ?Z)
                 (OUTCOME-OF ?Y ?A)
                 (EXISTS (?C)
                  (AND (THE-EXPECTED ?Y ?C) (IDENTITY ?Z ?C))))))
      (TYPICALITY-PROPERTY ?A ?B)
      (PROCESS ?A)))
(DEFINE-RELATION _CONCLUDED (?A ?B)
 "A process is concluded when it has reached a 
(whatever) result."
 :DEF
 (AND (EXISTS ?Y (AND (ENTITY ?Y) (OUTCOME-OF ?Y ?A)))
      (TYPICALITY-PROPERTY ?A ?B)
      (PROCESS ?A)))
(DEFINE-RELATION _CONCLUSIVE (?A ?B)
 "A process is conclusive when it is expected to reach a 
(whatever) result."
 :DEF (AND (TYPICALITY-PROPERTY ?A ?B) (PROCESS ?A)))
(DEFINE-RELATION _FORMAL (?A ?B) :DEF (LOGICAL-PROPERTY ?A ?B))
(DEFINE-RELATION _FULFILLED (?A ?B)
 "A process is fulfilled when it has reached an expected 
result."
 :DEF
 (AND (EXISTS (?Y ?Z)
       (AND (ENTITY ?Y)
            (SITUATION ?Z)
            (OUTCOME-OF ?Y ?A)
            (EXISTS (?C) (AND (THE-EXPECTED ?Y ?C) (IDENTITY ?Z ?C)))))
      (TYPICALITY-PROPERTY ?A ?B)
      (PROCESS ?A)))
(DEFINE-RELATION _INFORMAL (?A ?B)
 "Property for talking of something which approximate the 
syntactic structure of a model (a graph or else) but does not obey to a formal semantics."
 :IFF-DEF (AND (NOT (_FORMAL ?A ?B)) (LOGICAL-PROPERTY ?A ?B)))
(DEFINE-RELATION _INTEGRAL (?A ?B)
 "Something is integral when no essential part is absent." :DEF
 (AND (FORALL ?P (=> (PART-OF ?P ?A) (HAS-EXISTENCE ?P TRUE)))
      (TYPICALITY-PROPERTY ?A ?B)))
(DEFINE-RELATION _INTERRUPTED (?A ?B)
 "A process is interrupted when it has not reached a 
(whatever) result."
 :DEF
 (AND (NOT (EXISTS (?Y) (AND (ENTITY ?Y) (OUTCOME-OF ?Y ?A))))
      (TYPICALITY-PROPERTY ?A ?B)
      (PROCESS ?A)))
(DEFINE-RELATION _STRUCTURED (?A ?B)
 "Property for talking of something which has been provided 
with an ordering induced by some relation, not necessarily explicited. For example, both 
an informal classification and a logical model have this property."
 :DEF (LOGICAL-PROPERTY ?A ?B))