This paper describes the OntoMaven implementation of a resolution algorithm for importation in the ISO Common Logic (Edition 2) language. OntoMaven is a plug-in based extension of the Apache Maven software build tool for the development and reuse of knowledge base (KB) artifacts, such as ontologies and rule bases, managed in distributed (Web) repositories, such as Github and Subversion. The OntoMaven CL2 import plug-in contributes a proof-of-concept implementation of CL2 importation semantics that handles circular imports.
QN (G) := domain(N, G) is a domain restriction with domain name N applied to a text G.
MN := import(N) is an importation of the title N.
We also make use of composition notation and some shortcuts:
L(N, G) := X(ttl(N, G)) is a titling text. ? is a canonical unsatisfiable text, e.g. a text construction whose argument is the empty disjunction; G is unsatisfiable iff G ?.
A B(G) := A(B(G)) QhN1,:::, Nmi := QN1 : : : QNm
QS := QhN1,:::, Nmi, where S = fN1,: : :, Nmg with N j < N j+1.
In the last item, WLOG we make use of some total ordering, e.g. lexicographic, on the countable vocabulary V .
As defined in the CL2 Standard, the entailment relation ( ) holds fundamentally between corpora - sets of texts; however, it is left unspecified how a corpus is to be delineated in practice. In this proof-of-concept implementation, we use the file system as our mechanism for corpus delineation - a corpus is the set of XCL2 documents in a directory.
Instead of named texts, CL2 has titlings, ttl(N, G). The content G is not considered to be asserted unless it is imported, and the semantics of the assertions is affected by any domain restrictions that are applied to that importation, so that in general QS(MN ) QS0 (MN ) for S 6= S0. Expressions that occur within some titling are called inaccessible; otherwise, they are accessible. Unlike OWL and RDF, Common Logic is not closely tied to the physical structure of the Web or its standards and conventions. In particular, in titling ttl(N, G) it is not assumed that N is an IRI. If N is an IRI, it is not assumed that G may be dereferenced from that IRI. Here, we assume that titles are IRIs; however, our methods could be easily extended to the general case.
CL2 importations are allowed to be circular; e.g., the content of a titling may import itself, as in L(N, MN ), and the content of a pair of titlings may import each other, as in X(L(N, MM), L(M, MN )). Because of this, the CL2 semantics employs a fixed point approach to define the semantics of importations (see the Appendix).
A common strategy for handling circular importations in other languages, e.g. in OWL, is to ignore repetitions. However, since CL2 importation within a domain restriction may change the semantics of the imported text, more complex criteria must be satisfied in order to avoid circularity.
Our resolution of CL2 importation iteratively applies a semantics-preserving transformation R to a corpus C to obtain a sequence Cn = Rn(C ), n =0, 1, : : :, terminating when a fixed point (Cm = Cm+1) is reached or inconsistent titlings (different texts assigned to the same title, e.g. X (L(N, G), L(N, G0))) are found (in which case, C ?).
In the CL Standard, as well as its revision CL2, multiple dialects (serializations) are
presented. In our implementation, we handle only the XML-based syntax XCL2, although
this approach could be applied to CLIF2 or other CL2 dialects through translations
based on their shared abstract syntax. The XML-based syntax of XCL2 allows us to take
advantage of the many standards, and implementations thereof, available for manipulating
XML. In particular, canonical XML [
The contribution of this paper is the proof-of-concept implementation of the
OntoMaven [
OntoMaven [
Like Maven, OntoMaven is also based around the central concept of a build lifecycle which is made up of build phases representing certain stages in the development life cycle. It therefore extends an OntoMaven declarative XML-based POM (Project Object Model) to describe a KB project being build, its dependencies on required external KB artifacts and components which are published in distributed repositories, the build order, and the required plug-ins which implement and execute the goals defined for each project build phase. A goal represents a specific task which contributes to the build and management of an OntoMaven KB project. OntoMaven is using Maven’s extensible plug-in architecture for implementing predefined goals which are performing certain well-defined tasks in different build phases, such as import and dependency management of KB artifacts from distributed repositories, versioning with semantic difference computation, automated documentation and testing, and deployment etc. The focus of this section is on the CL2 import plug-in which implements an importation resolution algorithm.
The importation resolution algorithm iteratively transforms a given corpus of CL2 texts into a logically-equivalent corpus by resolving each accessible N importation provided there is a unique accessible N titling.
The import resolution algorithm is initialized with a set of XCL2 documents Docs which constitute the text corpus. The documents are contained in a data structure CL2-Corpus, which reflects the state of the corpus during the transformation process (see Listing 1).
The documents of the corpus may contain XInclude directives, either created by an earlier application of the importation resolution algorithm, inserted manually, or created by some other application. To assist in following these include directives, the corpus data structure also contains an XML Catalog Catalog and an Includes map. The Catalog is a map from the IRIs referenced by the XInclude directives to the local paths of any cached copies of the included texts. When the corpus is loaded, the locally-cached includes are loaded into memory in the Includes map, using their local path as the key, and uncached includes are downloaded from their remote locations, if possible, and added to the Catalog and Includes maps as well. Failure to obtain an included text causes an Exception to be thrown.
CL2-CORPUS(Docs;Catalog; Includes) 1 INIT(Docs) 2 T Empty Map 3 for each document d in Docs 4 do IDENTIFY-AVAILABLE-TITLINGS(d:root; T ) 5 IDENTIFY-AVAILABLE-TITLINGS(e; T ) 6 if e is Titling 7 then if T contains key e.name 8 then if e.content = T .get(e.name) 9 then return 10 else Conflicting Titling Error 11 else T .add(e.name, e.content ) 12 return 13 if e is Include 14 then 15 i Includes.get(Catalog.get(e.href)) 16 IDENTIFY-AVAILABLE-TITLINGS(i; T ) 17 return 18 for each node c in e.children 19 do if c is Restrict or Construct 20 then IDENTIFY-AVAILABLE-TITLINGS(c; T )
1 PROCESS-IMPORTS(T ) 2 while resolvable accessible importations exist 3 do for each document d in Docs 4 do R Empty Stack 5 PROCESS-IMPORT(d:root; R; T ) Listing 2. The Process-Imports function constitutes the entry point to the recursion.
Titlings initially accessible are collected into a set T by traversing the node tree of each document d, starting from the root element d:root, until the first Titling element in the subtree is encountered. Nodes other than the text elements Restrict and Construct also terminate their subtree recursion. Duplicate titlings are ignored, while inconsistent titlings lead to an error message and the premature termination of the importation process.
Listing 2 shows the entry into the recursion. Resolution of available imports is accomplished by traversing the structural elements (root and text elements) of each document in the corpus (XInclude directives encountered in this traversal are followed) and substituting each accessible importation occurrence with the content of a titling for the imported title, if such a titling is accessible anywhere in the corpus (see Listing 3). Substitution in this context means that the titling content is copied into an external document, and a reference to the external files is established by inserting an XML include (XInclude) directive in place of the CL2 importation.
In order to avoid duplicate importations, which could produce non-terminating loops, whenever an importation is resolved with an XInclude directive, its generated URI (described below) is added to Catalog prior to entry into a recursion over the subtree of the imported text. If the generated URI for the current Import element is found in Catalog, e: an element, R: the restriction context stack, T : the titling context stack. includeURI GENERATE-INCLUDE-URI(e.name, R) if Catalog contains includeURI then Duplicate import detected, replace e with empty Construct else i new xml include element i.href includeURI replace e with i newtext clone of T .get(e.name) localURI a local path for caching newtext Catalog.add(includeURI, localURI) Includes.add(localURI, newtext) IDENTIFY-AVAILABLE-TITLINGS(newtext; T )
PROCESS-IMPORT(newtext; R; T ) a duplicate importation has been detected, and an empty text construction is inserted in place of the Import element.
If a Titling element is encountered, there is no need to continue the recursion in the current branch, since all importations encountered in the content would be titled.
Each Import element, after checking for duplicates, is replaced with an include element, while the content of the imported titling is added to an Includes structure, which is in turn part of the CL2-Corpus structure and stores all imported titled texts.
Include elements may refer to texts that contain importations or nested titlings which have become accessible due to their importation. Therefore, the text referenced by the include is retrieved from the Includes structure and the recursion continues in the content of the included text, after newly available titlings are added to T .
The XML Catalogs standard [
When an Include element is encountered directly in subtree recursion, the included text is retrieved from the Includes structure and the recursion continues in the included text.
The history of domain restrictions is traced using a stack R. For each entry into a restricted context (within a Restricts element) the domain of the restriction is pushed onto 1 uri ”http://ontomaven.org?uri=” + URLENCODE(n) 2 Rnormalized R sorted alphabetically, without duplicates 3 for i 1 to R.length 4 do uri uri + ”;dom” + i + ”=” + URLENCODE(Rnormalized[i]) 5 return uri
the stack and deleted upon leaving the restricted context.
The scheme for constructing the system identifiers for the included resources is implemented in the procedure generate-include-uri, which is called from line 4 in the Process-Import procedure (see Listing 4).
As pointed out in the Appendix, the order of nestings of domain restrictions has no effect on the semantics of the resulting text, and it is sufficient to ensure that every arbitrary sequence of domain restrictions under which an importation is processed is recognized as the same domain restriction, as long as the members of the sequence are the same, regardless of their order or duplications. To achieve this, it is sufficient to sort the domains of the nested domain restrictions in alphabetical order and purge duplicates (line 2).
The system identifier for a resource that contains a text resulting from resolution of an importation of titled text with the title http://example.org/myText-A1#a (without domain restrictions) would be http://ontomaven.org?uri=http\%3A\%2F\ %2Fexample.org\%2FmyText-A1\%23a.
The system identifier for the same text imported both under the nested domain restrictions http://example.org/myDomain-N1 and http://example.org/ myDomain-N2, as well as under the nested domain restrictions http://example.org/ myDomain-N2, http://example.org/myDomain-N1 would be http://ontomaven. org?uri=http\%3A\%2F\%2Fexample.org\%2FmyText-N1\%23a;dom1=http\%3A\ %2F\%2Fexample.org\%2FmyDomain-N1;dom2=http\%3A\%2F\%2Fexample.org\ %2FmyDomain-N2.
Determination of equivalent titlings is accomplished on the syntactical level by following these steps: resolution of all CURIES and removal of prefix declarations stripping out of XML comments and processing instructions removal of @key attributes making the symbol edge explicit in non-IRI Names and Data elements. transformation to canonical XML form
The implementation of the CL2 importation algorithm described in this paper has
been incorporated in a plug-in to the Maven build management system and complements
the OntoMaven suite, which provides support for lifecycle management of OWL ontolgies
and related artifacts in the form of importation, semantic versioning [
Such tasks are referred to as goals in Maven terminology, and the CL2 importation task has been implemented in the form of such a Maven goal. The invocation and parametrization of Maven goals, as well as the rest of the build cycle, is controlled in a declarative way, using XML-based POM (Project Object Model) descriptors.
In software engineering circular dependencies between imports of software artifacts
are widely considered as problematic. Several solutions on how to find and avoid
circular dependencies have been proposed, including [
The halting problem of cyclic imports is also closely related to infinite loops in
recursion, as it occurs e.g. in several backward-reasoning resolution algorithms such
as SLDNF. Much work has been done in this field to define restriction properties (on
the dependency graph whose vertices are the predicate symbols from a logic program)
for which SLDNF then is complete, such as e.g. stratification. Other approaches use
alternating fixpoint semantics to capture the negation of positive existential closure (e.g.
for transitive closure), such as the constructive characterization of the well-founded
semantics for normal logic programs in terms of alternating fixpoint partial models [
The general problem of cycle detection also occurs in graphs and several algorithms have been proposed such as Floyd’s cycle-finding algorithm or Brents’s algorithm.
From the perspective of modular ontologies or knowledge bases, it has been
recognised since at least the 90’s [
The Common Logic community has chosen to embrace circular importations and semantics-altering importations into domain restrictions, together with the difficulties in implementation that arise from their interaction. The implementation presented here differs from previous approaches to circular dependencies due to the special requirements imposed on the resolution by importation within domain restriction, as well as the properties provide by the CL2 semantics that permit termination of the importation cycles.
The presented research follows a software engineering-oriented research methodology
grounded in Design Science research. It contributes with a new practical design artifact,
the OntoMaven CL2 plug-in, being a proof-of-concept implementation for the rigorous
ISO Common Logic (Edition 2) importation resolution that handles circular importation.
Future work will include
integration of importation resolution with a mechanism to assemble a corpus from
the IRIs of texts published on the internet (e.g. an XML configuration file, or a
DOL [
The first point is already partly addressed by Maven’s dependency resolution mechanism but is only applicable under the precondition that the external texts are published as Maven artefacts in Maven repositories. Future work will be focused on a generalization of this approach in order to cover cases where the external texts are published as general web resources, as well as generating transformed corpora in preparation for inference.
The correctness of the importation resolution algorithm presented above depends on the corpus Cn at the n-th step of the importation resolution process being logically equivalent to the original corpus C0 for all n. This may be proved from two theorems: Th. 9 shows that substituting the content of an accessible N titling in place of an occurrence of an accessible N importation is a semantics-preserving transformation. Th. 11 shows that each step of the importation resolution algorithm is semantics-preserving. The termination of the importation resolution algorithm, proved in Th. 10, depends on the achievement of a fixed point after a finite number of steps.4
From [
Let T be the set of texts in some CL2 language L with vocabulary V . Following [
Definition 1. Let a structural interpretation I be a structural pre-interpretation that satisfies the following constraints: for any names N, Ni 2 V , S any finite set of names in V , texts G, Gi 2 T , and sentences, statements or texts Ei 2 L , (a) TVI (MN ) = true. (b) TVI (L(N, G)) = true iff ttlI (N) = G. (c) If G is an importation or titling, then TVI (G) = TVI (QS(G)). (d) TVI (X()) = TVI (QS(X())) = true. (e) TVI (QS(X(G))) = TVI (QS(G)). (f) TVI (X(E1, : : :, En)) = ^in=1TVI (X(Ei)), n 1.
4Due to space limitations, we provide proofs for only some of the Theorems stated here. A journal paper with complete proofs is in preparation. (g) TVI (QS(X(E1, : : :, En))) = TVI (X(QS(X(E1)), : : :, QS(X(En)))), n (h) TVI (QS QN1 QN2 (G)) = TVI (QS QN2 QN1 (G)). The relevance of this structural semantics to the CL2 semantics is embodied in the following results.
Theorem 2. For every CL2 interpretation I there is a structural interpretation Struc(I) that has an equivalent satisfaction relation. That is, for any C T , I C iff Struc(I) st C .
Proof. Given I, we may define a structural interpretation J = Struc(I) having the same
title mapping, where for any text G 2 T , TVJ(G) = true iff I(G) = true and ArgC(G) 2
U D [ U D , as defined in [
st
C2, then C1 C2.
st
C2, then C1
C2.
In order to demonstrate that the transformations of the importation resolution algorithm preserve (structural) semantics, we will make use of some auxiliary definitions. We define the following subsets of T .
Tttl := fG 2 T : G = L(N, D) for some N 2 V , D 2 T g.
Tprop0 := fG 2 T : G = X(E)g for some sentence or discourse statement Eg. Tprop := f G 2 T : G = QS(G0) for some G0 2 Tprop0 and some finite S V g. Timp0 := fG 2 T : G = MN for some N 2 V g.
Timp := f G 2 T : G = QS(G0) for some G0 2 Timp0 and some finite S V g. We define the set of elementary texts Telem of L to be the union of Tttl, Tprop and Timp. A formal corpus is a corpus of elementary texts.
Theorem 3. For every text G 2 T , there is a unique finite formal corpus F (G) Telem that may be derived from G by a finite sequence of the following transformations, which preserve structural semantics: replacement of a corpus member that is a text construction with multiple arguments by the set of unary text constructions having one of these arguments; replacement of a corpus member that is a text construction with only text arguments by the set (possibly empty) of arguments; replacement of a corpus member that is a composition of domain restrictions of a text by a permuted composition of the same set of domain restrictions applied to the same text. replacement of a corpus member that is a composition of domain restrictions applied to a text construction by the set (possibly empty) of texts consisting of this composition of domain restrictions applied to a text construction of one of the arguments; replacement of a corpus member that is a composition of domain restrictions applied to a unary text construction of a text by the same composition of domain restrictions applied to the text. replacement of a corpus member that is a composition of domain restriction of a titling text by the titling text.
Proof. Intuitively, G corresponds to a finite abstract structural syntax tree, where each non-leaf subtree is a text, while leaves may be sentences, statements, importations or empty text constructions. Each path from the root to a leaf that is not an empty text construction corresponds to a unique elementary text, which together constitute F (G). Each transformation above preserves structural semantics, due to the structural interpretation constraints. A finite number of such transformations can be performed for a given finite text, terminating in F (G). Thus F (G) st fGg.
Theorem 4. For each C T we define F (C ) := [G2C F (G). Then F (C ) F (F (C )) = F (C ), F (C0 [ C1) = F (C0) [ F (C1), and C st F (C ). Telem, Let the closure core K (C ) of a structurally-satisfiable corpus C ? be the intersection over all structurally-satisfying interpretations of the formal corpora of its importation closures: K (C ) := \ st F (CloI (C )). If C st ?, we define K (C ) := Telem.
I C st Theorem 5. For every corpus C , F (C ) K (C1) K (C0 [ C1): Further, K (C )
K (C ), K (F (C )) = K (C ), and K (C0) [ st C , and hence K (C ) C .
A canonical corpus is a corpus C Telem such that there is no name N such that C contains both an accessible importation of N and an accessible titling of N. For every corpus C T , define Can(C ) to be the canonical corpus obtained by deleting from its closure core K (C ) any accessible N importation if there is an accessible N titling in K (C ). T , C st st ? is finite, then so is Can(C ).
?, then Can(C ) = Tttl [ Tprop.
Theorem 7. For every corpus C
T , Can(C )
C , and hence Can(C )
C . st st Theorem 8. For any pair of corpora C0, C1 T , C0 C1 iff Can(C0) (Can(C0) \ Tttl)). Further, C0 st C1 iff Can(C0) = Can(C1).
Can(C1 [ Theorem 9. Let C0 be a corpus containing an accessible N titling with content G. Let C1 be the corpus resulting from C0 by substituting G in place of an occurrence of an accessible N importation. Then C0 st C1, and hence C0 C1.
Proof. By construction, we have Can(C0) = Can(C1) and so from Th. 8 we have C0 st C1. By Th. 2, it follows that C0 C1.
Let C T be finite, C st ?, and let Cn = Rn(C ), n =0, 1, : : : be the result of the importation resolution procedure (ignoring the termination criterion).
Theorem 10. There exists a non-negative integer m such that Cm = Cm+1. Proof. There are a finite number of titlings, importations and domain restrictions (accessible or not) in the original corpus. Hence there will be a finite number of importations that are resolved by substituting titling content. Once these substitutions have been exhausted, the only further changes in the corpus will be substituting empty text constructions, which reduce the number of importations in the corpus, and so a fixed point is reached after some finite number of steps.
Theorem 11. Cn is structurally, and hence logically, equivalent to C0.
Proof. Consider the sequence Cˆn where Cˆn = Cn [ In, I0 is the empty set and In = In 1 [ fGng where Gn is the elementary text that is an N importation within the same set of domain restrictions as the importation occurrence that is substituted for at step n. Then it may be shown by induction that there is a finite subsequence n j, j =0, . . . , k such that F (Cˆn j ) is the same as some sequence obtained by the procedure defined in Th. 6. Further, for any integer i such that n j i < n j+1 F (Cˆi) = F (Cˆn j ) and for any integer i nk, F (Cˆi) = F (Cˆnk ) = K (C ).
Corollary 6. If Cm = Cm+1, then F (Cm) = Can(C ).