{
* Module: System-oHome
* ---------------------------------------------------------
* This file has been extracted from a ConceptBase database.
* Copyright is with the respective authors!

* Time extracted: 2019-07-17T10:10:26,080Z (UTC) 
* Active user: jeusfeld@myon
* CBserver version: 8.1.03 (2019-07-11) 
*
}

{$set module=System-oHome}

{ 2018-10-30 12:53:56.361 }

Proposition with 
   attribute
    revsingle : 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)
                ) $
end 

AdditionalConstraints!singleConstraint with 
   comment
    hint : "The attribute {m} of {c} is single-valued. Any instance of {c} may have at most one attribute of category {m}!"
end 

AdditionalConstraints!necConstraint with 
   comment
    hint : "The attribute {m} of {c} is defined necessary. Any instance of {c} must have at least one instance of {d} for the attribute {m}!"
end 

AdditionalConstraints!revsingleConstraint with 
   comment
    hint : "The attribute {m} of {c} is reverse single-valued. Any instance of {d} may have at most one instance of {c} connected to it via an attribute of category {m}!"
end 

{---}

{* Relation type names *}

Proposition with
  attribute
    reflexive:  Proposition;      {* any object is related to itself       *}
    transitive: Proposition;      {* relation is closed under transitivity *}
    symmetric: Proposition;       {* if x rel y then also y rel x          *}
    antisymmetric: Proposition;   {* if x rel y and (y rel x) then x=y *}
    asymmetric: Proposition       {* if x rel y then not y rel x     *}
end



{* A_e(x,m,y) is like (x m y) except that it only considers explicit  *}
{* attributions between x,y. This yields much faster executable code. *}

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) $
  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


{* Define a hint for the asym_IC constraint. This will be used by ConceptBase       *}
{* to generate a customized error message in case of a violation of the constraint. *}
 
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

{---} { 2019-07-17 10:08:31.840 }

DeepTelos in Module  end 

{ -/- }