{
* File: DualDeep_Part1.sml
* Author: Michael Schrefl, Bernd Neumayr, Manfred Jeusfeld, Christoph Schuetz
* Created: 10-Jun-2013/M.Jeusfeld (11-Dec-2013/M.Jeusfeld)
* ------------------------------------------------------
* Meta model and axiomatization for dual deep instantiation with
* generalization
*
* Part 1: Sorts and predicates
*
* requires ConceptBase 7.6 or later
*
* 14-Nov-2013: additional attributes for D and R; generalizing to link
* 25-Nov-2013: SPEC instead SUB
* 27-Nov-2013: link,predD,predR are all derived
*
* The Telos specifications in this file DualDeep_Part1.sml and in
* DualDeep_Part2.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.
*
}
{*
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/
*}
{* some useful definitions *}
RelationSemantics 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) $
end
{* now define the base sort O (here labelled OBJECT *}
OBJECT with
attribute
link: OBJECT; {* =(6)= generic link; corresponds to the predicate A in the paper *}
linkDR: OBJECT; {* =(4)= explicit attribute implying both range and domain constraints *}
linkD: OBJECT; {* =(3)= explicit attribute implying domain constraints *}
linkR: OBJECT; {* =(2)= explicit attribute implying range constraints *}
predD: OBJECT; {* =(8)= derived domain attribute (either from linkDR or linkD) *}
predR: OBJECT; {* =(7)= derived range attribute (either from linkDR or linkR) *}
IN: OBJECT; {* =(5)= *}
SPEC: OBJECT; {* =(17)= (c SPEC d): c is explicit subclass of d *}
ISIN: OBJECT;
MEMBER: OBJECT; {* =(9)= (x MEMBER c): c is the 'class' side *}
ISA: OBJECT; {* =(11)=,=(20)= *}
ORTHO: OBJECT;
SPEC_t: OBJECT; {* for transitive closure of SPEC *}
MEMBER_t: OBJECT;
ISA_t: OBJECT;
IN_t: OBJECT;
SPEC_rt: OBJECT; {* for reflexive&transitive closure of SPEC *}
MEMBER_rt: OBJECT;
ISA_rt: OBJECT;
IN_rt: OBJECT
end
{* OBJECT!link corresponds to A(x,i,a,j,y); below are its specializations D,R,DR *}
OBJECT!linkD isA OBJECT!link end {* =(6)= *}
OBJECT!linkR isA OBJECT!link end {* =(6)= *}
OBJECT!linkDR isA OBJECT!link end {* =(6)= *}
{* realize the derivation of predD,predR via Telos isA; *}
{* so an instance of linkDR is also an instance of predD etc. *}
OBJECT!linkDR isA OBJECT!predR end {* =(7)= DR(x,s,a,t,y) ==> R'(x,s,a,t,y) *}
OBJECT!linkR isA OBJECT!predR end {* =(7)= R(x,s,a,t,y) ==> R'(x,s,a,t,y) *}
OBJECT!linkDR isA OBJECT!predD end {* =(8)= DR(x,s,a,t,y) ==> D'(x,s,a,t,y) *}
OBJECT!linkD isA OBJECT!predD end {* =(8)= D(x,s,a,t,y) ==> D(x,s,a,t,y) *}
{* link,predR,predD have no explicit solution; all are stemming from their respective subclasses *}
{* implements the :<==> of =(6)=,=(7)=,=(8)= *}
AbstractnessConstraints in Class with
constraint
ac1: $ forall x,y/OBJECT (x link y) ==> (x linkD y) or (x linkR y) or (x linkDR y) $;
ac2: $ forall x,y/OBJECT (x predR y) ==> (x linkR y) or (x linkDR y) $;
ac3: $ forall x,y/OBJECT (x predD y) ==> (x linkD y) or (x linkDR y) $
end
{* closures of the extensional predicates *}
ClosureRules in Class with
rule
c1: $ forall x,y/OBJECT (x SPEC y) ==> (x SPEC_t y) $;
c2: $ forall x,y/OBJECT (x MEMBER y) ==> (x MEMBER_t y) $;
c3: $ forall x,y/OBJECT (x ISA y) ==> (x ISA_t y) $;
c4: $ forall x,y/OBJECT (x IN y) ==> (x IN_t y) $;
t1: $ forall x,y,z/OBJECT (x SPEC z) and (z SPEC_t y) ==> (x SPEC_t y) $;
t2: $ forall x,y,z/OBJECT (x MEMBER z) and (z MEMBER_t y) ==> (x MEMBER_t y) $;
t3: $ forall x,y,z/OBJECT (x ISA z) and (z ISA_t y) ==> (x ISA_t y) $;
t4: $ forall x,y,z/OBJECT (x IN z) and (z IN_t y) ==> (x IN_t y) $;
rt1: $ forall x,y/OBJECT (x SPEC_t y) ==> (x SPEC_rt y) $;
rt2: $ forall x,y/OBJECT (x MEMBER_t y) ==> (x MEMBER_rt y) $;
rt3: $ forall x,y/OBJECT (x ISA_t y) ==> (x ISA_rt y) $;
rt4: $ forall x,y/OBJECT (x IN_t y) ==> (x IN_rt y) $;
r1: $ forall x/OBJECT (x SPEC_rt x) $;
r2: $ forall x/OBJECT (x MEMBER_rt x) $;
r3: $ forall x/OBJECT (x ISA_rt x) $;
r4: $ forall x/OBJECT (x IN_rt x) $
end
{* links are attributes that have both a source and a target level *}
{* We use it for modeling the A(x,sl,a,tl,y) predicate as well as *}
{* R(x,sl,a,tl,y) and D(x,sl,a,tl,y) *}
{* =(1)=,=(6)= *}
OBJECT!link with
attribute
sourcelevel: Integer;
targetlevel: Integer;
label: ALABEL
end
{* =(1)= *}
ALABEL end {* just for labels of the attributes/relationships *}
DerivedPredicateDefinitions in Class with
rule
{* =(9)=,=(18)= *}
MEMBER_rule: $ forall x,c,s,d/OBJECT (x SPEC_rt s) and (s IN d) and (d SPEC_rt c) ==> (x MEMBER c) $;
{* =(20)= *}
ISA_rule: $ forall x,y/OBJECT (x SPEC y) or (x IN y) ==> (x ISA y) $;
{* not used *}
ORTHO_rule : $ forall x,y/OBJECT not (x SPEC_rt y) and not (y SPEC_rt x) ==> (x ORTHO y) $
end
{* an object is concrete if it has no explicit subclass/subobject *}
{* =(22)= *}
CONCRETE in QueryClass,MSFOLrule isA OBJECT with
constraint
isConcrete: $ not exists y/OBJECT (y SPEC this) $
end
{* NMEMBER is virtually a distance functions that counts the
explicit instantiation links (IN) on the path from p1_x to p2_c;
SPECs are overread via the MEMBER predicate
*}
{* =(19)= *}
NMEMBER in Function isA Integer with
parameter
p1_x: OBJECT;
p2_c: OBJECT
constraint
nmember_rule:
$ ((this=0) and (p1_x SPEC_rt p2_c)) or
(exists d/OBJECT (d MEMBER p2_c) and (this = NMEMBER(p1_x,d) + 1)
)
$
end
{* to characterize link multiplicities *}
{* not used in the paper *}
Functional end
Injective end
Total end
Surjective end
{* Inheritance of attributes *}
{* As we have no general predicates in ConceptBase, we use queries to realize them: *}
{* A^r*(x,i,a,j,y) <=> (yes in ARstar[x,i,a,j,y]) *}
{* not used in the paper *}
ARstar in GenericQueryClass isA YesClass with
parameter,computed_attribute
a1_x: OBJECT;
a2_i: Integer;
a3_a: ALABEL;
a4_j: Integer;
a5_y: OBJECT
constraint
c1: $
(exists m1/OBJECT!link From(m1,a1_x) and (m1 sourcelevel a2_i) and (m1 label a3_a) and (m1 targetlevel a4_j) and To(m1,a5_y)
) or
(exists s/OBJECT (a1_x SPEC s) and (yes in ARstar[s,a2_i,a3_a,a4_j,a5_y]) and
not exists y1/OBJECT (yes in ARstar[a1_x,a2_i,a3_a,a4_j,y1])
)
$
end
ADstar in GenericQueryClass isA YesClass with
parameter,computed_attribute
a1_x: OBJECT;
a2_i: Integer;
a3_a: ALABEL;
a4_j: Integer;
a5_y: OBJECT
constraint
c1: $
(exists m1/OBJECT!link From(m1,a1_x) and (m1 sourcelevel a2_i) and (m1 label a3_a) and (m1 targetlevel a4_j) and To(m1,a5_y)
) or
(exists t/OBJECT (a5_y SPEC t) and (yes in ADstar[a1_x,a2_i,a3_a,a4_j,t]) and
not exists x1/OBJECT (yes in ARstar[x1,a2_i,a3_a,a4_j,a5_y])
)
$
end
Astar in GenericQueryClass isA YesClass with
parameter,computed_attribute
a1_x: OBJECT;
a2_i: Integer;
a3_a: ALABEL;
a4_j: Integer;
a5_y: OBJECT
constraint
c1: $
(yes in ARstar[a1_x,a2_i,a3_a,a4_j,a5_y]) or
(yes in ADstar[a1_x,a2_i,a3_a,a4_j,a5_y])
$
end