{
* Module: System-oHome-MLT_telos
* ---------------------------------------------------------
* This file has been extracted from a ConceptBase database.
* Copyright is with the respective authors!
*
* CBserver version: 8.1.23 (2020-05-22) 
*
* -authors: Manfred Jeusfeld, Bernd Neumayr, Joao Paulo A. Almeida, Claudenir M. Fonseca, Victorio Albani Carvalho
* -comment: An attempt to partially formalize MLT with O-Telos/ConceptBase
* -copyright: (C) 2020 by the authors
* -derivedFrom: https://nemo.inf.ufes.br/wp-content/papercite-data/pdf/a_comprehensive_formal_theory_for_multi_level_conceptual_modeling_2017.pdf
* -license: Creative Commons Attribution ShareAlike 4.0 International
}

{$set module=System-oHome-MLT_telos}

{ 2020-05-25 11:02:40.454 }

MLT_telos with 
   comment
    authors : "Manfred Jeusfeld, Bernd Neumayr, Joao Paulo A. Almeida, Claudenir M. Fonseca, Victorio Albani Carvalho";
    copyright : "(C) 2020 by the authors";
    license : "Creative Commons Attribution ShareAlike 4.0 International";
    derivedFrom : "https://nemo.inf.ufes.br/wp-content/papercite-data/pdf/a_comprehensive_formal_theory_for_multi_level_conceptual_modeling_2017.pdf";
    comment : "An attempt to partially formalize MLT with O-Telos/ConceptBase"
end 





ENTITY in TYPE end

TYPE in TYPE,Class isA ENTITY with 
   irreflexive,antisymmetric,single,revsingle
    isPowerTypeOf : TYPE
   reflexive,antisymmetric,transitive
    specializes : TYPE
   single
     categorizes: TYPE;
     disjointlyCategorizes: TYPE;
     completelyCategorizes: TYPE;
     partitions: TYPE
   attribute
    properSpecializes : TYPE
   rule
     d_4: $ forall t1,t2/TYPE (t1 specializes t2) and (t1 <> t2) ==> (t1 properSpecializes t2) $
  comment
    c1 : "approximates definition of D2 of MLT; complement of INDIVIDUAL"
end 

{---}


INDIVIDUAL in TYPE,Class isA ENTITY with 
   constraint
    d_1 : $ forall x/INDIVIDUAL not exists y/ENTITY (y in x) $;
    d_1a : $ forall x/INDIVIDUAL not (x in TYPE) $
  comment
    c_1 : "approximates definition of D1 of MLT"
end 

{---}


TYPEwithINDIVIDUAL in QueryClass isA TYPE with
  constraint
    a_1a: $ (exists x1/INDIVIDUAL (x1 in this)) or (exists t1/TYPEwithINDIVIDUAL (t1 in this)) $
end

TYPEwithoutINDIVIDUAL in QueryClass isA TYPE with
  constraint
    a_1b: $ not (this in TYPEwithINDIVIDUAL) $
end

{---}


TYPE with
  rule
    d_3: $ forall t1,t2/TYPE e/Proposition (t1 specializes t2) and (e in t1) ==> (e in t2) $
  constraint
    d_4a: $ forall t1,t2/TYPE :(t1 specializes t2): ==> (t1 <> t2) $
end

{---}

TYPE with
  rule
    d_6: $ forall t1,t2,t3/TYPE (t1 isPowerTypeOf t2) and (t3 in t1) and not (t3 isA t2) ==> (t3 specializes t2) $;
    d_6a: $ forall t1,t2,t3/TYPE (t3 isPowerTypeOf t1) and (t2 specializes t1)  ==> (t2 in t3) $
end

BasicType in QueryClass,MSFOLrule isA TYPE with
  constraint
    a_1: $ exists x/TYPE (x isPowerTypeOf this) or (this isPowerTypeOf x) $
  comment
    c2: "This is not the same as axiom D7 or T3 respectively. We declare isPowerType explicitely and do not derive it."
end


OrderedType in QueryClass,MSFOLrule isA TYPE with
  constraint
    d_8: $ exists b/BasicType (this specializes b) $
end

OrderlessType in QueryClass,MSFOLrule isA TYPE with
  constraint
    d_8: $ not (this in OrderedType) $
end


RootTYPE in QueryClass,MSFOLrule isA TYPE with
  constraint
    isRoot: $ not exists t/TYPE :(this specializes t): or :(this isA t): $
end

LeafTYPE in QueryClass,MSFOLrule isA TYPE with
  constraint
    isLeaf: $ not exists t/TYPE :(t specializes this): or :(t isA this): $
end

TYPE with
  rule
    catr_1: $ forall t1,t2/TYPE (t1 disjointlyCategorizes t2) ==> (t1 categorizes t2) $;
    catr_2: $ forall t1,t2/TYPE (t1 completelyCategorizes t2) ==> (t1 categorizes t2) $;
    catr_3: $ forall t1,t2/TYPE (t1 partitions t2) ==> (t1 disjointlyCategorizes t2) $;
    catr_4: $ forall t1,t2/TYPE (t1 partitions t2) ==> (t1 completelyCategorizes t2) $
  constraint
    catc_5: $ forall t1,t2,s1,s2/TYPE (t1 isPowerTypeOf t2) and (s1 completelyCategorizes s2) and (s1 specializes t1) ==> (s2 specializes t2) $;
    catc_6: $ forall t1,t2,s1,s2/TYPE (t1 isPowerTypeOf t2) and (s1 categorizes s2) and (s2 specializes t2) ==> (s1 specializes t1) $
end

{---}
TYPE with
  rule
    catr_5: $ forall t1,t2,t3/TYPE (t1 categorizes t2) and (t3 in t1) ==> (t3 specializes t2) $
end
{---}

IncompleteCategorization in QueryClass isA TYPE with
   computed_attribute
    entity : ENTITY
  constraint
    isIncomplete : $ exists t1/TYPE (t1 completelyCategorizes this) and (~entity in this) and
                     not (exists t2/TYPE  (t2 properSpecializes this) and (~entity in t2)) $
end

NondisjointCategorization in QueryClass isA TYPE with
  computed_attribute
    entity: ENTITY;
    type: TYPE
  constraint
    isNondisjoint: $ exists t1,t2/TYPE (t1 disjointlyCategorizes t2) and
                      (this properSpecializes t2) and
                      (~type properSpecializes t2) and (this <> ~type) and 
                      (~entity in ~type) and (~entity in this) $
end


{---}

POWER_Link_GT in JavaGraphicalType,Class with 
   property
    textcolor : "0,0,0";
    edgecolor : "240,50,50";
    edgewidth : "1";
    edgestyle : "ldashed";
    edgeheadshape : "Caret";
    bgcolor : "255,255,255";
    label : "powertype of";
    font: "SansSerif";
    fontsize : "9"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 22
  rule
    gtrule : $ forall a/TYPE!isPowerTypeOf (a graphtype POWER_Link_GT) $
end 

ImplicitGT_isPowerTypeOf in JavaGraphicalType,Class with 
   property
    textcolor : "0,0,0";
    edgecolor : "160,110,110";
    edgewidth : "1";
    edgestyle : "ldashed";
    edgeheadshape : "Caret";
    bgcolor : "255,255,255";
    label : "powertype of";
    font: "SansSerif";
    fontsize : "9"
  priority
    p : 20
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
end

CAT_Link_GT in JavaGraphicalType,Class with 
   property
    textcolor : "0,0,0";
    edgecolor : "50,50,240";
    edgewidth : "1";
    edgestyle : "ldashed";
    edgeheadshape : "Caret";
    bgcolor : "255,255,255";
    label : "categorizes";
    font: "SansSerif";
    fontsize : "9"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 22
  rule
    gtrule : $ forall a/TYPE!categorizes (a graphtype CAT_Link_GT) $
end 

COMPLCAT_Link_GT in JavaGraphicalType,Class with 
   property
    textcolor : "0,0,0";
    edgecolor : "50,50,240";
    edgewidth : "1";
    edgestyle : "ldashed";
    edgeheadshape : "Caret";
    bgcolor : "255,255,255";
    label : "completely categorizes";
    font: "SansSerif";
    fontsize : "9"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 24
  rule
    gtrule : $ forall a/TYPE!completelyCategorizes (a graphtype COMPLCAT_Link_GT) $
end 

DISJCAT_Link_GT in JavaGraphicalType,Class with 
   property
    textcolor : "0,0,0";
    edgecolor : "50,50,240";
    edgewidth : "1";
    edgestyle : "ldashed";
    edgeheadshape : "Caret";
    bgcolor : "255,255,255";
    label : "disjointly categorizes";
    font: "SansSerif";
    fontsize : "9"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 25
  rule
    gtrule : $ forall a/TYPE!disjointlyCategorizes (a graphtype DISJCAT_Link_GT) $
end 

PART_Link_GT in JavaGraphicalType,Class with 
   property
    textcolor : "0,0,0";
    edgecolor : "50,50,240";
    edgewidth : "1";
    edgestyle : "ldashed";
    edgeheadshape : "Caret";
    bgcolor : "255,255,255";
    label : "partitions";
    font: "SansSerif";
    fontsize : "9"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 26
  rule
    gtrule : $ forall a/TYPE!partitions (a graphtype PART_Link_GT) $
end 



SPEC_Link_GT in JavaGraphicalType,Class with 
   property
    bgcolor : "0,50,200";
    textcolor : "0,0,0";
    edgecolor : "0,0,0";
    edgeheadcolor : "255,255,255";
    edgeheadshape : "Arrow";
    edgewidth : "1";
    label : ""
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 23
  rule
    gtrule : $ forall a/TYPE!specializes (a graphtype SPEC_Link_GT) $
end 

INSTOF_GT in JavaGraphicalType,Class with 
   property
    bgcolor : "255,255,255";
    textcolor : "0,0,0";
    edgecolor : "0,0,0";
    edgewidth : "1";
    edgeheadshape : "Caret";
    edgestyle : "ldashed";
    label : "instance of";
    font: "SansSerif";
    fontsize : "9"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 6
  rule
    gtrule : $ forall a/InstanceOf (a graphtype INSTOF_GT) $
end 

INSTOFDEDUCED_GT in JavaGraphicalType,Class with 
   property
    bgcolor : "255,255,255";
    textcolor : "0,0,0";
    edgecolor : "120,120,120";
    edgewidth : "1";
    edgeheadshape : "Caret";
    edgestyle : "ldashed";
    label : "instance of";
    font: "SansSerif";
    fontsize : "9"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 7
end 

ISA_GT in JavaGraphicalType,Class with 
   property
    bgcolor : "100,100,255";
    textcolor : "0,0,0";
    edgecolor : "50,50,240";
    edgeheadcolor : "255,255,255";
    edgeheadshape : "Arrow";
    edgewidth : "1";
    label : ""
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 6
  rule
    gtrule : $ forall a/IsA (a graphtype ISA_GT) $
end 

ISADEDUCED_GT in JavaGraphicalType,Class with 
   property
    bgcolor : "0,50,200";
    textcolor : "0,0,0";
    edgecolor : "120,120,120";
    edgewidth : "1";
    edgestyle : "dashed";
    label : "";
    edgeheadcolor : "255,255,255";
    edgeheadshape : "Arrow"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 7
end 

ATTR_GT in Class,JavaGraphicalType with 
   property
    textcolor : "0,0,0";
    edgecolor : "0,0,0";
    edgewidth : "1";
    font: "SansSerif";
    fontsize : "10";
    bgcolor : "255,255,255,240"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 5
  rule
    gtrule : $ forall x/Proposition!attribute (x graphtype ATTR_GT) $
end 

ATTRDEDUCED_GT in JavaGraphicalType with 
   property
    textcolor : "0,0,0";
    edgecolor : "0,0,0";
    edgewidth : "1";
    edgestyle : "dashed";
    font: "SansSerif";
    fontsize : "10";
    bgcolor : "255,255,255,240"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 7
end 

Individual_GT in Class,JavaGraphicalType with 
   property
    bgcolor : "255,255,255";
    textcolor : "0,0,0";
    linecolor : "0,0,0";
    font: "SansSerif";
    shape : "i5.cb.graph.shapes.Rect";
    size : "resizable";
    linewidth : "1"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBIndividual"
  priority
    pr : 5
  rule
    gtrule : $ forall x/Individual (x graphtype Individual_GT) $
end 

ImplicitGT_specializes in Class,JavaGraphicalType with 
   property
    bgcolor : "0,255,150";
    textcolor : "0,0,0";
    edgecolor : "120,120,120";
    edgewidth : "1";
    label : "";
    edgeheadcolor : "255,255,255";
    edgeheadshape : "Arrow"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBLink"
  priority
    p : 20
end 


TYPE_GT in Class,JavaGraphicalType with 
   property
    bgcolor : "250,250,180";
    textcolor : "0,0,0";
    linecolor : "0,0,0";
    shape : "i5.cb.graph.shapes.Rect";
    size : "resizable";
    font: "SansSerif";
    linewidth : "1"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBIndividual"
  priority
    pr : 24
  rule
    gtrule : $ forall x/TYPE (x graphtype TYPE_GT) $
end 

ENTITY_GT in Class,JavaGraphicalType with 
   property
    bgcolor : "250,255,255";
    textcolor : "0,0,0";
    linecolor : "0,0,0";
    shape : "i5.cb.graph.shapes.Rect";
    size : "resizable";
    font: "SansSerif";
    linewidth : "1"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBIndividual"
  priority
    pr : 22
  rule
    gtrule : $ forall x/ENTITY (x graphtype ENTITY_GT) $
end 

INDIVIDUAL_GT in Class,JavaGraphicalType with 
   property
    bgcolor : "220,220,220";
    textcolor : "0,0,0";
    linecolor : "0,0,0";
    shape : "i5.cb.graph.shapes.Rect";
    size : "resizable";
    font: "SansSerif";
    linewidth : "1"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBIndividual"
  priority
    pr : 26
  rule
    gtrule : $ forall x/INDIVIDUAL (x graphtype INDIVIDUAL_GT) $
end

BasicType_GT in Class,JavaGraphicalType with 
   property
    bgcolor : "210,220,100";
    textcolor : "0,0,0";
    linecolor : "0,0,0";
    shape : "i5.cb.graph.shapes.Rect";
    size : "resizable";
    font: "SansSerif";
    linewidth : "1"
  implementedBy
    implBy : "i5.cb.graph.cbeditor.CBIndividual"
  priority
    pr : 26
  rule
    gtrule : $ forall x/BasicType (x graphtype BasicType_GT) $
end


MLTPalette in Class,JavaGraphicalPalette isA XPalette with 
   palproperty
    bgcolor : "255,255,255";
    longtitle : "MLT"
  contains,implicitInstanceOf
    sp4 : INSTOFDEDUCED_GT
  contains,implicitAttribute
    sp5 : ATTRDEDUCED_GT
  contains,implicitIsA
    sp6 : ISADEDUCED_GT
  contains
    sp7 : ISA_GT;
    sp1 : Individual_GT;
    sp2 : INSTOF_GT;
    sp3 : ATTR_GT;
    mp1: ENTITY_GT;
    mp2: TYPE_GT;
    mp4: INDIVIDUAL_GT;
    mp5: BasicType_GT;
    mp15 : POWER_Link_GT;
    mp16 : SPEC_Link_GT;
    mp17 : ImplicitGT_specializes;
    mp18 : PART_Link_GT;
    mp19 : CAT_Link_GT;
    mp20 : COMPLCAT_Link_GT;
    mp21 : DISJCAT_Link_GT;
    mp22 : ImplicitGT_isPowerTypeOf
end 







{ -/- }