{
* Module: System-oHome
* ---------------------------------------------------------
* This file has been extracted from a ConceptBase database.
* Copyright is with the respective authors!
* Time extracted: 2020-05-25T11:02:40,350Z (UTC)
* Active user: jeusfeld@myon_amd64_Linux
* CBserver version: 8.1.23 (2020-05-22)
*
}
{$set module=System-oHome}
{ 2020-01-27 13:39:38.186 }
jeusfeld in CB_User end
{---} { 2020-05-25 11:02:39.011 }
Proposition with
attribute
revsingle : Proposition;
revnecessary : Proposition
end
AdditionalConstraints in Class with
constraint
singleConstraint : $ forall c,d/Proposition p/Proposition!single x,m/VAR
P(p,c,m,d) and (x in c) ==>
(
forall a1,a2/VAR
(a1 in p) and (a2 in p) and Ai(x,m,a1) and Ai(x,m,a2) ==>
(a1=a2)
) $;
necConstraint : $ forall c,d/Proposition p/Proposition!necessary x,m/VAR
P(p,c,m,d) and (x in c) ==>
exists y/VAR (y in d) and (x m y) $;
revsingleConstraint : $ forall c,d/Proposition p/Proposition!revsingle y,m/VAR
P(p,c,m,d) and (y in d) ==>
(
forall x1,x2/VAR
(x1 in c) and (x2 in c) and (x1 m y) and (x2 m y) ==>
(x1=x2)
) $;
revnecConstraint : $ forall c,d/Proposition p/Proposition!necessary y,m/VAR
P(p,c,m,d) and (y in d) ==>
exists x/VAR (x in c) and (x m y) $
end
AdditionalConstraints!singleConstraint with
comment
hint : "The attribute/relation {m} of {c} is single-valued (right-unique). Any instance of {c} may have at most one attribute of category {m}!"
end
AdditionalConstraints!necConstraint with
comment
hint : "The attribute/relation {m} of {c} is defined necessary (left-total). Any instance of {c} must have at least one instance of {d} for the attribute {m}!"
end
AdditionalConstraints!revsingleConstraint with
comment
hint : "The attribute/relation {m} of {c} is reverse single-valued (left-unique). Any instance of {d} may have at most one instance of {c} connected to it via an attribute of category {m}!"
end
AdditionalConstraints!revnecConstraint with
comment
hint : "The attribute/relation {m} of {c} is defined reverse necessary (right-total). Any instance of {d} must have at least one instance of {c} for the attribute {m}!"
end
{---} { 2020-05-25 11:02:39.238 }
Proposition with
attribute
reflexive : Proposition;
transitive : Proposition;
symmetric : Proposition;
antisymmetric : Proposition;
asymmetric : Proposition;
irreflexive: Proposition
end
RelationSemantics in Class with
constraint
asym_IC : $ forall AC/Proposition!asymmetric C/Proposition x,y/VAR M/VAR
P(AC,C,M,C) and (x in C) and (y in C) and
(x M y) ==> not (y M x) $;
antis_IC : $ forall AC/Proposition!antisymmetric C/Proposition x,y/VAR M/VAR
P(AC,C,M,C) and (x in C) and (y in C) and
(x M y) and (y M x) ==> (x = y) $;
irref_IC: $ forall x,M/VAR
AC/Proposition!irreflexive C/Proposition
P(AC,C,M,C) and (x in C)
==> not (x M x) $
rule
trans_R : $ forall x,z,y,M/VAR
AC/Proposition!transitive C/Proposition
P(AC,C,M,C) and (x in C) and (y in C) and (z in C) and
A_e(x,M,y) and (y M z) ==> (x M z) $;
refl_R : $ forall x,M/VAR
AC/Proposition!reflexive C/Proposition
P(AC,C,M,C) and (x in C)
==> (x M x) $;
symm_R : $ forall x,y,M/VAR
AC/Proposition!symmetric C/Proposition
P(AC,C,M,C) and (x in C) and (y in C) and
A_e(x,M,y) ==> (y M x) $
end
RelationSemantics!asym_IC with
comment
hint : "The {M} relation of {C} is declared asymmetric. Hence, if (x {M} y) holds, then (y {M} x) may not hold."
end
RelationSemantics!antis_IC with
comment
hint : "The {M} relation of {C} is declared antisymmetric. Hence, (x {M} y) and (y M x) may only hold for x=y."
end
RelationSemantics!irref_IC with
comment
hint : "The {M} relation of {C} is declared irreflexive. Hence, if (x {M} x) may not hold."
end
{---} { 2020-05-25 11:02:39.441 }
Proposition!attribute with
attribute
isTransitiveClosureOf : Proposition!attribute
end
MakeTransitiveSemantics1 in Class with
rule
transR1 : $ forall x,y,MA,MB/VAR
A,B/Proposition!attribute C/Proposition
(B isTransitiveClosureOf A) and
P(A,C,MA,C) and P(B,C,MB,C) and
(x in C) and (y in C) and
(x MA y) ==> (x MB y) $;
transR2 : $ forall x,y,z,MA,MB/VAR
A,B/Proposition!attribute C/Proposition
(B isTransitiveClosureOf A) and
P(A,C,MA,C) and P(B,C,MB,C) and
(x in C) and (y in C) and (z in C) and
(x MA z) and (z MB y) ==> (x MB y) $
end
{---} { 2020-05-25 11:02:40.002 }
MLT_telos in Module end
{---} { 2020-05-25 11:02:40.108 }
XPalette in Class,JavaGraphicalPalette with
contains,defaultIndividual
xx1 : DefaultIndividualGT
contains,defaultLink
xx2 : DefaultLinkGT
contains,implicitIsA
xx3 : ImplicitIsAGT
contains,implicitInstanceOf
xx4 : ImplicitInstanceOfGT
contains,implicitAttribute
xx5 : ImplicitAttributeGT
contains
xx6 : DefaultIsAGT;
xx7 : DefaultInstanceOfGT;
xx8 : DefaultAttributeGT;
xx9 : MetametaGT;
xx10 : SimpleClassGT;
xx11 : MetaClassGT;
xx12 : ClassGT;
xx13 : QueryClassGT
rule
inheritGTs : $ forall gt/JavaGraphicalType pal/JavaGraphicalPalette
(pal isA XPalette) and
(DefaultJavaPalette contains gt)
==> (pal contains gt) $;
inheritDef1 : $ forall gt/JavaGraphicalType pal/JavaGraphicalPalette
(pal isA XPalette) and
(DefaultJavaPalette defaultIndividual gt)
==> (pal defaultIndividual gt) $;
inheritDef2 : $ forall gt/JavaGraphicalType pal/JavaGraphicalPalette
(pal isA XPalette) and
(DefaultJavaPalette defaultLink gt)
==> (pal defaultLink gt) $;
inheritDef3 : $ forall gt/JavaGraphicalType pal/JavaGraphicalPalette
(pal isA XPalette) and
(DefaultJavaPalette implicitIsA gt)
==> (pal implicitIsA gt) $;
inheritDef4 : $ forall gt/JavaGraphicalType pal/JavaGraphicalPalette
(pal isA XPalette) and
(DefaultJavaPalette implicitInstanceOf gt)
==> (pal implicitInstanceOf gt) $;
inheritDef5 : $ forall gt/JavaGraphicalType pal/JavaGraphicalPalette
(pal isA XPalette) and
(DefaultJavaPalette implicitAttribute gt)
==> (pal implicitAttribute gt) $
end
{ -/- }