(define-theory Equality (kif-sets frame-ontology))
(in-theory 'Equality)


(DEFINE-RELATION CONCEPTUALLY-DIFFERENT (?A ?B)
 "This is conceptual non-identity, say it implies
that a meta-thing (predicate) R1 holding for the entity x is different
from a meta-thing R2 holding for the entity y. Typically, this relation is
used for defining special subrelations (eg, substantially-different, formally-
different, etc.). Other uses may arise in defining semantic field relations
(completely irrelated, contrary, converse, etc.)."
 :DEF
 (AND (EXISTS (?C1 ?C2)
       (AND (HOLDS-TRUE-2 ?C1 ?A)
            (HOLDS-TRUE-2 ?C2 ?B)
            (NOT (IDENTITY ?C1 ?C2))))
      (EQUALITY-RELATION ?A ?B)))
(DEFINE-RELATION DIFFERENT (?A ?B)
 "This is a generic non-identity, mainly useful
to functional expressions; for specialized equality/difference see other concepts
in this context."
 :DEF (AND (NOT (IDENTITY ?A ?B)) (EQUALITY-RELATION ?A ?B)))
(DEFINE-RELATION EQUAL-BUT-LOCALIZATION (?A ?B) :DEF
 (AND (OR (NOT (EXISTS (?C ?D)
                (AND (REGION-OF ?B ?D) (REGION-OF ?A ?C) (IDENTITY ?C ?D))))
          (NOT (EXISTS (?E ?F)
                (AND (ABSCISSA-VALUE ?B ?F) (ABSCISSA-VALUE ?A ?E) (= ?E ?F))))
          (NOT (EXISTS (?G ?H)
                (AND (ORDINATE-VALUE ?B ?H)
                     (ORDINATE-VALUE ?A ?G)
                     (= ?G ?H)))))
      (EQUALITY-RELATION ?A ?B)))
(DEFINE-RELATION EQUAL-BUT-TIME (?A ?B) :DEF
 (AND (OR (NOT (EXISTS (?C ?D)
                (AND (TIME-VALUE ?B ?D) (TIME-VALUE ?A ?C) (= ?C ?D))))
          (NOT (EXISTS (?E ?F)
                (AND (DURATION-VALUE ?B ?F)
                     (DURATION-VALUE ?A ?E)
                     (= ?E ?F)))))
      (EQUALITY-RELATION ?A ?B)))