It has been well recognized that the structuring of logicbased databases like formal ontologies is an important prerequisite to allow for an e cient reasoning on such databases. Development graphs have been introduced as a formal basis to represent and reason on structured speci cations. In this paper we present an initial methodology and a formal calculus to transform unstructured speci cations into structured ones. The calculus rules operate on development graphs allowing one to separate speci cations coalesced in one theory into a concisely structured graph.
It has been long recognized that the modularity of speci cations is an
indispensable prerequisite for an e cient reasoning in complex domains. Algebraic
speci cation techniques provide frameworks for structuring complex speci
cations and the authors introduced the notion of an development graph [
In this paper we present further steps towards the support for structure formation in large speci cations that additionally allows to factorize equivalent sub-speci cation, i.e. sub-ontologies. The idea is to provide a calculus and a corresponding methodology to crystallize intrinsic structures hidden in a specication and represent them explicitly in terms of development graphs. We start ? This work was funded by the German Federal Ministry of Education and Research under grants 01 IS 11013B and 01 IW 10002 (projects SIMPLE and SHIP) with a trivial development graph consisting of a single node that contains the entire speci cation. Step by step, the speci cation is split to di erent nodes in the development graph resulting in an increasingly richer graph. On the opposite, common concepts that are scattered in di erent speci cations are identi ed and uni ed in a common theory (i.e. node). 2
We base our framework on the notions of development graphs to specify and reason about structured speci cations. Development graphs D are acyclic, directed graphs hN ; Li, the nodes N denote individual theories and the links L indicate theory inclusions with respect to signature morphisms attached to the links.
This approach is based on the notion of institutions [
However, the abstractness of the signatures in the de nition of institution
(they are just a category) makes it di cult to cope with modularization of
signatures. Hence, we equip institutions with an additional structure such that
signatures behave more set-like. Institutions with pre-signatures [
Given an I-institution with pre-signatures, each node N 2 N of the graph is a tuple (sigN ; axN ; lemN ) such that sigN is a I-pre-signature called the local signature of N , axN a set of I-sentences called the local axioms of N , and lemN a set of I-sentences called the local lemmas of N . L is a set of global de nition links M 3+ N. Such a link imports the mapped theory of M (by the presignature ) as part of the theory of N . Thus we obtain corresponding notions of global (pre-)signatures, axioms and lemmata that are de ned inductively as follows: 1 jCj is the class of objects of a category C.
M 3+ N 2D A node N 2 N is globally reachable from a node M 2 N via a pre-signature = id is the 00 morphism , D ` M ? _ 3+ N for short, i 1. either M = N and 0 +3 K 2 L, and D ` K ? _ identity pre-signature morphism, or 2. M 3+ N , with = 00 0.
The maximal nodes (root nodes) dDe of a graph D are all nodes without outgoing links. DomD(N ) := SigD(N ) [ AxD(N ) [ LemD(N ) is the set of all signature symbols, axioms and lemmata visible in a node N . The local domain of N , domN := sigN [ axN [ lemN is the set of all local signature symbols, axioms and lemmata of N . The imported domain Imports D(N ) of N in D is the set of all signature symbols, axioms and lemmas imported via incoming de nition links. DomD = SN2N DomD(N ) is the set of all signature symbols, axioms and lemmata occurring in D. Analogously we de ne SigD, AxD, LemD, and AssD. DomdDe = SN2dDe DomD(N ) is the set of all signature symbols, axioms and lemmata occurring in the maximal nodes of D.
A node N has a well-formed signature i SigD(N ) is a valid IN -signature. A development graph has a well-formed signature i all its nodes have wellformed signatures. SiglDoc(M ) := hsigM [ sym(axM ) [ sym(lemM )iSigD(M) is the local signature of N . A node N is well-formed i it has a well-formed signature SigD(N ) and AxD(N ); LemD(N ) Sen(SigD(N )). A development graph is wellformed, if all its nodes are well-formed.
Given a node N 2 N with well-formed signature, its associated class ModD(N ) of models (or N -models for short) consists of those SigD(N )-models n for which (i) n satis es the local axioms axN , and (ii) for each K 3+ N 2 S, nj is a K-model. In the following we denote the class of -models that ful ll the -sentences by Mod ( ). A well-formed development graph D := hN ; Li is valid i for all nodes N 2 N ModD(N ) j= lemN .
Given a signature and Ax; Lem Sen( ), a support mapping Supp for Ax and Lem assigns each lemma ' 2 Lem a subset H Ax [ Lem such that (i) Modhsym(H)[sym(')i (H) j= ' (ii) The relation @ (Ax [ Lem) Lem with @ ' , ( 2 Supp(') _ 9 : 2 Supp( ) ^ @ ') is a well-founded strict partial order. If D is a development graph, then a support mapping Supp is a support mapping for D i for all N 2 D Supp is a support mapping for AxD(N ) and LemD(N ). 3
As a rst step towards structure formation we will formalize requirements on development graphs that re ect our intuition of an appropriate structuring for (formal) ontologies in particular (and formal speci cations in general) in the following principles.
The rst principle is semantic appropriateness, saying that the structure of the development graph should be a syntactical re ection of the relations between the various concepts in our ontology. This means that di erent concepts are located in di erent nodes of the graph and the links of the graph re ect the logical relations between these concepts. The second principle is closure saying, for instance, that deduced knowledge should be located close to the concepts guaranteeing the proofs. Also the concept de ned by the theory of an individual node of a development graph should have a meaning of its own and provide some source of deduced knowledge. The third principle is minimality saying that each concept (or part of it) is only represented once in the graph. When splitting a monolithic theory into di erent concepts common foundations for various concepts should be (syntactically) shared between them by being located at a unique node of the graph.
In the following we translate these principles into syntactical criteria on development graphs and also into rules to transform and refactor development graphs. In a rst step we formalize technical requirements to enforce the minimalityprinciple in terms of development graphs. Technically, we demand that each signature symbol, each axiom and each lemma has a unique location in the development graph. When we enrich a development graph with more structure we forbid to have multiple copies of the same de nition in di erent nodes. We therefore require that we can identify for a given signature entry, axiom or lemma a minimal theory in a development graph and that this minimal theory is unique. We de ne: De nition 1 (Providing Nodes). Let hN ; Li be a development graph. An entity e is provided in N 2 N i e 2 DomhN ;Li(N ) and 8 M DomhN ;Li(M ). Furthermore, 1. e is locally provided in N i additionally e 2 domN holds. 2. e is provided by a link l : M 3+ N if not locally provided in N and 9e0 2 DomhN ;Li(M ): (e0) = e. In this case we say that l provides e from e0. e is exclusively provided by l i e is not provided by any other link l0 2 L. Finally, the closure-principle demands that there are no spurious nodes in the graph that do not contribute anything new to a concept. We combine these requirements into the notion of location mappings: 3+ N: e 62 De nition 2 (Location Mappings). Let D = hN ; Li be a development graph. A mapping locD : DomD ! N is a location mapping for D i 1. locD is surjective (closure) 2. 8N 2 N : 8e 2 domN : locD(e) = N 3. 8e 2 DomD: locD(e) is the only node providing e (minimality) Furthermore, for a given locD we de ne locD1 : N ! 2DomD by locD1(N ) := fe 2 DomDjlocD(e) = N g. We will write loc and loc 1 instead of locD and locD1 if D is clear from the context.
Based on the notion of location mappings we formalize our intuition of a structuring. The idea is that the notion of being a structuring constitutes the invariant of the structure formation process and guarantees both, requirements imposed by the minimality-principle as well as basic conditions on a development graph to re ect a given formal speci cation or ontology.
De nition 3 (Structuring). Let D = hN ; Li be a valid development graph, loc : DomD ! N , 2 jSignj, Ax; Lem Sen( ) and Supp be a support mapping for D. Then (D; loc; Supp) is a structuring of ( ; Ax; Lem) i 1. loc is a location mapping for D. 2. let DomdDe = 0 [ Ax0 [ Lem0 then = 0, Ax = Ax0 and Lem Lem0. 3. 8 2 LemD : 8 2 Supp( ): 9 : loc( ) ? _ 3+ loc( ) ^ ( ) = 4
In the following we present the transformation rules on development graphs that transform structurings again into structurings. Using these rules we are able to structure the initially trivial development graph consisting of exactly one node that comprises all given concepts step by step. This initial development graph consisting of exactly one node satis es the condition of a structuring provided that we have an appropriate support mapping at hand.
We de ne four types of structuring-invariant transformations: (i) horizontal splitting and merging of development graph nodes, (ii) vertical splitting and merging of development graph nodes, (iii) factorization and multiplication of development graph nodes, and (iv) removal and insertion of speci c links. Splitting and merging as well as factorization and multiplication are dual operations. For lack of space and because we are mainly interested in rules increasing the structure of a development graph we will omit the formal speci cation of the merging and multiplication rules here.
We illustrate our rules with the help of a running example in mathematics. We start from a at theory specifying a Ring over two operations + and . A structure (R; +; ) is a Ring, if (R; ) is an abelian group, (R; +) a monoid and distributes over +. Furthermore, an abelian group is a monoid for which additionally commutativity holds and inverse exists. The initial development graph consists of a single node (without any links) containing all the symbol de nitions, axioms and theorems of the example.
Vertical Split. The rst refactoring rule aims at the split of speci cations in di erent theories. In terms of the development graph a node is replaced by two nodes one of them importing the other; each of them contains a distinct part from a partitioning of the speci cation of the original node. While all outgoing links start at the top node, we are free to reallocate incoming links to either node. To formalize this rule we need constraints on how to split a speci cation in di erent chunks such that local lemmata are always located in a node which provides also the necessary axioms and lemmata to prove it. 1 k 1 . . . De nition 4. Let S = (D; loc; Supp) be a structuring of ( ; Ax; Lem) and N 2 sNigDN.1A]p:a:r:ti]tiosniginNgk ,PafxoNr N is a set fN1; : : : ; Nkg with k > 1 such that 1. sigN = = axN1 ] : : : ] axNk , lemN = lemN1 ] : : : ] lemNk 2. sigNi [axNi [lemNi 6= ; for i = 1; : : : ; k. A node Ni 2 P is lemma independent i Supp( ) \ (axN [ lemN ) (axNi [ lemNi ) for all 2 lemNi .
De nition 5 (Vertical Split). Let S = (hN ; Li; loc; Supp) be a structuring of ( ; Ax; Lem) and P = fN1; N2g be a partitioning for some N 2 N such that N1 is lemma independent. Then, the vertical split S wrt. N and P is S0 = (D0; loc0; Supp) with D0 = hN 0; L0i where
N 0 :=fN1; N2g ] (N n N ) L0 :=f M
3+ M 0 2 LjM 6= N ^ M 0 6= N g [ f N1 8 N2 loc0(e) = < [ f M 3+ N1 j M
3+ N 2 Lg [ f N2 if loc(e) = N and e 2 DomD0 (N2)
N1 if loc(e) = N and e 62 DomD0 (N2) : loc(e) otherwise id +3 N2g 3+ M j N 3+ M 2 Lg such that SigD0 (Ni); i = 1; 2, are valid signatures and axi; lemi i = 1; 2. Conversely, S is a vertical merge of N1 and N2 in S0.
Sen(SigD0 (Ni)), Horizontal Split. Similar to a vertical split we introduce a horizontal split which divides a node into two independent nodes. In order to ensure a valid new development graph, each of the new nodes imports the same theories as the old node and contributes to the same theories as the old node did.
De nition 6 (Horizontal Split). Let S = (hN ; Li; loc; Supp) be a structuring of ( ; Ax; Lem), P = fN1; : : : ; Nkg be a partitioning for some node N 2 N such that each Ni 2 P is lemma independent and loc 1(N ) = domN . The horizontal split of S wrt. N and P is S0 = (D0; loc0; Supp) with D0 = hN 0; L0i where 1. N 0 := fN1; : : : ; Nkg ] (N n N )
1 jDomN1
Using the transformation rules, the at initial theory of our running example can be refactored (cf. Fig. 3). We apply the vertical split rule twice to extract R and the distributivity law, followed by the horizontal-split rule to separate the two instances of a monoid. Finally, we apply the vertical-split rule to extract the extra axioms from M onoid(R; ). We are left with two copies of a monoid which we like to generalize to a common abstract monoid. This can be achieved by the following rule.
Factorization The factorization rule allows one to merge equivalent concepts into a single generalized concept and then to represent the individual ones as instantiations of the generalized concept. A precondition of this rule is that all individual concepts inherit the same (underlying) theories.
De nition 7 (Factorization). Let S = (hN ; Li; loc; Supp) be a structuring of ( ; Ax; Lem). Let K1; : : : ; Kn; M1; : : : ; Mp 2 N with p > 1 such that sigMj [ axMj 6= ; and 9 i;j : Ki
i;j +3 Mj 2 L for i = 1; : : : ; n; j = 1; : : : ; p.
Distrib(*, +), Comm(*), Inverse(*), Monoid(R, +), Monoid(R, *), R . . .
M1 1 ; 1 K1 . . .
Mp . . .
Kn . . . p ; n
Applying the factorization rule allows us to introduce a generic concept of monoids which is instantiated to obtain both previous copies of a monoid.
The factorization rule only covers a su cient criterion demanding that each theory imported by a de nition link to one concept is also imported via de nition links by all other concepts. The more complex case in which a theory is imported Distrib(*, +) Comm(*), Inverse(*), via a path of links can be handled by allowing one to shortcut a path in a single global link. This results in the following rule. 1. 8l0 : M 3+ N: if l0 provides exclusively (e) from some eDomD(M ) then e 2 DomD0 (N ) and l 6= l0; 2. 8e 2 DomD:8M 2 DGRootsD: if loc(e) ? _ 3+ M then there exists M 0 2 dD0e such that loc(e) ? _ 3. 8 2 LemD: Supp( )
3+ M 0; DomD0 (N ) and 8SiglDoc(N )
DomD0 (N ).
Theorem 1 (Structuring Preservation). Let S := (D; loc; Supp) (D = hN ; Li) be a structuring of ( ; Ax; Lem). Then 1. every horizontal split of S wrt. some N 2 N and partitioning P of N , 2. every horizontal merge of S wrt. nodes fN1; : : : ; Nkg N , 3. every vertical split of S wrt. some N 2 N and partitioning P of N , 4. every factorization of S wrt. nodes M1; : : : Mp 2 N , 5. every multiplication of S wrt. N , 6. every transitive enrichment of S, and 7. every reduction of S is a structuring of ( ; Ax; Lem). 5
The refactoring rules presented above provide the necessary instruments to externalize the structure inherent in a given at theory. Nevertheless we need Char Sig. char; A; B; : : : ; Z Ax. 8x : char: x = A _ Lem. | String Sig. str; strnil; addc Ax. 8c : char; x : str: strnil 6= addc(c; x) 8x : str: x = strnil _ 9c : char; y : str: x = addc(c; y) 8c; c0 : char; x; x0 : str: addc(c; x) = addc(c0; x0) ! c = c0 ^ x = x0, : : :g Lem. | Stringops Sig. strapp; strlen Ax. strlen(strnil) = 0 8c : char; x : str: strlen(addc(c; x)) = succ(x) 8x : str: strapp(strnil; x) = x; : : : Lem. 8x; y; z : str: strapp(strapp(x; y); z) = strapp(x; strapp(y; z)); : : : appropriate heuristics to determine suitable partitions for horizontal or vertical splits, in order to group together strongly related entities and afterwards make explicit analogous groupings of entities by factorization. One heuristic is, for instance, to group together all axioms and lemmas exclusively devoted to a speci c sort. E.g. all axioms about characters, or all axioms about natural numbers. From there we carve out those entities about a di erent sort including an already classi ed sorts, and so on. Examples for these are strings or natural numbers, and in the next iteration lists of strings (cf. Fig. 6). These identi ed subsets can then be further partitioned into those de ning the basic datatype and the (inductive) functions and predicates over these. This separates the de nition of lists of natural numbers from the append functions on these, for instance.
Such heuristics guide the application of the horizontal and vertical split rules. From there we can identify nodes with isomorphic local entries and, using the transitivity and reduction rules together with further applications of the split rules try to enable the application of the factorization rule.
We illustrate the refactoring process with the help of a further example,
where we start with attened theories, and step by step carve out the intrinsic
structure. The example from Fig. 6 is about lists of natural numbers, strings
formed over characters and length functions operating on such lists. All the
signature symbols, axioms, and lemmas occur in a single node in the initial
development graph. For sake of readability we partition the set of these entities
into pairwise disjunct subsets and name them accordingly (cf. [
Fig. 7 illustrates the structure formation process for this example. In the rst step the de nitions of Nat and Char are separated from the rest by applying the vertical split rule twice. In the next steps we form the individual theories of String and Stringops respectively. Notice that Stringops includes strlen counting characters in a string such that Stringops has to import Nat. After applying again a vertical split we obtain the theories of Natlist and Natlistops. Since the local axioms of String and Natlist are renamings of each other we factorize these local axioms to a new theory of generic lists. 1. Initial Graph Char, String, Stringops, Nat, Natlist, Natlistops 2. Vertical Split (2x) String, Stringops, Natlist, Natlistops Char
Nat 5. Superfluous Link 6. Vertical Split
7. Factorization 3. Vertical Split Stringops, Natlist, Natlistops
Nat String
Char Natlistops Natlist Nat
Natlist, Natlistops
Nat Natlistops Natlist
Nat Stringops String Char
Natlist, Natlistops
Nat Stringops [String] Char 4. Vertical Split Stringops String Char
Genlist Stringops String
Char String Char Stringops
Genlistops
Natlistops Genlist
Natlist
Nat Stringops String
Char Natlistops
Nat Genlist
[Natlist] 8. Transitive Link (2x) 9. Factorization This node consists of the renamed Genlist local axioms of String (or Natlist, SAixg.. l8isnt;:neill;eamd;dx : list: nil 6= add(n; x) respectively) plus the necessary sig- 8x : list: x = nil nature de nitions to obtain a well- _ 9n : elem; y : list: x = add(n; y) formed development graph node. 8!n;nn=0: nel0e^mx;x=;xx00:; l:i:st:: add(n; x) = add(n0; x0) This theory is imported via de ni- Lem. | tion links to String and Natlist using corresponding pre-signature morphisms to map it to list of chars and numbers, respectively. Both, String and Natlist have now empty local signatures and axioms. In Fig 7 we indicate those nodes with empty local signature, empty local axioms and empty local lemmata by a light-gray color of the node name. 6
There is related work to (re-)structure ontologies (after attening) following
locality criteria into modules containing all knowledge about speci c concepts.
However, since ontology languages have simple imports without renamings,
duplicated sub-ontologies that are for instance equal up to renaming remain hidden.
To excavate these ontologies requires other heuristics than pure logic based ones
to guide the structuring process, and therefore we deliberately did not impose
speci c criteria how to apply the rules beyond the minimal conditions that the
dependency relations among concepts, relations and facts and derived facts and
relations is preserved. It is easy to see that the modularizations of ontologies not
including derived lemmas obtained by using the locality criteria from [
Based on the de nition of structurings as concise development graphs, we presented transformation rules that allow one to make explicit common structures hidden in a at theory in terms of development graphs. It provides a framework to modularize attened ontologies in a useful way as illustrated by two simple examples. An implementation is planned to provide an interactive tool to modularize and factorize large ontologies as well as (semi-)automatic procedures.