{
* File: DualDeep_Part2.sml
* Author: Michael Schrefl, Bernd Neumayr, Manfred Jeusfeld, Christoph Schuetz
* Created: 27-Jun-2013/M.Jeusfeld (18-Mar-2014/M.Jeusfeld)
* ------------------------------------------------------
* Meta model and axiomatization for multi-level links
* Part 2: Axioms implemented by integrity constraints
*
* requires ConceptBase 7.6 or later
*
* 11-Oct-2013: axioms d1a,dab redundant/deprecated
* 22-Oct-2013: move single/necessary constraints of linkDR to DualDeep_Part2
* 23-Oct-2013: d3a: "nmember(y,d2,f-t)" --> "isa*(y,d2)", d3b: "nmember(x,c2,e-s)" --> "isa*(x,c2)"
* since axioms d2a/d2b already check reduction of potencies
* 25-Oct-2013: d5a,d5b: treat the case that the two A predicates match the same parameters
* 28-Oct-2013: IN instead ISA in axiom i2 (version 1.6 of axioms)
* 14-Nov-2013: additional constraints to forbid cross-over attributes
* 19-Nov-2013: adapt to new version of DDI axioms
* 25-Nov-2013: some renaming and changes to a6: SPEC_t instead ISA_t
* 27-Nov-2013: single formula for a4; split formulas of a6
* 28-Nov-2013: a10a,a10b unified into a10
* 18-Mar-2014: rename the formula labels according to the formula numbers in the paper
*
* The Telos specifications in this file DualDeep_Part2.sml and in
* DualDeep_Part1.sml implement the DDI definitions in table 1
* of the paper
*
* "Dual Deep Instantiation and its ConceptBase Implementation"
* by Bernd Neumayr, Manfred Jeusfeld, Michael Schrefl, and Christoph Schuetz
*
* The definitions and formulas marked by =(i)= refer to the respective entry in that
* table.
* In the old (now obsolete) numbering scheme, we used the following constraint labels
* old new
* a1 --> a12
* a2 --> a22
* a3a --> a13
* a3b --> a23
* a4 --> a24
* a5 --> a14
* a6a --> a15
* a6b --> a16
* a7a --> a26
* a7b --> a27
* a8a --> a28
* a8b --> a29
* a9a --> a30
* a9b --> a31
* a10 --> a25
*
}
{*
This source file is licensed under a
Creative Commons Attribution-ShareAlike 3.0 license.
You may use the files if you attribute your work to our work.
And you may alter our work if you make it available under
the same or similar license.
http://creativecommons.org/licenses/by-sa/3.0/
*}
{* =(1)= }
OBJECT!link with
single,necessary {* multiplicity constraints for the attributes of link *}
sourcelevel: Integer;
targetlevel: Integer
necessary {* allow for multiple labels in future extensions *}
label: ALABEL
end
DDI_SyntacticRestrictions in Class with
constraint
{* =(12)= acyclicity of isa+ *}
a12: $ forall x,c/OBJECT (x ISA_t c) ==> (x \= c) $;
{* =(22)= Abstract superclass rule *}
a22: $ forall x,c/OBJECT (x IN c) ==> (c in CONCRETE) $;
{* =(13)= single instantiation *}
a13: $ forall x,c,d/OBJECT (x IN c) and (x IN d) ==> (c = d) $;
{* =(23)= single specialization *}
a23: $ forall x,s,z/OBJECT (x SPEC s) and (x SPEC z) ==> (s = z) $;
{* =(24)= Definition by instantiation or specialisation *}
a24: $ forall x,y/OBJECT (x SPEC y) ==> not exists c/OBJECT (x IN c) $;
{* =(14)= Unique introduction of relationship labels *}
a14: $ forall x,s,y,t/OBJECT m1,m2/OBJECT!link a/ALABEL
Ai(x,link,m1) and To(m1,y) and (m1 label a) and
Ai(s,link,m2) and To(m2,t) and (m2 label a)
==>
exists c,d/OBJECT m/OBJECT!link
Ai(c,linkDR,m) and To(m,d) and (m label a) and
(x ISA_rt c) and (s ISA_rt c) and (y ISA_rt d) and (t ISA_rt d)
$;
{* =(15)= Stratification of relationships; case without generalization *}
a15: $ forall x,s,y,t/OBJECT m1,m2/OBJECT!link j,l/Integer a/ALABEL
Ai(x,link,m1) and To(m1,y) and (m1 label a) and (m1 targetlevel j) and
Ai(s,link,m2) and To(m2,t) and (m2 label a) and (m2 targetlevel l) and
(x ISA_t s)
==>
(j <= l)
$;
{* =(16)= *}
a16: $ forall x,s,y,t/OBJECT m1,m2/OBJECT!link i,k/Integer a/ALABEL
Ai(x,link,m1) and To(m1,y) and (m1 label a) and (m1 sourcelevel i) and
Ai(s,link,m2) and To(m2,t) and (m2 label a) and (m2 sourcelevel k) and
(y ISA_t t)
==>
(i <= k)
$;
{* =(26)= orthogonality of relationships R' *}
a26: $ forall x,y,t/OBJECT a/ALABEL i,j/Integer m1,m2/OBJECT!link
Ai(x,predR,m1) and To(m1,y) and (m1 label a) and (m1 sourcelevel i) and (m1 targetlevel j) and
Ai(x,predR,m2) and To(m2,t) and (m2 label a) and (m2 sourcelevel i) and (m2 targetlevel j)
==>
not (y SPEC_t t)
$;
{* =(27)= *}
a27: $ forall x,y,s/OBJECT a/ALABEL i,j/Integer m1,m2/OBJECT!link
Ai(x,predD,m1) and To(m1,y) and (m1 label a) and (m1 sourcelevel i) and (m1 targetlevel j) and
Ai(s,predD,m2) and To(m2,y) and (m2 label a) and (m2 sourcelevel i) and (m2 targetlevel j)
==>
not (x SPEC_t s)
$
end
DDI_SpecializationAndInstantiation in Class with
constraint
{* =(28)= Reduction of potencies, source side *}
a28: $ forall x,y,c,d/OBJECT a/ALABEL i,j,k,l,n/Integer mx,mc/OBJECT!link
Ai(x,link,mx) and To(mx,y) and (mx label a) and (mx sourcelevel i) and (mx targetlevel j) and
Ai(c,link,mc) and To(mc,d) and (mc label a) and (mc sourcelevel k) and (mc targetlevel l) and
(n = NMEMBER(x,c)) ==> (n = k - i) $;
{* =(29)= Reduction of potencies, target side *}
a29: $ forall x,y,c,d/OBJECT a/ALABEL i,j,k,l,n/Integer mx,mc/OBJECT!link
Ai(x,link,mx) and To(mx,y) and (mx label a) and (mx sourcelevel i) and (mx targetlevel j) and
Ai(c,link,mc) and To(mc,d) and (mc label a) and (mc sourcelevel k) and (mc targetlevel l) and
(n = NMEMBER(y,d)) ==> (n = l - j) $;
{* =(30)= instantiation and specialization of attributes; target side *}
a30: $ forall x,y,c,d1/OBJECT a/ALABEL i,j,k,l/Integer mx,m1/OBJECT!link
Ai(x,link,mx) and To(mx,y) and (mx label a) and (mx sourcelevel i) and (mx targetlevel j) and
Ai(c,predR,m1) and To(m1,d1) and (m1 label a) and (m1 sourcelevel k) and (m1 targetlevel l) and
(j <= l) and (x ISA_rt c) ==>
exists d2/OBJECT m2/OBJECT!link
Ai(c,predR,m2) and To(m2,d2) and (m2 label a) and (m2 sourcelevel k) and (m2 targetlevel l) and
(y ISA_rt d2)
$;
{* =(31)= instantiation and specialization of attributes; source side *}
a31: $ forall x,y,c1,d/OBJECT a/ALABEL i,j,k,l/Integer mx,m1/OBJECT!link
Ai(x,link,mx) and To(mx,y) and (mx label a) and (mx sourcelevel i) and (mx targetlevel j) and
Ai(c1,predD,m1) and To(m1,d) and (m1 label a) and (m1 sourcelevel k) and (m1 targetlevel l) and
(i <= k) and (y ISA_rt d) ==>
exists c2/OBJECT m2/OBJECT!link
Ai(c2,predD,m2) and To(m2,d) and (m2 label a) and (m2 sourcelevel k) and (m2 targetlevel l) and
(x ISA_rt c2)
$;
{* =(25)= Stratification of relationships; case with generalization *}
a25: $ forall x,s,y,t/OBJECT m1,m2/OBJECT!link a/ALABEL
Ai(x,link,m1) and To(m1,y) and (m1 label a) and
Ai(s,link,m2) and To(m2,t) and (m2 label a) and
(x SPEC_t s)
==>
not (t SPEC_t y)
$
end