OMG_API4KP_Standard.tex

\newcommand{\version}{1.0}

%% Global switches
% Do we pretend that this is a final version?
\newif\ifpretendfinal
%\pretendfinaltrue 
\pretendfinalfalse

% Real PDF comments, or 
% "paper" margin notes (using todonotes or ednotes package)?
\newif\ifpdfcomment
\pdfcommenttrue
%\pdfcommentfalse
\newcommand{\mycomment}{}

\documentclass[10pt,fleqn,%
\ifpretendfinal
final%
\else
draft%
\fi,
%final,
]{scrreprt}

\usepackage{pdflscape} % Make landscape pages display as landscape

% Editorial Notes for LaTeX documents
\ifpretendfinal
  \usepackage[hide]{ed}
\else  
  \usepackage[show]{ed}
\fi 

% Use real todonotes package or work-around with ednotes
\newif\iftodo
%\todotrue [TA] This is not correctly. It is necessary to renewcommand{\todonote}, so for now this options does the same thing as \todofalse
\todofalse


\usepackage{uml}

%color highlight, for editing
\usepackage{color}
\ifpretendfinal
  \newcommand{\red}[1]{#1} 
\else  
  \newcommand{\red}[1]{{\color{red}{#1}}}
\fi

% language definitions
\usepackage{ctable}
\usepackage[final]{listings}
\lstset{basicstyle=\ttfamily\small,columns=fixed}
\usepackage{lstsemantic}
\usepackage{algorithmic}% http://ctan.org/pkg/algorithms


%% Hacks
%\usepackage{savesym}

%% Font and language
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[english]{babel}
\usepackage{textcomp}
\usepackage{courier}
\usepackage[scaled=.9]{helvet}

% set up Unicode symbols
\usepackage{declare-unicode}


% Keyword Index 
\usepackage{makeidx}
\makeindex
% used in definition of \termref, \termdefinition  


%%
\usepackage{omg} % OMG-specific macros
\usepackage{this} % macros specific to this submission

%% Math Macros
\usepackage{math}
\usepackage{hetonto-subset}

%% Utilities
\usepackage{etoolbox}
\usepackage{ifmtarg}
\usepackage{stringstrings}
\usepackage{stmaryrd}
\usepackage{enumitem}

%% Graphics
\usepackage{standalone}
\usepackage{tikz}
\usepackage{rotating}
\usetikzlibrary{matrix,shapes,arrows,calc}
\usepackage{tikz-uml}
%\input{illustrations/DOL-tikz-preamble}


%% linguistics
\usepackage{english}
% Quotes
\usepackage[babel]{csquotes} 
\MakeAutoQuote{“}{”}
\MakeAutoQuote*{‘}{’}
% FN: can we remove that? the quotation marks lead to errors in my editor, so I removed them in the source code anyway. 

%% Hyperref
\usepackage[
          % we want hyperlinks even in draft mode
          final,
          plainpages=false,
          pdfpagelabels,
          bookmarksnumbered,
          hyperindex=true
         ]{hyperref}

%% To-do notes and/or comments
% \savesymbol{todo}
% \restoresymbol{ed}{todo}

\usepackage{xkeyval}
\makeatletter
% author
\newcommand*\CommentAuthor{}
\define@key{Comment}{author}{%
\renewcommand*\CommentAuthor{#1}}
% date
\newcommand*\CommentDate{}
\define@key{Comment}{date}{%
\renewcommand*\CommentDate{#1}}
% id
\newcommand*\CommentId{}
\define@key{Comment}{id}{%
\renewcommand*\CommentId{#1}}
% replyto
\newcommand*\CommentReplyTo{}
\define@key{Comment}{replyto}{%
\renewcommand*\CommentReplyTo{#1}}
% type (currently represented as color and text prefix)
\newcommand*\CommentType{}
\define@key{Comment}{type}{%
\renewcommand*\CommentType{#1}}
\makeatother
\presetkeys{Comment}{%
author=,date=,id=,replyto=,type=}{}%

\newcommand*{\SetCommentColorByType}[1]{%
% http://tex.stackexchange.com/questions/24922/comparing-an-argument-to-a-string-when-argument-is-a-result-of-a-command-with-et
\edef\localType{{#1}}% enforce expansion of #1
\expandafter\ifstrequal\localType{q-aut}{\colorlet{CommentColor}{red}}{%
\expandafter\ifstrequal\localType{q-all}{\colorlet{CommentColor}{orange}}{%
\expandafter\ifstrequal\localType{todo}{\colorlet{CommentColor}{orange}}{%
\expandafter\ifstrequal\localType{fyi}{\colorlet{CommentColor}{lightgray}}{%
\colorlet{CommentColor}{yellow}}}}}}
\makeatletter
\newcommand*{\SetCommentPrefixByType}[1]{%
\edef\localType{{#1}}% enforce expansion of #1
\expandafter\@ifmtarg\localType{% if empty
\edef\CommentPrefix{}%
}{% if not empty
\caseupper[q]{#1}%
\edef\CommentPrefix{\thestring: }%
}}
\makeatother

\newcommand*{\initComment}[1]{%
\setkeys{Comment}{#1}%
\SetCommentColorByType{\CommentType}%
\relax%
\SetCommentPrefixByType{\CommentType}%
\relax%
}

\makeatletter
\ifpdfcomment
% forward class options "draft" or "final" into document
\ifpretendfinal
\usepackage[final]{pdfcomment}
\else
\usepackage[draft]{pdfcomment}
\fi

\newcommand*{\todonote}[2][]{%
\initComment{#1}%
\pdfcomment[author=\CommentAuthor,color=CommentColor,date=\CommentDate,id=\CommentId]{%
\CommentPrefix
%\usebox{CommentPrefix}
#2}}


\newcommand*{\reply}[2][]{%
\initComment{#1}%
\pdfreply[author=\CommentAuthor,color=CommentColor,date=\CommentDate,id=\CommentId,replyto=\CommentReplyTo]{%
%\usebox{CommentPrefix}
#2}}

\newcommand*{\markupcomment}[3][]{%
\initComment{#1}%
\pdfmarkupcomment[author=\CommentAuthor,color=CommentColor,date=\CommentDate,id=\CommentId]{#2}{%
%\usebox{CommentPrefix}
#3}}

% Hyperlinks don't work inside pdfcomment's PDF comments :-(
\newcommand*{\todonoteURL}[1]{#1}
\else % \ifpdfcomment
  \iftodo
     \usepackage[textsize=tiny]{todonotes} % must load after tikz
   \else % \iftodo

      \newcommand*{\todonote}[2][]{
        \initComment{#1}%
        % TODO set color according to type
        % TODO display author (unless empty)
        % TODO display date (unless empty)
        \ednote{TODO: #2}
        }

       \newcommand*{\reply}[2][]{
         \initComment{#1}%
         % TODO set color according to type
         % TODO display author (unless empty)
         % TODO display date (unless empty)
         \ednote{Reply: \CommentPrefix #2}}

       \newcommand*{\markupcomment}[3][]{
         \initComment{#1}%
         % TODO set color according to type
         % TODO display author (unless empty)
         % TODO display date (unless empty)
         \ednote{\CommentPrefix #3}#2}
 \fi % \iftodo
 % dummy versions of some pdfcomment commands
 \renewcommand*{\textLF}{\\}

  \newcommand*{\todonoteURL}[1]{\url{#1}}
\fi % \ifpdfcomment
\makeatother
\newcommand*{\ticket}[1]{\todonoteURL{http://trac.informatik.uni-bremen.de:8080/OntoIOp/ticket/#1}}

% comment commands for frequent users
\newcommand*{\CLnote}[2][author=Tara Athan]{%
\todonote[author=Tara Athan,#1]{#2} 
}




%% ISO structures not defined by isov2.cls, and additional semantic macros
% cross-reference to a normative reference
\newcommand*{\nitem}[1]{[#1]}
% reference from the definition of one term to another defined term
\newcommand*{\termref}[1]{\index{#1}#1\enspace}
% subject field restriction of a term
\newcommand*{\subjectfield}[1]{ {\textlangle}#1{\textrangle}}
% synonym of a term
\newcommand*{\synonym}{; }
% MIME type
\newcommand*{\mimetype}[1]{\textit{#1}}
% Font style for syntactic features only supported with institutions
\newcommand*{\institutionsOnly}{\bfseries\itshape}
% Font style for syntactic features
\newcommand*{\syntax}[1]{\texttt{#1}}


% requirements (as per Annex H of ISO/IEC Directives, Part 2)
\newcommand*{\notallowed}{\textbf{not allowed}\enspace}
\newcommand*{\notrequired}{\textbf{not required}\enspace}
\newcommand*{\required}{\textbf{required}\enspace}
\newcommand*{\recommended}{\textbf{recommended}\enspace}
\newcommand*{\shallnot}{\textbf{shall not}\enspace}
\newcommand*{\shall}{\textbf{shall}\enspace}
\newcommand*{\shouldnot}{\textbf{should not}\enspace}
\newcommand*{\should}{\textbf{should}\enspace}
\newcommand*{\may}{\textbf{may}\enspace}
\newcommand*{\hasto}{\textbf{has to}\enspace}

\newenvironment{Grammar}
 {%\texonly{\footnotesize}
  \begin{example}}{\end{example}\ignorespaces}

\newenvironment{AbstractGrammar}
 {\par%\texonly{\smallskip\samepage}
   \begin{Grammar}}{\end{Grammar}\par}

\newenvironment{ConcreteDisplay}
 {\nopagebreak\begin{quote}\casl}{\end{quote}\pagebreak[3]}

\newenvironment{ConcreteInput}
 {\begin{example}}{\end{example}\ignorespaces}

\newcommand{\DisplayLatexInput}[3]
 {The sign displayed as 
 \texorhtml{`\begin{casl}\(#1\)\end{casl}'}{#2 in \LaTeX}
 is input as `\Gram{#3}'.} 

\newcommand{\DisplayISOInput}[3]
 {The sign displayed as `\begin{casl}\(#1\)\end{casl}' may be input as
 `\math{#2}' in ISO Latin-1, or as `\Gram{#3}' in ASCII.} 

% FN: Latex Hacks by Fabian 

% Sourcecode from isov2.cls
\newcommand{\outofscopename}{The following are outside the scope of this }
\newcommand{\pagename}{Page}
%\newcommand{\tablename}{Table}
\newcommand{\tbpname}{To be published.}
\newcommand{\annexrefname}{annex}
\newcommand{\clauserefname}{clause}
\newcommand{\examplerefname}{example}
\newcommand{\figurerefname}{Figure}
\newcommand{\noterefname}{note}
\newcommand{\tablerefname}{Table}
\newcommand{\pagerefname}{page}
%\newcommand{\abstractname}{}
%\newcommand{\appendixname}{}
%\newcommand{\chaptername}{}
%\newcommand{\partname}{}
\newcommand{\refname}{}
\newcommand{\isourl}[1]{\texttt{<}\url{#1}\texttt{>}}
\newcommand{\aref}[1]{\annexrefname~\ref{#1}}
\newcommand{\bref}[1]{[\ref{#1}]}
\newcommand{\cref}[1]{\clauserefname~\ref{#1}}
\newcommand{\eref}[1]{\examplerefname~\ref{#1}}
\newcommand{\fref}[1]{\figurerefname~\ref{#1}}
\newcommand{\nref}[1]{\noterefname~\ref{#1}}
\newcommand{\tref}[1]{\tablerefname~\ref{#1}}
\newcommand{\pref}[1]{\pagerefname~\pageref{#1}}


\newcommand{\rtm}[0]{\small{\textregistered\enspace}}
\newcommand{\OMGparagraph}[1]{
\vspace{3pt}
{\centerline {#1}}
\vspace{3pt}
}

%%%% Code which is used to produce minipages with border
\usepackage{xparse}
\newlength{\currentindent}
\newsavebox{\fminipagebox}
\setlength{\currentindent}{\parindent}
\NewDocumentEnvironment{fminipage}{m O{\fboxsep}}
 {
  \par\kern#2\noindent\begin{lrbox}{\fminipagebox}
  \begin{minipage}{#1}\ignorespaces  \setlength{\parindent}{\currentindent}}
 {\end{minipage}\end{lrbox}%
  \makebox[#1]{%
    \kern\dimexpr-\fboxsep-\fboxrule\relax
    \fbox{\usebox{\fminipagebox}}%
    \kern\dimexpr-\fboxsep-\fboxrule\relax
  }\par\kern#2
 }

%%%% 


\newenvironment{symbols}[0]{\begin{longtable}{p{.15\textwidth}p{.84\textwidth}}}{\end{longtable}}
\newcommand{\symboldef}[2]{ #1 & #2 \\}

%\renewcommand{\termref}[1]{#1} 
\usepackage{textcomp}

\usepackage{longtable}

\newcommand{\sectionWN}[1]{ \section*{#1}   \addcontentsline{toc}{section}{#1}  } 

% Temporary Hacks (to be removed later or cleaned up) 
\newcommand{\clause}[1]{\chapter{#1}}
\newcommand{\sclause}[1]{\section{#1}}
\newcommand{\ssclause}[1]{\subsection{#1}}
\newcommand{\sssclause}[1]{\subsubsection{#1}}
\newcommand{\termdefinition}[2]{\index{#1}\paragraph{#1} #2}
\newcommand{\termdefinitionLight}[2]{\paragraph{#1} #2}
\newcommand{\nisref}[1]{#1}


\renewcommand{\subjectfield}[1]{} % {#1}
%\renewcommand{\bref}[1]{#1}

\newcommand{\normannex}[1]{ \chapter{Annex (normative): #1} }
\newcommand{\infannex}[1]{ \chapter{Annex (informative): #1} }
\newenvironment{definitions}[0]{\medskip }{}
\newenvironment{note}[0]{\ \\ \textsc{Note} \quad}{}
\newenvironment{example}[0]{\ \newline \textsc{Example}\quad }{}
%\newenvironment{symbols}[0]{\medskip
%	 \begin{tabbing} 
%	OWL 2 Full XXXX  \= Text \kill
%}{\end{tabbing}}

%\usepackage{cleveref}
\renewcommand*{\todonote}[2][]{
        \initComment{#1}%
        % TODO set color according to type
        % TODO display author (unless empty)
        % TODO display date (unless empty)
        \ednote{TODO: #2}
        }

%the afterpage is used to introduce a blank page
\usepackage{afterpage}
\newcommand\blankpage{%
    \null
    \thispagestyle{empty}%
    \addtocounter{page}{-1}%
    \newpage}

%\allowdisplaybreaks


\begin{document}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  FRONTMATTER:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\frontmatter

% own memoir pagestyle

\pagestyle{headings}  % switches on printing of running heads

\begin{flushright}
Date: \today
\end{flushright}
\begin{flushleft}
\includegraphics{omglogo.jpeg}


\bigskip\bigskip
\bigskip\bigskip
\bigskip
%\HUGE{a}
{\fontsize{30}{36}\selectfont Application Programming Interface for Knowledge Platforms (API4KP)}

\bigskip
Version \version

\bigskip\bigskip\bigskip\bigskip\bigskip\bigskip\

\vskip\medskipamount % or other desired dimension
\leaders\vrule width \textwidth\vskip2pt % or other desired thickness
\vskip 12pt 
\nointerlineskip

OMG Document Number: ad/2015-mm-dd \\
Normative reference: \\
Machine readable files(s): ad/2015-05-05, ad/2015-05-05, ..., ad/2015-05-12, \\ \qquad \qquad \qquad ad/2015-05-14 \\
Normative: \\
Non-normative: \\
 

\vskip 12pt
\leaders\vrule width \textwidth\vskip2pt % or other desired thickness
\vskip\medskipamount % ditto
\nointerlineskip
\end{flushleft}

\pagenumbering{gobble}% Remove page numbers (and reset to 1)
\thispagestyle{empty}
\clearpage

\pagenumbering{roman} 
		

\noindent Copyright \copyright 2015, Object Management Group, Inc.\\
Copyright \copyright 2015, Thematix Partners LLC \\
\ednote{[Tara Athan 2016-06-09] TODO: Add additional copyrights.}



\OMGparagraph{USE OF SPECIFICATION - TERMS, CONDITIONS \& NOTICES}
The material in this document details an Object Management Group specification
 in accordance with the terms, conditions and notices set forth below. This
  document does not represent a commitment to implement any portion of this
   specification in any company's products. The information contained in this
   document is subject to change without notice.

\OMGparagraph{LICENSES}
The companies listed above have granted to the Object Management Group, Inc.
 (OMG) a nonexclusive, royalty-free, paid up, worldwide license to copy and
 distribute this document and to modify this document and distribute copies of
  the modified version. Each of the copyright holders listed above has agreed
that no person shall be deemed to have infringed the copyright in the
included material of any such copyright holder by reason of having used the
specification set forth herein or having conformed any computer software to the
 specification.
Subject to all of the terms and conditions below, the owners of the copyright  in this
specification hereby grant you a fully-paid up, non-exclusive, nontransferable, perpetual,
worldwide license (without the right to
sublicense), to use this specification to create and distribute software and special 
purpose specifications that are based upon this specification, and to use, copy, and distribute 
this specification as provided under the Copyright Act; provided that: (1) both the copyright
notice identified above and this permission notice appear on any copies of this specification; (2)
the use of the specifications is  for informational purposes and will not be copied or
posted on any network computer or broadcast in any media and will not be 
otherwise resold or transferred for commercial purposes; and (3) no modifications are made to this
specification. This limited permission automatically terminates without notice if you breach any of
these terms or conditions. Upon termination, you will destroy immediately any copies of the
specifications in your possession or control. 

\OMGparagraph{PATENTS}
The attention of adopters is directed to the possibility that compliance with or adoption of OMG specifications may require use of an invention covered by patent rights. OMG shall not be responsible for identifying patents for which a
 license may be required by any OMG specification, or for conducting legal inquiries into the legal validity or scope of those patents that are brought to its attention. OMG specifications are prospective and advisory only.
  Prospective users are responsible for protecting themselves against liability for infringement of patents.

\OMGparagraph{GENERAL USE RESTRICTIONS}
Any unauthorized use of this specification may violate copyright laws, trademark laws, and communications regulations and statutes. This document contains information which is protected by copyright. All Rights Reserved. No
part of this work covered by copyright herein may be reproduced or used in any form or by any means--graphic, electronic, or mechanical, including
 photocopying, recording, taping, or information storage and retrieval systems--without permission of the copyright owner.

\OMGparagraph{DISCLAIMER OF WARRANTY}
WHILE THIS PUBLICATION IS BELIEVED TO BE ACCURATE, IT IS PROVIDED ``AS IS'' AND MAY CONTAIN ERRORS OR MISPRINTS. THE OBJECT MANAGEMENT GROUP AND THE COMPANIES LISTED ABOVE MAKE NO WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, WITH REGARD TO THIS PUBLICATION, INCLUDING BUT NOT LIMITED TO ANY WARRANTY OF TITLE OR OWNERSHIP, IMPLIED WARRANTY OF MERCHANTABILITY OR WARRANTY OF FITNESS FOR A PARTICULAR PURPOSE OR USE. 
IN NO EVENT SHALL THE OBJECT MANAGEMENT GROUP OR ANY OF THE COMPANIES LISTED ABOVE BE LIABLE FOR ERRORS CONTAINED HEREIN OR FOR DIRECT, INDIRECT, INCIDENTAL, SPECIAL, CONSEQUENTIAL, RELI\-ANCE OR COVER DAMAGES, INCLUDING LOSS
 OF PROFITS, REVENUE, DATA OR USE, INCURRED BY ANY USER OR ANY THIRD PARTY IN CONNECTION WITH THE FURNISHING, PERFORMANCE, OR USE OF THIS MATERIAL, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGES. 

The entire risk as to the quality and performance of software developed using this specification is borne by you. This disclaimer of warranty constitutes an
 essential part of the license granted to you to use this specification.

\OMGparagraph{RESTRICTED RIGHTS LEGEND}
Use, duplication or disclosure by the U.S. Government  is subject to the restrictions set forth in subparagraph (c) (1) (ii) of The Rights in Technical Data and Computer Software Clause at DFARS 252.227-7013 or in subparagraph
 (c)(1) and (2) of the Commercial Computer Software - Restricted Rights clauses at 48 C.F.R. 52.227-19 or as specified in 48 C.F.R. 227-7202-2 of the DoD F.A.R. Supplement and its successors, or as specified in 48 C.F.R. 12.212 of
  the Federal Acquisition Regulations and its successors, as applicable. The specification copyright owners are as indicated above and may be contacted through the Object Management Group, 140 Kendrick Street, Needham, MA 02494, U.S.A.

\OMGparagraph{TRADEMARKS}
MDA\rtm, Model Driven Architecture\rtm, UML\rtm, UML Cube logo\rtm, OMG Logo\rtm, COR\-BA\rtm\ and XMI\rtm\ are registered trademarks of the Object Management Group, Inc., and Object Management Group\texttrademark\,, OMG\texttrademark\, , Unified Modeling Language\texttrademark\,, Model Driven Architecture Logo\texttrademark\,, Model Driven Architecture Diagram\texttrademark\,, CORBA logos\texttrademark\,, XMI Logo\texttrademark\,, CWM\texttrademark\,, CWM Logo\texttrademark\,, IIOP\texttrademark\, , IMM\texttrademark\, , MOF\texttrademark\, , OMG Interface Definition Language (IDL)\texttrademark\, , and OMG  SysML\texttrademark\,\   are trademarks of the Object Management Group. All other products or company names mentioned are used for identification purposes only, and may be trademarks of their respective owners.

\OMGparagraph{COMPLIANCE}
The copyright holders listed above acknowledge that the Object Management Group (acting itself or through its designees) is and shall at all times be the sole entity that may authorize developers, suppliers and sellers of computer
 software to use certification marks, trademarks or other special designations to indicate compliance with these materials.
Software developed under the terms of this license may claim compliance or conformance with this specification if and only if the software compliance is of a nature fully matching the applicable compliance points as stated in the
 specification. Software developed only partially matching the applicable compliance points may claim only that the software was based on this specification, but may not claim compliance or conformance with this
  specification. In the event that testing suites are implemented or approved by Object Management Group, Inc., software developed using this specification may claim compliance or conformance with the specification only if the software
   satisfactorily completes the testing suites.

\newpage 
\OMGparagraph{\large{\textbf{OMG's Issue Reporting Procedure}}}
All OMG specifications are subject to continuous review and improvement. As part of this process 
we encourage readers to report any ambiguities, inconsistencies, or inaccuracies
they may find by completing the Issue Reporting Form listed on the main web page
\url{http://www.omg.org}, under Documents, Report a Bug/Issue (\url{http://www.omg.org/technology/agreement.htm}).

\renewcommand{\contentsname}{Table of Contents}

\tableofcontents

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%   MAINMATTER --
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\mainmatter
%\addtocmark{Introduction} % additional mark in the TOC
%:MM



\chapter*{Preface}
\addcontentsline{toc}{chapter}{Preface}

\sectionWN{OMG}

Founded in 1989, the Object Management Group, Inc. (OMG) is an open membership, not-for-profit computer industry standards consortium that produces and maintains computer industry specifications for interoperable, portable, and
 reusable enterprise applications in distributed, heterogeneous environments. Membership includes Information Technology vendors, end users, government agencies, and academia. 

OMG member companies write, adopt, and maintain its specifications following a mature, open process. OMG's specifications implement the Model Driven Architecture\textregistered\, (MDA\textregistered\,), maximizing ROI through a full-lifecycle approach to enterprise integration that covers multiple operating systems, programming languages, middleware and networking infrastructures, and software development environments. OMG's specifications include: UML\textregistered\, (Unified Modeling Language\texttrademark\,); CORBA\textregistered\, (Common Object Request Broker Architecture); CWM\texttrademark\, (Common Warehouse Metamodel); and industry-specific standards for dozens of vertical markets.

More information on the OMG is available at http://www.omg.org/.


\sectionWN{OMG Specifications}	

As noted, OMG specifications address middleware, modeling and vertical domain frameworks. All OMG Specifications are available from the OMG website at:

\url{http://www.omg.org/spec}

\noindent Specifications are organized by the following categories:
\begin{itemize}
	\item  Business Modeling Specifications
	\item Middleware Specifications
	\begin{itemize}
		\item CORBA/IIOP
		\item Data Distribution Services
		\item Specialized CORBA
	\end{itemize}				
	\item IDL/Language Mapping Specifications
	\item Modeling and Metadata Specifications
	\begin{itemize}	
		\item UML, MOF, CWM, XMI
		\item UML Profile										
	\end{itemize}			
	\item Modernization Specifications
	\item Platform Independent Model (PIM), Platform Specific Model (PSM), Interface Specifications
	\begin{itemize}	
		\item CORBAServices
		\item CORBAFacilities
	\end{itemize}			
	\item OMG Domain Specifications
	\item CORBA Embedded Intelligence Specifications
	\item CORBA Security Specifications
\end{itemize}	

\bigskip 
\noindent
All of OMG's formal specifications may be downloaded without charge from our website. (Products implementing OMG specifications are available from
 individual suppliers.) Copies of specifications, available in PostScript and
 PDF format, may be obtained from the Specifications Catalog cited above or by contacting the Object Management Group, Inc. at:

\bigskip
\noindent 
OMG Headquarters \\
140 Kendrick Street \\
Building A, Suite 300 \\
Needham, MA 02494 \\
USA\\
Tel: +1-781-444-0404\\
Fax: +1-781-444-0320\\
Email: \url{pubs@omg.org}\\

\noindent Certain OMG specifications are also available as ISO standards. Please consult \url{http://www.iso.org}  


\sectionWN{Typographical Conventions}
The type styles shown below are used in this document to distinguish
 programming statements from ordinary English. However, these conventions are
 not used in tables or section headings where no distinction is necessary.

\medskip \noindent
Times/Times New Roman - 10 pt.:  Standard body text

\medskip \noindent
{\fontencoding{T1}\fontfamily{phv}\fontseries{b}\fontshape{n}\selectfont
Helvetica/Arial - 10 pt. Bold: } OMG Interface Definition Language (OMG IDL)
and syntax elements.


\medskip \noindent
\texttt{\textbf {Courier - 10 pt. Bold:}}  Programming language elements.

\medskip \noindent
{\fontencoding{T1}\fontfamily{phv}\fontseries{m}\fontshape{n}\selectfont
Helvetica/Arial - 10 pt.: } Exceptions

\medskip\noindent
NOTE: Italic text represents names defined in the specification or the name of
 a document, specification, or other publication.  
\sectionWN{Issues}	
The reader is encouraged to report any technical or editing issues/problems
 with this specification to \url{http://www.omg.org/report_issue.htm}.


%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%
\setcounter{chapter}{-1}
\chapter{Submission-Specific Material}
\section{Submission Preface}
Athan Services, XYZ\ednote{[Tara Athan 2015-06-09] TODO: Add additional submitters.}, and Thematix Partners LLC are pleased  to submit this joint proposal in response to the Application Programming Interfaces (API) to Knowledge Bases (KB) RFP (OMG document ad/2010-06-09). The submitter contacts for this submission are:
\begin{itemize}
	\item Thematix Partners LLC, Elisa Kendall, ekendall@thematix.com	
\end{itemize}
% http://www.omg.org/cgi-bin/doc?ad/10-06-09.pdf

Clause 0 of this document contains information specific to the OMG submission process and is not part of the proposed specification. The proposed specification starts with Clause 1 “Scope”.





\section{Mandatory Requirements}


\begin{center}
\begin{longtable}{|p{0.09\textwidth}|p{0.42\textwidth}|p{0.42\textwidth}|}
%\caption{Mandatory Requirements}\\
\hline
\textbf{ID} & \textbf{RFP requirement} & \textbf{How this proposal  addresses requirement}\\
\hline
\endfirsthead
\multicolumn{3}{l}%
{\tablename\ \thetable\ -- \textit{Continued from previous page}} \\
\hline
\textbf{ID} & \textbf{RFP requirement} & \textbf{How this proposal addresses requirement}\\
\hline
\endhead
\hline \multicolumn{3}{l}{\textit{Continued on next page}} \\
\endfoot
\hline
\endlastfoot

6.5.1 & Reference information model &
   \\ \hline
%
6.5.1.1 & 
Submitters shall specify a reference information model for the terms used in the 
descriptions of the service functions and the interface parameters. This model 
should be a PIM in the UML or MOF form. This model shall be closely aligned 
with the W3C specification for OWL and RDF.  &
The API4KP ontology, expressed in OWL and converted to UML, satisfies this requirement.
	\\ \hline
%
6.5.2 & Retrieval of raw information from KB -
Proposals shall provide a PIM that defines at least the following capabilities: &
	\\ \hline
6.5.2.1 &
 List the ontologies known in the KB; &
\mycomment{Applied to a KR}
This proposal introduces the concept of a structured Knowledge Resource, as a generalization of the RFPs concept of a KB.
An optional section of the Description of a Structured Knowlege Resource is a listing of the identifiers of the Basic Knowledge Resources which are its "leaf components". 
\mycomment{  TODO this should either restrict to collection-type Structured KRs or adapted to non-collection types}
\mycomment{Applied to a KP}
There are two orthogonal views of a KP: in regard to its Knowledge content and its (software) Components.
Another action that is made available is getting the KRs that are registered in an immutable KP.
Another action is to get the Components of an immutable KP.
\mycomment{ Applied to a KP Manager}
Yet another action is getting the (mutable or immutable) KPs that are managed by a KP Manager.
	\\ \hline
6.5.2.2 &
 List the classes known in a given ontology; &
 % Applied to a Basic KR
This proposal generalizes to the case of Knowledge Resources which are not traditional ontologies. "Class" is a syntactic category of OWL DL. An optional section of the Description of a Basic Knowledge Resource is a listing of vocabulary that is mentioned in it, optionally grouped and/or filtered by the syntactic categories of its language.
 % Applied to a Structured KR
 Another action is getting a description of syntactic decomposition of the leaves of the Structured KR, without flattening or translating into the focus language. The requested syntactic category is language-neutral, e.g. "Names" or "Truth-valued Formulas".
 % Applied to a KP, KP Manager or other Communicating Entity
 An Action on a Communicating Entity of this type is getting its Roles.
 % Applied to a Role
 Get the Proficiencies of a Role.
 % Applied to a Proficiency
 Get the Functionalities exposed by a Proficiency.
  % Applied to an Operation
  Get the Actions that are composed to defined the Operation
 % ToDo these relationships need to be sorted out in regard to abstraction level.
	\\ \hline
6.5.2.3 &
 List the properties known in a given ontology; &
 See 6.5.2.2
	\\ \hline
6.5.2.4 &
 List the datatypes known in a given ontology; &
 See 6.5.2.2
	\\ \hline
6.5.2.5 &
 List the explicit sub-classes of a given class; &
This proposal generalizes to the case of Knowledge Resources which are not traditional ontologies. A "subclass" statement is a syntactic category of formula in OWL DL. In other languages, a request for subclass relationships may require inference.
The principal idea in this requirement, and several others below, is that it should be possible to filter a Knowledge Resource according to a specified syntactic category of formula, according to its language.
This proposal provides a class of Syntactic Filter Operations
which takes as input a KR and a syntactic pattern
and returns a new KR.
% TODO add "syntactic pattern" to the glossary
	\\ \hline
6.5.2.6 &
 List the explicit super-classes of a given class; &
 See 6.5.2.5.
	\\ \hline
6.5.2.7 &
 List the explicit equivalent classes to a given class; &
 See 6.5.2.5.
	\\ \hline
6.5.2.8 &
 List the explicit sub-properties of a given property; &
 See 6.5.2.5.
	\\ \hline
6.5.2.9 &
 List the explicit super-properties of given property; &
 See 6.5.2.5.
	\\ \hline
6.5.2.10 &
 Get the reference URI of a given ontology, class or property; &
 In this proposal, every Knowledge Source has an identifier appropriate to its platform; in the case that the platform is the Semantic Web, that identifier is an IRI.
 A Knowledge Source may have also have annotations.
 An optional section in the Description of a Knowledge Source includes its annotations.
  Similarly, languages may allow annotations to be attached to parts of a Knowledge Source or entities mentioned in a Knowledge Source, as long as they are denoted by an identifier.
 This proposal also provides a class of Discover Operations, which return a listing of the identifiers known to a Knowledge Platform that satisfy a query of its annotations.
 Further, this operation may be considered a lifting operation, where the KnowledgeItem is identified by a URL
 and its Manifestion or Expression has a different IRI.
 %ToDO does this capture the original intent?
	\\ \hline
6.5.2.11 &
 Get the specification of a given class: enumerated, restriction, equivalent specification along with the parameters (constraints...) of this specification;&
 See 6.5.2.5.
	\\ \hline
6.5.2.12 &
 Get the specification of a given property: datatype, object, equivalent, inverse property along with the parameters (constraints, classes at both ends...) of this specification;&
 See 6.5.2.5.
	\\ \hline
6.5.2.13 &
 Get the ‘Top’ (DL terminology) class (equivalent to owl:Thing);&
 %ToDo Ask about the intent of this task
 See 6.5.2.5.
	\\ \hline
6.5.2.14 &
 Test if two classes are “structurally equivalent” (see [SS]).&
 In this proposal, a class of Parse Operations are provided that return the (abstract syntax) Expression of a Knowledge Resource Manifestation. If two Expressions are "equal", then their Manifestations are structurally equivalent.
%ToDo Ask about the intent of this task
 	\\ \hline
6.5.3 & Modification and creation of raw information in KB - Proposals shall provide a PIM that defines at least the following capabilities: &
	\\ \hline
6.5.3.1 &
 Create a class in a given ontology from its reference URI and its specification: enumerated, restriction, equivalent...;&
 An Operation that creates a BasicExpression in the abstract syntax of a particular language, e.g. OWL, RDF, CL, and adds it to an existing BasicExpression in the same language
 is defined in terms of a composition of Actions. The input to the first Action is a KRR language, and the output is an Action that takes a concrete syntactic category in that KRR language. The next output is an Action that takes a tuple containing the parameters required by the constructor of that syntactic category  (or equivalently a curried series of Actions, one for each parameter) and returns the Expression. Additional (curried) Actions takes an IRI and an Expression, and return the Expression annotated with the IRI.
 An Adding Operation is used to add the Expression to an existing KR.
 If the existing KR is Basic, then the new KR will also be Basic.
 If the exiting KR is Structured, then the new KR will also be Structured.
 In the case of an existing Basic KR, the Adding Operation first creates a Collection-Structured KR (e.g. Set or List type, as appropriate) containing the existing KR and the new BasicExpression.
 Then a Merge Operation is used combine these into a single new Basic KR.
 If the existing KR is Structured, then Expression is incorporated into that Structure.
 KPs may partially support this operation for a particular set of languages.
	\\ \hline
6.5.3.2 &
 Delete a class;&
 % Structured Expression 
 Delete a collection of Expressions E1 from a Structured Expression E2. - what this means depends on the Structure (i.e. consider deleting a list - order must be matched, versus deleting a set of expressions from a list structure)
 Delete all Expressions from a Structured Expression E2 that satisfy a specific pattern.
 % Basic Expression
Modify a BasicExpression E2 by applying a delete operation to one of its parameters that is of Collection type.
	\\ \hline
6.5.3.3 &
 Create a property in a given ontology from its reference URI and its
specification: datatype, object, equivalent, inverse...:&
See 6.5.3.1
	\\ \hline
6.5.3.4 &
 Delete a property. &
See 6.5.3.2
	\\ \hline
6.5.4 &
 Querying a KB&
	\\ \hline
6.5.4.1 &
 Proposals shall provide a PIM that specifies the set of standardized expressive powers that a KB may know. For each of these expressive powers, proposals shall clearly specify the semantics.&
 For declarative semantics, expressive power is specified in terms of a preorder on logics.
 % TODO Define expressive power for effective semantics.
 
	\\ \hline
6.5.4.2 &
Proposals shall provide a PIM that specifies the set of standardized reasoning tasks that a KB may perform. For each of these reasoning tasks, proposals shall clearly specify the semantics. &
  %TODO start with OntoIOp, and extend as needed
	\\ \hline
6.5.4.3 &
 Proposals shall provide a PIM that defines the following capabilities: &
	\\ \hline
6.5.4.3.1 &
 Get the expressive power of the KB;&
 What is the minimal sublogic in which a KR can be expressed?
 What is the maximal logic that a KP supports?
	\\ \hline
6.5.4.3.2 &
 Check if a given expressive power is supported by a KB;&
    Compare two logics in regard to expressive power.
    Compare the given expressive power to the set of expressive powers supported by a KP.
	\\ \hline
6.5.4.3.3 &
 Get a list of reasoning tasks supported by the KB;&
    Get all the Functionalities required by the Proficiencies of a KP
    Filter a set of Functionalities by type, e.g. Reasoning Functionalities
	\\ \hline
6.5.4.3.4 &
 Check if a given list of reasoning tasks are supported by a KB;&
   Set containment applied to sets of Functionalities
	\\ \hline
6.5.4.4 &
 Proposals shall provide a PIM that allows at least the following reasoning tasks (on ontologies):&
	\\ \hline
6.5.4.4.1 &
 Check the consistency of a given ontology;&
 The Query Operation allows checking of inconsistency by determining if the KR
 entails a contradiction. An alias ConsistencyCheck Operation is defined.
	\\ \hline
6.5.4.4.2 &
 Check the entailment of a given ontology by another ontology;&
 The Query Operation
	\\ \hline
6.5.4.4.3 &
 Check the equivalency between two given ontologies;&
 Conjunction of two Query operations
	\\ \hline
6.5.4.5 &
Proposals shall provide a PIM that allows at least the following reasoning tasks (on classes): &
	\\ \hline
6.5.4.5.1 &
 Check satisfiability of a given class expression;&
  Query Operation with query parameter
	\\ \hline
6.5.4.5.2 &
Check subsumption of a given class expression by another class
expression; &
   See 6.5.4.4.2
	\\ \hline
6.5.4.5.3 &
 List the classes that subsumes a given class expression; &
   See 6.5.4.5.1
	\\ \hline
6.5.4.5.4 &
 List the classes that are subsumed by a given class expression;&
   See 6.5.4.5.1
	\\ \hline
6.5.4.5.5 &
 Check equivalency of a given class expression in another class expression;&
   See 6.5.4.4.2
	\\ \hline
6.5.4.5.6 &
 List the classes that are equivalent to a given class expression;&
   See 6.5.4.5.1
	\\ \hline
6.5.4.6 &
 Proposals shall provide a PIM that allows at least the following reasoning tasks
(on instances):&
	\\ \hline
6.5.4.6.1 &
Check if a given instance is an instance of a given class expression; &
   See 6.5.4.4.2
	\\ \hline
6.5.4.6.2 &
 List all known instances of a given class expression;&
   See 6.5.4.5.1
	\\ \hline
6.5.4.6.3 &
List all answers to a given Conjunctive Query Answering (see [CQA]); &
   See 6.5.4.5.1
	\\ \hline
	
6.5.5 &
 Instances in a KB -
Proposals shall provide a PIM that defines at least the following capabilities:&
	\\ \hline
6.5.5.1 &
Creation of an instance of a class. &
See 6.5.3.1
\\ \hline
6.5.5.2 &
Deletion of an instance. &
See 6.5.3.2
	\\ \hline
6.5.5.3 &
Modification of the values of the properties of an instance (add, remove, get and set the values of). &
See 6.5.3.2
	\\ \hline
6.5.6 &
Proposals shall provide a PIM that defines at least the following capabilities: &
	\\ \hline
6.5.6.1 &
Load a RDF or an OWL file in the KB (from the web, and/or from a local file store, ...); &
A Structured KR may be of IO[KnowledgeManifestation] type, and calling the run functionality of this type executes an import task, returning a Knowledge Manifestation.
Lifting Operations are provided from KnowledgeManifestation to KnowledgeExpression and further
to Knowledge Asset.
	\\ \hline
6.5.6.2 &
Unload (i.e. remove from the list of known ontologies) an ontology from a KB, if possible; &
An Update Operation is provided for mutable KPs, to change its state, including adding or
removing KRs from its registry.
	\\ \hline
6.5.6.3 &
Export an ontology in a serialized form (rdf/xml...). &
Lowering Operations are provided from Knowledge Asset to Knowledge Expression to Knowledge Manifestation.
A Structured KR may be of IO[Unit] type, and calling the run functionality of this type executes an export task.
	\\ \hline
6.5.7 &
 PSMs &
	\\ \hline
6.5.7.1 &
Proposals shall specify a platform mapping that fully maps the PIM into Java interface such that the service can be accessed from a Java application. &
 https://github.com/ag-csw/Java4CL/tree/java8/api4kb
	\\ \hline
6.5.7.2 &
 Proposals shall specify a platform mapping that fully maps the PIM into WSDL [WSDL] such that the service can be accessed from a WS-I Basic Profile 1.1 compliant client.&
	\\ \hline
6.5.7.3 &
Proposals shall define the RESTful platform [RESTful] to which they map and provide a mapping that defines how to access a service implementing the PIM from a RESTful client.
Note that the “PSM for REST” is not required to be a full map for the PIM. &
	\\ \hline
6.5.7.4 &
 Proposals shall specify one or more PSMs (e.g., OWL notation, XML Schema) for the serialization of knowledge base schemas and knowledge base populations. This PSM should correspond to the reference information model PIM that is required by 6.5.1.The proposal shall use one of the existing interchange formats already defined for OWL and RDF.&
   \\ RDF is all that is necessary for the Description format, although it is backed by a model of higher expressivity.
   \\ I see no need to specify a particular RDF format for this Description, as whatever we pick will go out of fashion eventually.
   \\ We could specify a particular RDF format that all KPs are required to accept?
	\\ \hline


\end{longtable}
\end{center}
\ednote{[Tara Athan 2015-06-09] TODO: Add additional mandatory requirements}

\section{Optional Requirements}

\begin{center}
\begin{longtable}{|p{0.09\textwidth}|p{0.42\textwidth}|p{0.42\textwidth}|}
%\caption{Optional Requirements}\\
\hline
\textbf{ID} & \textbf{RFP requirement} & \textbf{How this proposal  addresses requirement}\\
\hline
\endfirsthead
\multicolumn{3}{l}%
{\tablename\ \thetable\ -- \textit{Continued from previous page}} \\
\hline
\textbf{ID} & \textbf{RFP requirement} & \textbf{How this proposal addresses requirement}\\
\hline
\endhead
\hline \multicolumn{3}{l}{\textit{Continued on next page}} \\
\endfoot
\hline
\endlastfoot
%
6.6.1 & 
If appropriate, submitters may propose modifications to the ODM specification that would generally improve its usefulness in specifying interfaces to knowledge bases. In particular, submitters may propose changes that enable consistency between the ODM metamodel and the concepts and forms used in the proposed service operations, including import/export of ontologies as specified in 6.5.7.4.	&

   \\ \hline
%%
%
\end{longtable}
\end{center}
\ednote{[Tara Athan 2015-06-09] TODO: Add additional optional requirements}


\clearpage

\section{Issues to be Discussed}

\begin{center}
\begin{longtable}{|p{0.09\textwidth}|p{0.42\textwidth}|p{0.42\textwidth}|}
%\caption{Optional Requirements}\\
\hline
\textbf{ID} & \textbf{Discussion item} & \textbf{Resolution}\\
\hline
\endfirsthead
\multicolumn{3}{l}%
{\tablename\ \thetable\ -- \textit{Continued from previous page}} \\
\hline
\textbf{ID} & \textbf{Discussion item} & \textbf{Resolution}\\
\hline
\endhead
\hline \multicolumn{3}{l}{\textit{Continued on next page}} \\
\endfoot
\hline
\endlastfoot
%
6.7.1	& 
Proposals should discuss exception handling (API and service exceptions) as well as explanation support, meaning, explanation of the proof steps taken by a reasoner to arrive at a specific conclusion.	&
   \\ \hline
%
%	
\end{longtable}
\end{center}
\ednote{[Tara Athan 2015-06-09] TODO: Add additional issues}


\clearpage

\section{Evaluation Criteria}

\begin{center}
\begin{longtable}{|p{0.09\textwidth}|p{0.42\textwidth}|p{0.42\textwidth}|}
%\caption{Evaluation Criteria}\\
\hline
\textbf{ID} & \textbf{Criterion} & \textbf{Comment}\\
\hline
\endfirsthead
\multicolumn{3}{l}%
{\tablename\ \thetable\ -- \textit{Continued from previous page}} \\
\hline
\textbf{ID} & \textbf{Criterion} & \textbf{Comment}\\
\hline
\endhead
\hline \multicolumn{3}{l}{\textit{Continued on next page}} \\
\endfoot
\hline
\endlastfoot
%
	& 
Submissions dealing with more reasoning tasks will be favored.	&
   \\ \hline
%

\end{longtable}
\end{center}
\ednote{[Tara Athan 2015-06-09] TODO: Add additional evaluation criteria}


\section{Proof of Concept}
Prototypical open source tools for \THIS/ are already available, see
annex \ref{a:tools}. It is expected that they will reach industrial
strength within two or three years.
\ednote{[Tara Athan 2015-06-09] TODO: This is a placeholder paragraph}


\section{Changes to Adopted OMG Specifications}
This specification proposes no changes to adopted OMG specifications.
\ednote{[Tara Athan 2015-06-09] TODO: This is a placeholder paragraph}

%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%


\chapter{Scope}
\pagenumbering{arabic} 
This \OMGSpec/ specifies a meta-API for Knowledge Platforms (\THIS/)\index{\thisindex ! definition}.  \THIS/ is designed to
serve as a conceptual model for concrete APIs for Knowledge Platforms, including existing and future APIs.
This \OMGSpec/ responds to the
Application Programming Interfaces (API) to Knowledge Bases (KB) RFP (OMG document ad/2010-06-09)
 \cite{RFP}.
 
 \ednote{TODO: use the sections from the RFP Scope section (6.2).}


\section{Background Information}
Logical languages are used in several fields of computing for the development of formal, 
machine-processable texts that carry a formal semantics.
\ednote{[Tara Athan 2015-06-09] TODO: This is a placeholder paragraph}

\section{Features Within Scope}\index{\thisindex ! scope}
% Can't use \begin{inscope}, as that creates an itemize environment
The following are within the scope of this \OMGSpec/:
\ednote{[Tara Athan 2015-06-09] TODO: This is the point after which DOL stuff remains.}
\todonote[author=Tara Athan,date=D:201110182133+02'00', type=todo]{This is the point after which DOL stuff remains.
Testing newcommand* definition...
}
\begin{enumerate}
\item\label{it:scope-heterogeneous} homogeneous OMS as well as heterogeneous OMS (OMS that consist of parts, which are written in different languages);
\item mappings between OMS (mapping OMS symbols to OMS symbols);
\item OMS networks (they involve several OMS and mappings between them);
\item \label{it:scope-translation} translations between different OMS languages conforming with \THIS/ (translating whole OMS to another language);
\item\label{it:scope-annotation} annotation and documentation of OMS, mappings between OMS, symbols,
and sentences;
\item recommendations of vocabularies for annotating and documenting OMS;
\item a syntax for embedding the constructs mentioned under (\ref{it:scope-heterogeneous})–(\ref{it:scope-annotation}) as annotations into existing OMS;
\item a syntax for expressing (\ref{it:scope-heterogeneous})–(\ref{it:scope-translation}) as standoff markup that points into existing OMS;
\item a formal semantics of (\ref{it:scope-heterogeneous})–(\ref{it:scope-translation});
\item structuring constructs for modeling non-monotonic behaviour; 
\item criteria for existing or future OMS languages to conform with \THIS/.
\end{enumerate}

The following are outside the scope of this \OMGSpec/:
\begin{enumerate}
\item the (re)definition of elementary OMS languages, \ie languages that allow the declaration of OMS symbols (non-logical symbols) 
and
stating sentences about them;
\item algorithms for obtaining mappings between OMS;
\item concrete OMS and their conceptualization and application;
%% I believe that this is really obsolete now. –Christoph Lange, 2011-12-13
% \item a formal definition of interoperability and how to measure the degree of interoperability of two systems\todonote[author=Christoph Lange,date=D:201110182133+02'00']{Well, now this might even be in scope.  We'll see...}
\item mappings between services and devices, and definitions of service and device interoperability;
\item non-monotonic logics\footnote{Logics (formalized as institutions) are necessarily monotonic; conformance criteria for non-monotonic logics ares till under development. However, minimization provides non-monotonic reasoning in \THIS/. It is also possible to include non-monotonic logics by construing entailments between formulas as sentences of the institution.}. 

\end{enumerate}

This \OMGSpec/ describes the syntax and the semantics of the Distributed Ontology, Model and
Specification Language (\THIS/) by defining an abstract syntax and an associated model-theoretic
semantics for \THIS/. 


\chapter{Conformance}\label{c:conformance}
\index{conformance|(}
This clause defines conformance criteria for languages and logics that can be used with \THIS/, as well as conformance criteria for
serializations, translations and applications. The conformance of a
number of OMS languages (namely OWL 2, Common Logic, RDF and RDF Schema, UML Class Diagrams, CASL) as well as translations among
these is discussed in informative annexes of this \OMGSpec/.

It is expected that \THIS/ will be used for other languages than the  set of \THIS/-conforming
languages that are discussed in this \OMGSpec/. There is a  \textbf{\termref{registry} for \THIS/-conforming languages and translations} hosted
at \url{http://logichub.org}.  The registry  also includes descriptions of
\THIS/-conforming languages and translations (as well as other information needed by implementors
and users) in both human-readable and machine-processable form.  

There will be Maintenance Authority (MA)\footnote{or, depending on advisability, a Registration
Authority} established to maintain the registry as an informative resource governed by the
standard.  The registry contents itself will not be normative; however, it is 
expected to become the basis for normative activities.


\sclause{Conformance of an OMS Language/a Logic with \THIS/}\label{c:conform:logic}

\begin{fminipage}{\textwidth}
\textbf{Rationale}: for an OMS language to conform with \THIS/,
\begin{itemize}
\item its logical language aspect\index{language aspect ! logical} either needs to satisfy certain criteria about its abstract
syntax and formal semantics itself, or there must be a translation (again satisfying certain
criteria) to a language that already is \THIS/-conforming.
\item its structuring language aspect\index{language aspect ! structuring} (if present) must not conflict with \THIS/'s own structuring
mechanisms
\item its annotation language aspect\index{language aspect ! annotation} must not conflict with \THIS/'s meta-language constructs.
\end{itemize}
We also define different conformance levels with respect to the usage of IRIs as identifiers for all kinds
of entities that the OMS language supports.
\end{fminipage}


%
%\begin{description}
%\item[Entailment conformance] An OMS language is entailment conformant with \THIS/ if
%its logic is presented as a (not necessarily monotonic) entailment system.\todonote[author=Christoph Lange,date=D:201110060000+02'00',type=todo]{if we want belief revision, we need to talk about "lists of sentences" (i.e. something ordered)}\footnote{Text that goes into ``terms and definitions'': an entailment system consists of a set of sentences $\Sen(\Sigma)$ and a relation $\operatorname{\vdash}\subseteq \mathcal{P}(\Sen(\Sigma))\times \Sen(\Sigma)$, indexed by signatures $\Sigma$ and compatible with signature morphisms.}
%
%\item[Semantic conformance] 
%\end{description}

An OMS language is conforming with \THIS/ if it satisfies the following conditions:
\begin{enumerate}
\item its abstract syntax is specified as an SMOF compliant meta model
or as an EBNF grammar;
\item it has at least one serialization in the sense of section~\ref{c:conform:serialization};
%\item complete round-trip mappings from the human-readable serialization
%to the abstract syntax and vice versa;
\item either there exists a translation of it into a conforming
  language\footnote {For example, consider the translation of OBO1.4
    to OWL, giving a formal semantics to OBO1.4.}, or:
\begin{enumerate}
\item the logical language aspect\index{language aspect ! logical} (for expressing basic OMS) is conforming, and in particular has a semantics (see below),
\item  the structuring language aspect\index{language aspect ! structuring} (for expressing structured OMS and relations
between those) is conforming (see below), and
\item the annotation language aspect\index{language aspect ! annotation} (for expressing comments and annotations)
is conforming (see below).
\end{enumerate}
\end{enumerate}


The \emph{logical language aspect}\index{language aspect ! logical} of an OMS language
is %semantically
conforming with \THIS/ if each logic corresponding to a profile (including
the logic corresponding to the whole logical language aspect) is presented as an
institution \cite{GoguenBurstall92}, and there is a mapping from
the abstract syntax of the OMS language to signatures and sentences
of the institution.
% It may additionally be presented as an institution, leading
%to the possibility of interpreting additional \THIS/ language constructs.%
Note that one OMS language can have several sublanguages or profiles 
corresponding to several logics (for example, OWL 2 has profiles EL, RL and QL, apart from the
whole OWL 2 itself).


The \emph{structuring language aspect}\index{language aspect ! structuring} of an OMS language is conforming with \THIS/ if it can be
mapped to \THIS/'s structuring language in a semantics-preserving way. The structuring language aspect
\may be empty.

The \emph{annotation language aspect}\index{language aspect ! annotation} of an OMS language is conforming with \THIS/ if its constructs
have no impact on the semantics. The annotation language aspect \shall be non-empty; it \shall
provide the facility to express comments.

We define the following levels of conformance of the abstract syntax of a 
 OMS language with \THIS/, listed from highest to lowest:

\begin{description}
\item[Full IRI conformance] The abstract syntax specifies that IRIs be used for
 identifying all symbols and entities.
\item[No mandatory use of IRIs] The abstract syntax does not require  IRIs
 to be used to identify entities. Note that this includes the case of
  optionally supporting IRIs without enforcing their use (such as in Common
  Logic).
\end{description}

Any conforming language and logic shall have a machine-processable description
 as detailed in \cref{c:conform:description}.

\ssclause{Conformance of language/logic translations with \THIS/}\label{c:conform:translation}
\begin{fminipage}{\textwidth}
\textbf{Rationale}: a translation between logics must satisfy certain criteria in order to conform with \THIS/.
Also, a translation between OMS languages based on such logics must be consistent with the
translation between these logics.  Translations should break neither structuring language aspects nor comments/annotations\index{language aspect ! (general)}.
\end{fminipage}

A logic translation is conforming with \THIS/ if it is presented either as an institution morphism or
as an institution comorphism.  
%If the
%languages are presented additionally as institutions, the translations
%\may also be presented as an institution morphism or an institution
%comorphism.

A language translation \shall provide a mapping between
the abstract syntaxes (it \may also provide mappings between concrete
syntaxes). 
A language translation  from language $L_1$ (based on institution
$I_1$) to language $L_2$ (based on institution $I_2$) is conforming
with \THIS/ if it is based on a logic translation such the following
diagram commutes (i.e.\ following both possible paths from 
$L_1$ to $I_2$ leads to the same result):
Language
translations \may also translate the structuring language aspect, in
this case, they \shall preserve the semantics of the structuring
language aspect.  Furthermore, language translations \should preserve
comments and annotations.  All comments attached to a sentence (or
symbol) in the source \should be attached to its translation in the
target (if there are more than one sentences (resp.\ symbols)
expressing the translation, to at least one of them).

\sclause{Conformance of a Serialization of an OMS Language With \THIS/}\label{c:conform:serialization}
\begin{fminipage}{\textwidth}
\textbf{Rationale}: The main reason for the following specifications is identifier injection. \THIS/ is capable
of assigning identifiers to entities (symbols, axioms, modules, etc.) inside fragments of OMS
languages that occur in a \THIS/ document, even if that OMS language doesn't support such identifiers
by its own means. 
Such identifiers will be visible to a \THIS/ tool, but not to a tool that only supports the OMS
language.  To achieve this without breaking the formal semantics of that OMS language, we make use
of \termref{annotation} or commenting features that the OMS language supports, in order to place such
identifiers inside annotations/ comments.  Depending on the nature of the concrete given
serialization of the OMS language, be it plain text, some serialization of RDF, XML, or some other 
structured text format, we can be more specific about what the annotation/commenting facilities of
that serialization must look like in order to support this identifier injection.  
Well-behaved XML and RDF schemas support identifier injection in a `nice' way (rather than using
text-level comments). In the worst case we cannot 
inject anything into an OMS language fragment, because the OMS language serialization simply
would not allow us to write suitable comments, but we would have to point into it from the enclosing context
by using \termref{standoff markup}.


Further conformance criteria in this section are introduced to facilitate the convenient reuse of
verbatim fragments of OMS language inside a \THIS/ document.

Independently from these criteria, we distinguish different levels of conformance of a
serialization with respect to its means of conveniently abbreviating long IRI identifiers.
\end{fminipage}

We define seven levels of conformance of a serialization of an OMS language with \THIS/.

\begin{description}
\item[XMI conformance]
An XMI serialization has been automatically derived from the SMOF specification
of the abstract syntax, using MOF 2 XMI Mapping.
%\ednote{Christoph to all: I'm not sure how MOF and XMI works, i.e. how to inject identifiers into comments there. TM: XMI is an XML-based format.}
\item[XML conformance]
The given serialization has to be specified as an XML schema\footnote{Here, we refer to the general \emph{concept} of a schema, not of the W3C XML Schema language as one way of implementing it.  It is not even required that a machine-readable implementation of the schema serialization exists.}, which satisfies
 all of the following conditions:
\begin{itemize}
\item The elements of the schema belong to one or more non-empty XML
namespaces.%\todonote[author=Christoph
%Lange,date=D:201110051438+02'00',type=fyi]{That means that in a heterogeneous
%OMS we can recognize that a sentence is, \eg, stated in OWL, without
%explicitly ``tagging'' it as ``OWL'' (which we would have to do in the case
%of  a serialization that is merely text conforming).}
\item The serialization shall use XML \emph{elements} to represent all structural elements of an OMS.
\item The schema shall not forbid both attributes and child elements from foreign namespaces (here: the
 \THIS/ namespace \url{http://www.omg.org/spec/DOL/1.0/xml}) on any elements.\footnote{This is because either an attribute or a child element is used to inject identifiers into elements of the XML serialization; cf. clause~\ref{sec:existing-serialization}.}
\end{itemize}

\item[RDF conformance]
The given serialization has to be specified as an RDF vocabulary, which
 satisfies all of the following conditions:
\begin{itemize}
\item The elements of the vocabulary belong to one or more RDF namespaces
 identified by absolute URIs.
\item The serialization shall specify ways of giving IRIs or URIs to all structural elements of an OMS.\footnote{The rationale is that RDF in principle allows for identifying any kinds of items, so an RDF-based serialization of an OMS language should not forbid making use of such RDF constructs that do allow for identifying arbitrary items.}
\footnote{The OWL RDF serialization, for example, does not satisfy the RDF conformance level, for the following reason. There is an \texttt{owl:imports} property but no class representing imports. 
 Therefore, it is not possible to represent a concrete import, of an ontology $O_1$ importing an ontology $O_2$, as a resource, which could have an identifier.  RDF reification would allow for giving the statement $O_1$ \texttt{owl:imports} $O_2$ an identifier. 
 However, the RDF triples resulting from this reification, including, e.g., the triple \texttt{:import\_id rdf:predicate owl:imports},  would not match the head of any rule in the mapping from RDF graphs to the OWL structural specification 
 \url{http://www.w3.org/TR/2012/REC-owl2-mapping-to-rdf-20121211/\#Mapping_from_RDF_Graphs_to_the_Structural_Specification}). 
 They would thus remain left over in the RDF graph that is attempted to be parsed into an OWL ontology, and thus violate the requirement that at the end of this parsing process, the RDF graph must be empty.}  
% \todonote[author=Christoph Lange,date=D:201109221422+02'00',type=q-aut]{Update on 2014-10-09: Is it OK to have this footnote here?  Or if not, where should it go?  I believe it answers the following question:\\ And what if it doesn't? \eg OWL doesn't specify IRIs for import declarations, so we can, \eg, not annotate them when using the RDF serialization of OWL. We could only do it via RDF reification, or by using an XML serialization.}
\item There shall be no additional rules (stated in writing in the specification of the serialization, or formalized in its implementation in, e.g., OWL) that forbid properties from foreign vocabulary namespaces to be stated about arbitrary subjects for the purpose of annotation.
\end{itemize}

\item[Text conformance]
The given serialization has to satisfy all of the following conditions:
\begin{itemize}
\item The serialization conforms with the requirements for the \mimetype{text/plain} media type specified in \nisref{IETF/RFC 2046}, section 4.1.3.
\item The serialization shall provide a designated comment construct that can be placed sufficiently flexible as to be uniquely associated with any non-comment construct of the language.  That means, for example, one of the following:
  \begin{itemize}
  \item The serialization provides a construct that indicates the start and end of a comment and may be placed before/after each token that represents a structural element of an OMS.
  \item The serialization provides line-based comments (ranging from an indicated position to the end of a line) but at the same time allows the flexible placement of line breaks before/after each token that represents a structural element of an OMS.
  \end{itemize}
\end{itemize}

\item[Standoff markup conformance]
An OMS language is standoff markup conforming with \THIS/ if one of its serializations conforms with
the requirements for the \mimetype{text/plain} media type specified in \nisref{IETF/RFC 2046},
section 4.1.3.  Note that conformance with \mimetype{text/plain} is a prerequisite for using, for
example, fragment URIs in the style of \nisref{IETF/RFC 5147} for identifying text ranges.
\end{description}

%~\todonote[author=Christoph Lange,date=D:201110060000+02'00',type=fyi]{The latter two seem trivial, but we need them to rule out ad hoc diagrams drawn on a napkin}

Independently from the conformance levels given above, there is the following hierarchy of conformance \wrt CURIEs (compact URIs) as a means of abbreviating IRIs (grammar specified in \cref{c:curies}), listed from highest to lowest:
\begin{description}
\item[Prefixed CURIE conformance] The given serialization allows non-logical symbol identifiers to have the syntactic form of a CURIE, or any subset of the CURIE grammar that allows named prefixes (\syntax{prefix:reference}, where a declaration of \THIS/-conformance of a serialization \may redefine the separator character to a character different from \syntax{:}).  A serialization that conforms \wrt prefixed CURIE  is \notrequired to support CURIEs with no prefix: its declaration of \THIS/-conformance \may forbid the use of prefixed CURIEs.\\
  Informative comments:
  \begin{itemize}
  \item In the case that CURIEs are used, a prefix map with multiple prefixes \may be used to map the non-logical symbol identifiers of a native OMS to IRIs in multiple namespaces (\cf \cref{c:map-ids})
  \item The reason for allowing redefinitions of the prefix/reference separator character is that certain serializations of OMS languages may not allow the colon (\syntax{:}) in identifiers.
  \end{itemize}
\item[Non-prefixed names only] The given serialization only supports CURIEs with no prefix, or any subset of the grammar of the \syntax{REFERENCE} nonterminal in the CURIE grammar.\\
  Informative comment: In this case, a binding for the empty prefix \hasto be declared, as this is the only possibility of mapping the identifiers of the native OMS to IRIs, which are located in one flat namespace.
\end{description}

Any conforming serialization of an OMS language shall have a machine-processable description as detailed in \cref{c:conform:description}.

\sclause{Machine-Processable Description of Conforming Languages, Logics, and Serializations}\label{c:conform:description}

\begin{fminipage}{\textwidth}
\textbf{Rationale}: When a parser processes a \THIS/ OMS found somewhere, which refers to modules in OMS languages, or includes them verbatim, the parser needs to know what language to expect; further \THIS/-supporting software needs to know, e.g., what other \THIS/-conforming languages the module in the given OMS language can be translated to.  Therefore we require that all languages/logics/serializations that conform with \THIS/ describe themselves in a machine-comprehensible way.
\end{fminipage}

For any conforming OMS language, logic, and serialization of an OMS language, it is required that it be assigned an HTTP IRI, by which it can be identified.  It is also required that a machine-processable description of this language/logic/serialization be retrievable by dereferencing this IRI, according to the linked data principles.  At least there has to be an RDF description in terms of the vocabulary specified in \aref{a:lola}, which has to be made available in the RDF/XML serialization when a client requests content of the MIME type \mimetype{application/rdf+xml}.  Descriptions of the language/logic/serialization in further representations, having different content types, may be provided.%\CLnote[type=fyi]{that opens the door for, \eg, OMDoc}


\sclause{Conformance of a Document With \THIS/}\label{c:conform:document}
\begin{fminipage}{\textwidth}
\textbf{Rationale}: for exchanging \THIS/ documents with other users/tools, nothing that has a formal semantics
must be left implicit.  One \THIS/ tool may assume that by default any OMS fragments inside a \THIS/
document are in some fixed OMS language unless specified otherwise, but another \THIS/ tool can't be
assumed to understand such \THIS/ documents.  Defaults are, however, practically convenient, which is
the reason for having the following section about the conformance of an \emph{application}.
\end{fminipage}

A document conforms with \THIS/ if it contains a \THIS/ text that is well-formed according to the
grammar.  That means, in particular, that any information related to logics has to be made explicit
(as foreseen by the \THIS/ abstract syntax specified in \cref{c:abstract-syntax}), such as:
\begin{itemize}
\item the logic of each OMS that is part of the \THIS/ document,
\item the translation that is employed between two logics (unless it is one of the default translations specified in \aref{a:graph})
\end{itemize}
However, details about aspects of an OMS that do not have a formal, logic-based semantics, may be
left implicit.  For example, a conforming document may omit explicit references to matching
algorithms that have been employed in obtaining an alignment.

\sclause{Conformance of an Application With \THIS/}\label{c:conform:application}

In practice, \THIS/-aware \emph{applications} may also deal with documents that are not conforming 
with \THIS/ according to the criteria established in \cref{c:conform:document}.  However, an 
application only \emph{conforms} with \THIS/ if it is capable of producing \THIS/-conforming documents as 
its output when requested.

We expect most \THIS/-aware applications to support a fixed (possibly extensible) set of OMS languages
conforming with \THIS/.  It is, for example, possible that a \THIS/-aware application only supports OWL
and Common Logic.  In that case, the application may process documents that mix OWL and Common 
Logic ontologies \emph{without} explicitly declaring the respective logics, as the respective 
syntaxes of OWL and Common Logic can be distinguished by examining the different keywords.  
However, for \THIS/ conformance, that application has to be capable of exporting documents with 
explicit references to the logics used.

\THIS/-aware applications also should be able to strip \THIS/ annotations
from embedded fragments in other OMS languages. Moreover, they should
be able to expand CURIEs into IRIs when requested.

\index{conformance|)}

\chapter{Normative References}
\begin{enumerate}
% OLD text
% The following referenced documents are indispensable for the application of this document. For dated references, only
% the edition cited applies. For undated references, the latest edition of the referenced document (including any
% amendments) applies.
  \item{W3C/TR REC-owl2-syntax:2009} {OWL 2 Web Ontology Language: Structural Specification and Functional-Style Syntax. W3C Recommendation, 27 October 2009.\\ \url{http://www.w3.org/TR/2009/REC-owl2-syntax-20091027/}}
  \item{ISO/IEC 14977:1996} {Information technology – Syntactic metalanguage – Extended BNF}
  \item{W3C/TR REC-xml:2008} {Extensible Markup Language (XML) 1.0 (Fifth Edition). W3C Recommendation, 26 November 2008. \\
  \url{http://www.w3.org/TR/2008/REC-xml-20081126/}}
  \item{W3C/TR REC-owl2-profiles:2009} {OWL 2 Web Ontology Language: Profiles. W3C Recommendation, 27 October 2009. \\
  \url{http://www.w3.org/TR/2009/REC-owl2-profiles-20091027/}}
  \item{ISO/IEC 24707:2007} {Information technology – Common Logic (CL): a framework for a family of logic-based languages}
  \item{OMG Document ptc/2010-11-14:} {OMG Unified Modeling Language (OMG UML), Superstructure, Version 2.4. \\
  \url{http://www.omg.org/spec/UML/2.4/Superstructure}. Section 7 (Classes)}
  \item{IETF/RFC 3986} {Uniform Resource Identifier (URI): Generic Syntax. January 2005.\\ \url{http://tools.ietf.org/html/rfc3986}}
  \item{IETF/RFC 3987} {Internationalized Resource Identifiers (IRIs). January 2005.\\ \url{http://tools.ietf.org/html/rfc3987}}
  \item{IETF/RFC 5147} {URI Fragment Identifiers for the text/plain Media Type.  April 2008.\\ \url{http://tools.ietf.org/html/rfc5147}}
  \item{W3C/TR REC-xptr-framework:2003} {XPointer Framework.  W3C Recommendation, 25 March 2003. \\ \url{http://www.w3.org/TR/2003/REC-xptr-framework-20030325/}}
  \item{W3C/TR REC-rdf11-concepts:2014} {RDF 1.1 Concepts and Abstract Syntax.  W3C Recommendation, 25 February 2014. \\ \url{http://www.w3.org/TR/2014/REC-rdf11-concepts-20140225/}}
  \item{W3C/TR REC-xml-names:2009} {Namespaces in XML 1.0 (Third Edition). W3C Recommendation, 8 December 2009.\\
   \url{http://www.w3.org/TR/2009/REC-xml-names-20091208/}}
  \item{W3C/TR REC-rdfa-core:2013} {RDFa Core 1.1 -- Second Edition.  Syntax and processing rules for embedding RDF through attributes. W3C Recommendation, 22 August 2013.\\ \url{http://www.w3.org/TR/2013/REC-rdfa-core-20130822/}}
  % This standard has no unique year, as it consist of multiple parts (see http://tools.ietf.org/html/rfc3629#ref-ISO.10646)
  \item{ISO/IEC 10646} {Information technology – Universal Multiple-Octet coded Character Set (UCS)}
  %\item{W3C/TR REC-rdf-sparql-query:2008} {SPARQL Query Language for RDF. W3C Recommendation, 15 January 2008. \url{http://www.w3.org/TR/2008/REC-rdf-sparql-query-20080115/}}
  \item{W3C/TR REC-rdf-schema:2014} {RDF Schema 1.1. W3C Recommendation, 25 February 2014.\\ \url{http://www.w3.org/TR/2014/REC-rdf-schema-20140225/}}
  \item{W3C/TR REC-rdf11-mt:2014} {RDF 1.1 Semantics.  W3C Recommendation, 25 February 2014. \\ \url{http://www.w3.org/TR/2014/REC-rdf11-mt-20140225/}}
  \item{ODM} {Ontology Definition Metamodel, 2 September 2014. \\ \url{http://www.omg.org/spec/ODM/1.1/}}
\item{MOF} { Meta Object Facility} \\ \url{http://http://www.omg.org/mof/}
\item{SMOF} { Support for Semantic Structure, April 2013} \\ \url{http://www.omg.org/spec/SMOF/1.0/}
\item{XML} {Metadata Interchange (XMI) – using MOF 2 XMI, April 2014} \\ \url{http://www.omg.org/spec/XMI//}
%\item{PRR} {Production Rule Representation, December 2009} \\ \url{ http://www.omg.org/spec/PRR/1.0// }
\item{SBVR} {Semantics Of Business Vocabulary And Rules, November 2013} \\ \url{http://www.omg.org/spec/SBVR/}
\item{DTV} {Date-Time Vocabulary, August 2013} \\ \url{http://www.omg.org/spec/DTV/1.0/}
\item{RIF} {Rule Interchange Format, February 2013} \\ \url{http://www.w3.org/TR/rif-overview/}
\item{SKOS} { Simple Knowledge Organization System} \\ \url{ http://www.w3.org/2004/02/skos/}

\end{enumerate}




\chapter{Terms and Definitions}\label{terms-and-defs}
%\ednote{OMG specifications shall not contain glossaries, hence always
%refer to this section if definitions of terms are needed.}

For the purposes of this document, the following terms and definitions apply.

\sclause{Distributed Ontology, Model and Specification Language}

\begin{definitions}
  \termdefinitionLight{Distributed Ontology, Model and Specification Language\synonym
  \THIS/}\index{\thisindex ! definition}{language for formalizing {libraries}\index{library} of \termref{OMS} and OMS networks\index{OMS network}, 
  whose syntax and semantics are specified in this \OMGSpec/{}.}
%
% \begin{note}
%  When viewed as an \termref{OMS language}, \THIS/ has \termref{OMS} as its
% non-logical symbols\index{non-logical symbol}, and OMS mappings\index{OMS mapping} as its sentences\index{sentence}.
% \end{note}

\red{
  \termdefinition{library}{collection of named \termref{OMS} and OMS networks\index{OMS network}, possibly written in different OMS languages\index{OMS language}, linked by named OMS mappings\index{OMS mapping}.}
}

\end{definitions}


\sclause{Native OMS, OMS, and OMS Languages}\label{c:native-oms}

\begin{definitions}

\termdefinition{native OMS}{A
collection of expressions (like non-logical symbols\index{non-logical symbol}, sentences\index{sentence} and structuring elements) from a given \termref{OMS language}.}
  \begin{example}
    An UML class diagram, an ontology written in OWL 2 EL, and  a specification written in CASLE are three different native OMS. 
  \end{example}
	\begin{note}
	An \termref{OMS} can be written in different \termref{OMS language} 	serializations\index{serialization}.
	\end{note}	


\termdefinition{OMS language}{language equipped with a formal, declarative, logic-based semantics,
plus non-logical annotations\index{annotation}.}
  \begin{example}
    OMS languages include OWL 2 DL, Common Logic, F-logic, UML class diagrams, RDF Schema, and OBO.
  \end{example}
  \begin{note}
  An OMS language is used for the formal specification of \termref{native OMS}.
  \end{note}
  \begin{note}
  We distinguish between the {logical language aspect}, the {structuring language aspect}, and the {annotation language aspect} of an OMS language. 
  \end{note}



%\begin{definitions}
\termdefinition{\THIS/ structured OMS}{A syntactically valid \THIS/ library (as defined in this \OMGSpec/) that contains a library definition (see section \ref{c:keywords}).}
  \begin{note}
   \THIS/ structured OMS, typically, use native OMS as building blocks for defining structured OMS, OMS mappings or OMS networks.  
  \end{note}
  \begin{note}
   All \THIS/ structured OMS are structured OMS. 
  \end{note}
	


\termdefinitionLight{OMS (ontology, specification or model)\index{OMS}}
{A native OMS or a \THIS/ structured OMS.}
\begin{note}
	An OMS is either a basic or a structured OMS.
\end{note}
\begin{note}
	An OMS has a single signature and model class over that signature as its model-theoretic semantics.
\end{note}



\begin{definitions}
\termdefinitionLight{basic OMS\index{basic OMS}\synonym flat OMS}{A native OMS that does not utilize any elements from the structuring language aspects of its language.}
  \begin{note}
    Basic OMS are self-contained in the sense that it semantics does not depend on some other OMS.  In particular, the OMS does not involve any importations.
  \end{note}
  \begin{note}
    Since a basic OMS has no structuring elements, it consists just of a \termref{signature} equipped with a set of sentences\index{sentence} and annotations\index{annotation}.
  \end{note}
	



  \termdefinitionLight{\termref{non-logical symbol}\synonym OMS symbol\index{OMS symbol|see {OMS symbol}
 }}{atomic expression or syntactic constituent of an \termref{OMS} that requires an interpretation through a \termref{model}.}
  \begin{note}
  This differs from the notion of ``atomic sentence'': such sentences
  may involve several non-logical symbols.
  \end{note}

  \begin{example}
    Non-logical symbols in OWL \nisref{W3C/TR REC-owl2-syntax:2009} (there called ``entities'') comprise
    \begin{itemize}
    \item individuals (denoting objects from the domain of discourse),
    \item classes (denoting sets of objects; also called concepts), and
    \item properties (denoting binary relations over objects; also called
      roles).
    \end{itemize}
    This is opposed to logical symbols in OWL, e.g., those for intersection
    and union of classes.
  \end{example}

\smallskip

  \begin{example}
    Non-logical symbols in Common Logic \nisref{ISO/IEC 24707:2007} comprise
    \begin{itemize}
    \item names (denoting objects from the domain of discourse),
    \item sequence markers (denoting sequences of objects).
    \end{itemize}
    This is opposed to logical symbols in Common Logic, e.g.\ logical connectives and
    quantifiers.
  \end{example}


\termdefinitionLight{\termref{signature}\synonym vocabulary}\index{vocabulary|see {signature}}
{set (or otherwise
  structured collection) 
of non-logical symbols\index{non-logical symbol} of an \termref{OMS}.}
   \begin{note}
     The signature of a term is the set of all non-logical symbols occurring
     in the \termref{term}. The signature of an \termref{OMS language} is the
     set of all non-logical symbols possible in that language.     
   \end{note}
   \begin{note}
    The signature of an OMS is usually uniquely determined.
   \end{note}


\termdefinition{model}{semantic interpretation of all non-logical symbols\index{non-logical symbol} of a \termref{signature}.}
  \begin{note}
    A model of an OMS is a model of the signature of the OMS
    that moreover satisfies all the axioms\index{axiom} of the OMS.
  \end{note}
  \begin{note}
  This term refers to \emph{model} in the sense of model theory (a
  branch of logic). It is not to be confused with \emph{model} in the
  sense of modeling (i.e., the ``M'' in OMS).
  \end{note}

  
\termdefinition{term}{syntactic expression either consisting of a single \termref{non-logical symbol} or recursively composed of other terms (a.k.a. its subterms).}
  \begin{note}
	  A term belongs to the logical language aspect of an OMS language.
  \end{note}

  
\termdefinition{sentence}{term that is either true or false in a given \termref{model}, i.e.\ which is assigned a truth value in this \termref{model}.}
  \begin{note}
In a \termref{model}, on the one hand, a sentence is always true or false. In an \termref{OMS}, on the
other hand, a sentence can have several logical statuses: it can be an axiom, if postulated to be true;
a theorem, if proven from other axioms and theorems; a conjecture, if expecting to be proven from 
other axioms and theorems; or have another of many possible statuses.
  \end{note}
  \begin{note}
  A sentence can conform to one or more signatures (namely those signatures
  containing all non-logical symbols used in the sentence).
  \end{note}
  \begin{note}
  It is quite common that sentences are required to be closed (i.e.\ have no
  free variables). However, this depends on the OMS language at hand.
  \end{note}
  \begin{note}
	  A sentence belongs to the logical language aspect of an OMS language.
  \end{note}


\termdefinition{axiom}{\termref{sentence} that is  postulated to be valid (i.e.\ true in every \termref{model}).}


  \termdefinition{theorem}{\termref{sentence} that has been proven from other axioms \index{axiom} and theorems\index{theorem}.}

  \termdefinition{satisfaction relation}{relation between models and sentences indicating which sentences hold true in the model.}

\red{
  \termdefinition{logical theory}{\termref{signature} equipped with a set of sentences\index{sentence} over the signature.}
}

\red{
 \termdefinitionLight{\termref{entailment}\synonym specialization}{relation between two \termref{OMS}
expressing that the second one is logically implied by the first one.}
\begin{note}
The converse is generalization.
\end{note}
}

\red{
  \termdefinition{query language}{\termref{OMS language} specifically dedicated to queries\index{query}.}
\begin{example}
SPARQL, Prolog
\end{example}
\begin{note}
There are also general purpose OMS languages, which can express both \termref{OMS} and queries.
\end{note}
}


\termdefinition{query}{\termref{sentence} containing query variables\index{query variable}
   that can be instantiated by a \termref{substitution}.}


\termdefinition{query variable}{\termref{symbol} that will be used in a \termref{query} and a
\termref{substitution}.}
  \begin{note}
   From an abstract point of view, query variables are just symbols; 
   they are used in a way
   that they will be substituted using a substitution.
   Many OMS languages have special notations for (query) variables.
  \end{note}
  \begin{note}
   Usually, query variables are the free variables of a sentence; there
   can be other (bound) variables.
  \end{note}
  \begin{note}
  If there are no variables in an OMS language, constants can be used as query
  variables.
  \end{note}


\termdefinition{substitution}{\termref{OMS mapping} that maps query variables\index{query variable} of one \termref{OMS} to complex terms\index{term} of another OMS.}



\termdefinition{answer substitution}{\termref{substitution} that, when applied to
   a given \termref{query}, turns the latter into a logical consequence of a
   given \termref{OMS}.}
\end{definitions}  




%%%%%%%%%%%%%%%%%%%%
\sclause{Semantic Web}\label{c:terms-semantic-web}
%%%%%%%%%%%%%%%%%%%%
\begin{definitions}

\termdefinition{resource\subjectfield{web}}{something that can be globally identified.}
  \begin{note}
    \nisref{IETF/RFC 3986:2005, Section 1.1} deliberately defines a resource as ``in a general sense \textelp{} whatever might be identified by \textins*{an IRI}''.  The original source refers to URIs, but \THIS/ uses the compatible IRI standard \nisref{IETF/RFC 3987:2005} for identification.
  \end{note}
  \begin{example}
Familiar examples include an electronic document, an image, a source of information with a 
consistent purpose (\eg, ``today's weather report for Los Angeles''), a service (\eg, an 
HTTP-to-SMS gateway), and a collection of other resources. A resource is not necessarily accessible 
via the Internet; \eg, human beings, corporations, and bound books in a library can also be 
resources. Likewise, abstract concepts can be resources, such as the operators and operands of a 
mathematical equation, the types of a relationship (\eg, ``parent'' or ``employee''), or numeric 
values (\eg, zero, one, and infinity). \nisref{IETF/RFC 3986:2005, Section 1.1}
  \end{example}



\termdefinition{element (of an OMS)}{any \termref{resource} in an \termref{OMS} (\eg a \termref{non-logical symbol}, a \termref{sentence}, a \termref{correspondence}, the \termref{OMS} itself, ...) or a named set of such \termref{resources}.}
  

\termdefinition{linked data}{structured data that is published on the Web in a machine-processable way, according to principles specified in \cite{BernersLee:LinkedData2006,BizerHeath09}.}
  \begin{note}
    The linked data principles (adapted from \cite{BernersLee:LinkedData2006} and its paraphrase at \cite{Wikipedia:LinkedData2011}) are the following:
    \begin{enumerate}
    \item Use IRIs as names for things.
    \item Use HTTP IRIs so that these things can be referred to and looked up (``dereferenced'') 
    by people and user agents.\footnote{I.e., the IRI is treated as a URL (uniform resource locator).}
    \item Provide useful machine-processable (plus optionally human-readable) information about the thing when its IRI is dereferenced, using standard formats.
    \item Include links to other, related IRIs in the exposed data to improve discovery of other related information on the Web.
    \end{enumerate}
  \end{note}

  \begin{note}
    RDF, serialized as RDF/XML \cite{W3C:REC-rdf-syntax-grammar-20140225}, is the most common format for publishing linked data.  However, its usage is not mandatory.
  \end{note}
  \begin{note}
    Using HTTP content negotiation \cite{rfc2616} it is possible to serve representations in different formats from the same URL. 
  \end{note}
\end{definitions}

\sclause{OMS Annotation and Documentation}\label{c:terms-annotation}
 
\begin{definitions}
  \termdefinition{annotation}{additional information without a logical semantics that is attached to an element\index{element (of an OMS)} of an \termref{OMS}.}
  \begin{note}\label{note:annotation-rdf}
Formally, an annotation is given as a
%$$(\text{subject}, \text{predicate}, \text{object})$$
triple as 
defined by \nisref{SOURCE: W3C/TR REC-rdf11-concepts:2014, Section 3.1}.  The subject of an annotation 
is an element of an OMS.  The predicate is an RDF property defined in an external OMS and 
describes in what way the annotation object is related to the annotation subject.
  \end{note}  
  \begin{note}
According to note~\ref{note:annotation-rdf} it is possible to interpret annotations under an RDF 
semantics.  ``Without a logical semantics'' in this definition means that annotations to an OMS are 
not considered sentences of that OMS.
  \end{note}


  \termdefinition{OMS documentation}{set of all annotations\index{annotation} to an \termref{OMS}, plus any other documents and explanatory comments generated during or after development or deployment of the OMS.}
  \begin{note}
    Adapted from \cite{SuarezFigueroaEtAl:OntologyGlossary2008}.
  \end{note}
\end{definitions}

\sclause{Structured OMS}

\red{
\termdefinition{structured OMS}
{\termref{OMS} that results from other (basic and structured) \termref{OMS} by \termref{import}, \termref{union}, \termref{combination}, \termref{renaming} or other structuring operations.}
\begin{note}
	  Structured OMS are either \THIS/ structured OMS or native OMS that utilize elements of their structuring language aspect. 
  \end{note}
	
	

\termdefinition{flattenable OMS}
{OMS that can be seen, by purely syntactical means, to be logically  equivalent to a flat OMS.}
\begin{note}
More precisely, an OMS is flattenable if and only if it is either a basic OMS or it is an \termref{extension},
 \termref{union}, translation, \termref{module extraction}, \termref{approximation}, \termref{filtering},
  or reference of named OMS involving only flattenable OMS. 
\end{note}


\termdefinition{elusive OMS}
{OMS that is not flattenable\index{flattenable OMS}.}
}



\termdefinition{subOMS}{\termref{OMS} whose sets of non-logical symbols\index{non-logical symbol} and sentences\index{sentence} are subsets of those present in a given larger \termref{OMS}.}


  \termdefinition{import}{reference to an \termref{OMS}  
   behaving as if it were verbatimly included; 
   also import of \termref{libraries}.}
  \begin{note}
Semantically, an import of $O_2$ into $O_1$ is equivalent to the verbatim inclusion of $O_2$ in place of the import declaration.
  \end{note}
  \begin{note}
    The purpose of $O_2$ importing $O_1$ is to make non-logical symbols and sentences of $O_1$ available in $O_2$.
  \end{note}
  \begin{note}
    Importing $O_1$ into $O_2$ turns $O_2$ into an extension of $O_1$.
  \end{note}
  \begin{note}
    An owl:import in OWL is an import.
  \end{note}
  \begin{note}
    The import of a whole library into another library is also called import.
  \end{note}
 
  \termdefinition{union}{aggregation of several \termref{OMS}
    to a new \termref{OMS}, without any renaming.}
 
  \termdefinition{renaming}{assignment of new names
   to some non-logical symbols\index{non-logical symbol} of an \termref{OMS}.}
\begin{note}
A renaming results in an \termref{OMS mapping} between the
original and the renamed OMS.
\end{note}

  \termdefinition{reduction}{restriction of an \termref{OMS} to a smaller \termref{signature}.}

\termdefinition{extension}{\termref{OMS} whose sets of non-logical symbols\index{non-logical symbol} and sentences\index{sentence} are supersets of those present in a given smaller \termref{OMS}.}



\termdefinition{extension mapping}{inclusion \termref{OMS mapping} between two
   OMS where the sets of non-logical symbols\index{non-logical symbol} and
   sentences\index{sentence} of the second OMS are supersets of those
   present in the first OMS.} 
\begin{note} 
The second OMS is said to extend the first, and is an extension of the
first OMS.
\end{note} 



\termdefinitionLight{consequence-theoretic conservative extension\index{conservative extension ! consequence-theoretic}}{extension that does
   not add new theorems\index{theorem} (in terms of the unextended \termref{signature}).}
  \begin{note}
    An extension $O_2$ of an OMS $O_1$ is a consequence-theoretic conservative extension, if all properties formulated in the signature of $O_1$ hold for $O_1$ whenever they hold for $O_2$.
  \end{note}


\termdefinitionLight{model-theoretic conservative extension\index{conservative extension ! model-theoretic}}{extension
   that does not lead to a restriction of class of \termref{model}s of an \termref{OMS}.}
  \begin{note}
    An extension $O_2$ of an OMS $O_1$ is a model-theoretic conservative extension, if all properties formulated in the signature of $O_1$ hold for $O_1$ whenever they hold for $O_2$.
  \end{note}
  \begin{note}
   Any model-theoretic conservative extension is also a consequence-theoretic one.
  \end{note}


\termdefinitionLight{conservative extension\index{conservative extension ! (general)}}{consequence-theoretic or model-theoretic conservative extension\index{conservative extension ! model-theoretic}.}
  \begin{note}
   If used without qualification, the consequence-theoretic version is meant.
  \end{note}


\termdefinition{monomorphic extension}{\termref{extension} whose newly introduced
   non-logical symbols\index{non-logical symbol} are interpreted in a way unique up to isomorphism.}
  \begin{note}
An \termref{extension} $O_2$ of an \termref{OMS} $O_1$ is a monomorphic extension, if each model of $O_1$ can be expanded to a model of $O_2$ that is unique up to isomorphism.
  \end{note}
  \begin{note}
    Each monomorphic extension is also a model-theoretic conservative extension but not vice versa.
  \end{note}

  \termdefinition{definitional extension}{\termref{extension} whose newly introduced
   non-logical symbols\index{non-logical symbol} are interpreted in a unique way.}
  \begin{note}
An \termref{extension} $O_2$ of an \termref{OMS} $O_1$ is a definitional extension, if each model of $O_1$ can be uniquely expanded to a model of $O_2$.
  \end{note}
  \begin{note}
    $O_2$ being a definitional extension of $O_1$ implies a bijective correspondence between the classes of models of $O_2$ and $O_1$.
  \end{note}
  \begin{note}
    Each definitional extension is also a monomorphic extension but not vice versa.
  \end{note}

  \termdefinition{weak definitional extension}{\termref{extension} whose newly introduced
   non-logical symbols\index{non-logical symbol} can be interpreted in at most one way.}
  \begin{note}
An \termref{extension} $O_2$ of an \termref{OMS} $O_1$ is a weak definitional extension, if each model of $O_1$ can be expanded to at most one model of $O_2$.
  \end{note}
  \begin{note}
    An extension is definitional if and only if it is both weakly definitional
   and model-theoretically conservative.
  \end{note}

  \termdefinition{implied extension}{model-theoretic conservative extension\index{conservative extension ! model-theoretic} that does not introduce new non-logical symbols\index{non-logical symbol}.}
  \begin{note}
    A conservative extension $O_2$ of an \termref{OMS}
    $O_1$ is an implied extension, if and only if the signature of
    $O_2$ is the signature of $O_1$.  $O_2$ is an implied extension of
    $O_1$ if and only if the model class of $O_2$ is the model class
    of $O_1$.
  \end{note}
  \begin{note}
    Each implied extension is also a definitional extension but not vice versa.
  \end{note}


\termdefinition{module}{\termref{subOMS} that conservatively extends to conservative extension  the whole \termref{OMS}.}
%\todonote[author=Christoph Lange]{a more formal definition, from \todonoteURL{http://iswc2011.semanticweb.org/fileadmin/iswc/Papers/PostersDemos/iswc11pd_submission_75.pdf}: Modules are subsets of
%OMS that preserve all entailments over a set of terms $\Sigma$ called seed signature.  Modules based on syntactic locality are defined in Cuenca Grau, B., Horrocks, I., Kazakov, Y., Sattler, U.: Modular reuse of ontologies: Theory and practice. J. of Artif. Intell. Research 31, 273–318 (2008)}}
  \begin{note}
The conservative extension can be either model-theoretic or consequence-theoretic; without
 qualification, the consequence-theoretic version is used.
  \end{note}
%\ednote{this is about coverage only. Should we also care about safety? No, see \url{https://github.com/tillmo/DOL/issues/23}.}


\termdefinition{module extraction}{activity of obtaining from an \termref{OMS} concrete 
modules\index{module} to be used for a particular purpose (\eg to contain a particular 
sub-\termref{signature} of the original \termref{OMS}).}
  \begin{note}
    Cited and slightly adapted from \cite{SuarezFigueroaEtAl:OntologyGlossary2008}.
  \end{note}
  \begin{note}
The goal of module extraction is ``decomposing an OMS into smaller, more manageable modules with
appropriate dependencies'' \cite{DBLP:series/lncs/5445}.
  \end{note}
  \begin{example}
Consider an OWL DL ontology about wines, from which we would like to extract a module about white 
wines. That module would contain the declaration of the non-logical symbol ``white wine'', all 
declarations of non-logical symbols related to ``white wine'', and all sentences about all of these 
non-logical symbols.
  \end{example}


\termdefinition{approximant}{approximation (in the sense of a logically implied theory, possibly 
after suitable translation)  of an OMS in a smaller \termref{signature} or a \termref{sublanguage}.}


\termdefinition{maximum approximant}{
best possible (in the sense of a maximum set of logical consequences)
\termref{approximant} of an OMS in a smaller \termref{signature} or a \termref{sublanguage}.}
\begin{note}
 Technically, a maximum approximant is a uniform interpolant, see \cite{DBLP:conf/ijcai/LutzW11}.
\end{note}


\termdefinition{closed world assumption}{presumption that what is not known to be true, is false.}

\termdefinitionLight{\termref{minimization}\synonym circumscription\index{circumscription|see {minimization}}}
{way of implementing the \termref{closed world assumption} by restricting the models\index{model} to those that are minimal.}
  \begin{note}
    See \cite{circ1}, \cite{circ2}.
  \end{note}

  \termdefinition{combination}{aggregation of all the OMS in an \termref{OMS network}, where \termref{non-logical symbol}s are shared according to the \termref{OMS mapping}s in the OMS network.}
\begin{example}
Consider an ontology involving a concept \texttt{Person},
and another one involving \texttt{Human being}, and an \termref{alignment}
that relates these to concepts. In the combination of the ontologies
along the alignment, there is only one concept, representing both
\texttt{Person} and \texttt{Human being}.
\end{example}

 
  \termdefinition{sharing}{property of \termref{OMS symbols} being mapped to the same symbol when computing a \termref{combination} of an \termref{OMS network}.}
 \begin{note}
  Sharing is always relative to a given OMS network that
  relates different OMS. That is, two given OMS symbols
  can share with respect to one OMS network, and not share with respect to some
  other OMS network.
 \end{note}

\sclause{Mappings Between OMS}\label{c:mappings}

   \termdefinitionLight{\termref{OMS mapping}\synonym link\subjectfield{OMS}}{relationship between two \termref{OMS}.}
  
%%   \termdefinition{logical OMS mapping}{\termref{OMS mapping} that has a formal, logic-based semantics}
%%   \begin{note}
%%     Logical OMS mappings are given as sets of symbol map items\index{symbol map item}, which generate \emph{signature morphisms}.
%%   \end{note}
%%   \begin{note}
%% Some specific kinds of logical OMS mappings will be introduced below.  
%%   \end{note}

 \termdefinition{symbol map item}{pair of symbols of two OMS, indicating how a symbol from the first OMS is mapped by a signature morphism to a symbol of the second OMS}
 \begin{note}
   A symbol map item is given as $s_1 \mapsto s_2$, where $s_1$ is a symbol from the \emph{source} OMS 
   and $s_2$ is a symbol from the \emph{target}  of the OMS mapping.
 \end{note}

  \termdefinitionLight{interpretation\index{interpretation}\synonym view\synonym refinement}{\termref{OMS mapping} that postulates a
specialization relation
 between two \termref{OMS}} along a morphism between their signatures.
  \begin{note}
    An interpretation typically leads to proof obligations, \ie one has to prove that 
  translations of axioms\index{axiom} of the source OMS along the morphism accompanying the interpretation are theorems in the target OMS.
  \end{note}

  \termdefinition{equivalence}
{\termref{OMS mapping} ensuring that two \termref{OMS} share the
  same definable concepts.}
  \begin{note}
    Two OMS are equivalent if they have a common definitional extension.
    The OMS may be written in different OMS languages.
  \end{note}

  \termdefinition{interface signature}{\termref{signature} mediating between an \termref{OMS} and a \termref{module} of that \termref{OMS} in the sense that it contains those non-logical symbols\index{non-logical symbol} that the sentences\index{sentence} of the \termref{module} and the sentences\index{sentence} of the \termref{OMS} have in common.}
  \begin{note}
    Adapted from \cite{CuencaGrauEtAl:ExtractingModulesOntologies2007}.
  \end{note}

  \termdefinition{module relation}{\termref{OMS mapping} stating that one \termref{OMS} is a \termref{module} of the other one.}


\termdefinition{alignment}{an \termref{OMS mapping} expressing a collection of semantic
relations between entities of the two OMS.}
\begin{note}
Alignments consist of correspondences\index{correspondence}, each of which may have a confidence value. If all
confidence values are 1, the alignment can be given a formal, logic-based semantics.
\end{note}

 \termdefinition{correspondence}{relationship between an \termref{non-logical symbol} $e_1$ from an \termref{OMS} $O_1$ and an \termref{non-logical symbol} $e_2$ from an OMS $O_2$, or between an \termref{non-logical symbol} $e_1$ from $O_1$ and a \termref{term} $t_2$ formed from non-logical symbols\index{non-logical symbol} from $O_2$.
  \begin{note}
A correspondence is given as a quadruple 
$(e_1, R, \left\{\begin{array}{c}e_2\\ t_2\end{array}\right\}, c)$,
where $R$ denotes the type of relationship that is asserted to hold between the two non-logical 
symbols/terms, and $0\le c\le 1$ is a confidence value.  $R$ and $c$ may be omitted: When $R$ is 
omitted, it defaults to the equivalence relation, unless another default
relation has been explicitly specified; when $c$ is omitted, it defaults to $1$.}
  \end{note}
  \begin{note}
     A confidence value of $1$ does not imply logical equivalence (\cf \cite{KutzEtAl:ChineseWhispers2010} for a worked-out example).
  \end{note}
  \begin{note}
     Not all OMS languages implement logical equivalence.  For example, OWL does not implement logical equivalence in general, but separately implements equivalence relations restricted to individuals (\textit{owl:sameAs}), classes (\textit{owl:equivalentClass}) and properties (\textit{owl:equivalentProperty}).
  \end{note}

  \termdefinition{matching}{algorithmic procedure that generates an \termref{alignment} for two given \termref{OMS}.}
  \begin{note}
    For both matching and alignment, see \cite{DBLP:books/daglib/0032976,KhanKeet13}.
  \end{note}

 
\termdefinitionLight{\termref{OMS network}\synonym distributed OMS\synonym hyperontology} graph with \termref{OMS} as nodes and OMS mappings\index{OMS mapping} as edges, showing how the OMS are interlinked.
%\ednote{Is ``hyperontology'' a synonym for ``OMS network'', or rather for
%``heterogeneous OMS''? For the former. ``Hyperontologies. introduce a notion of heterogeneously structured ontology, which also affords distributed networks of ontologies written in
%different formalisms, which we call hyperontologies.'' (from ``Carnap, Goguen, and the Hyperontologies'')}
\begin{note}
 In \cite{MossakowskiTarlecki09}, a distinction between focused and distributed heterogeneous specifications is made. In the terminology of this standard, this is the distinction between \termref{OMS} and OMS networks.
\end{note}
  \begin{note}
    An OMS network is a diagram of OMS in the sense of category theory, but different from a diagram
    in the sense of model-driven architecture.
  \end{note}
 \begin{note}
   The links between the nodes of a distributed OMS can be given using interpretations or alignments. Imports between the nodes
   of a  distributed OMS are automatically included in the distributed OMS. By including an interpretation or an alignment in a distributed 
   OMS, the involved nodes are automatically included.
 \end{note}
 \begin{example}
 Consider two ontologies and an \termref{interpretation} between them.  In the distributed OMS of the interpretation there are 
  two nodes, one for each ontology, and one edge from the source ontology to the target ontology of the interpretation. 
 \end{example}




\end{definitions}

\sclause{Features of OMS Languages}\label{c:terms-features}
 
\begin{definitions}
  \termdefinition{OMS language translation}{mapping from constructs in the source \termref{OMS language} to their equivalents in the target \termref{OMS language}.}
%
\begin{note}
  An OMS language translation shall satisfy the property that the
  result of a translation is a well-formed text in the target
  language.
\end{note}

\red{
\termdefinition{OMS language graph}{graph of OMS languages\index{OMS language} and
OMS language translations\index{language translation}, typically used in a \termref{heterogeneous environment}.}
\begin{note}
  In an OMS language graph, some of the OMS language translations can be
  marked to be default translations\index{default translation}.
\end{note}

\termdefinition{default translation}{specially marked \termref{OMS language
    translation} or \termref{logic translation} that will be used
  whenever a translation is needed and no explicit translation is
  given.} 
}

\red{
\termdefinition{heterogeneous environment}{environment for the
  expression of homogeneous and \termref{heterogeneous OMS}, comprising
a \termref{logic graph}, an \termref{OMS language graph} and 
\termref{supports relations}.}
\begin{note}
  Although in principle, there can be many heterogeneous environments,
  for ensuring \termref{interoperability}, there will be a global
  heterogeneous environment (maintained in some registry), with
  subenvironments for specific purposes.
\end{note}
}



  \termdefinition{sublanguage}{syntactically specified subset of a given language, consisting of a subset of its terminal and nonterminal symbols and grammar rules.}

 \termdefinitionLight{language aspect\index{language aspect ! (general)}}{set of language constructs of a given language, not necessarily forming a sublanguage.}

  \termdefinitionLight{logical language aspect\index{language aspect ! logical}}{the (unique) language aspect of an \termref{OMS language} that enables the expression of non-logical symbols\index{non-logical symbol} and sentences\index{sentence} in a logic.}

\termdefinitionLight{structuring language aspect\index{language aspect ! structuring}}{the (unique) language aspect of an \termref{OMS language} 
that covers \termref{structured OMS} as well as the relations of \termref{basic OMS} and \termref{structured OMS} 
to each other, including, but not limited to {imports}\index{import}, OMS mappings\index{OMS mapping}, conservative extensions\index{conservative extension ! (general)}, 
and the handling of prefixes for CURIEs.}

  \termdefinitionLight{annotation language aspect\index{language aspect ! annotation}}{the (unique) language aspect of an \termref{OMS language} that enables the  expression of comments and annotations\index{annotation}.}

  \termdefinition{profile}{(syntactic) \termref{sublanguage} of an \termref{OMS language} interpreting according to a particular \termref{logic}
that targets specific applications or reasoning methods.}
  \begin{example}
    Profiles of OWL 2 include OWL 2 EL, OWL 2 QL, OWL 2 RL, OWL 2 DL, and OWL 2 Full.
  \end{example}
  \begin{note}
  Profiles typically correspond to sublogics\index{sublogic}.
  \end{note}
  \begin{note}
  Profiles can have different logics\index{logic}, even with completely
  different semantics, e.g.\ OWL 2 DL versus OWL 2 Full.
  \end{note}
  \begin{note}
    The logic needs to support the language.
  \end{note}
  
\end{definitions}

\sclause{OMS Language Serializations}\label{c:term-serializations}

\begin{definitions}
  \termdefinition{serialization}{specific syntactic encoding of a given \termref{OMS language}.}
  \begin{note}
    Serializations serve as standard formats for exchanging OMS between tools.
  \end{note}
  \begin{example}
    OWL uses the term ``serialization''; the following are standard OWL serializations: OWL functional-style syntax, OWL/XML, OWL Manchester syntax, plus any standard serialization of RDF (\eg RDF/XML, Turtle, \dots).  However, RDF/XML is the only one tools are required to implement.
  \end{example}
  \begin{example}
Common Logic uses the term ``dialect''; the following are standard Common Logic dialects: Common Logic Interchange Format (CLIF), Conceptual Graph Interchange Format (CGIF), eXtended Common Logic Markup Language (XCL).
  \end{example}


   \termdefinition{document}{result of serializing an OMS using a given serialization.}


  \termdefinition{standoff markup}{way of providing {annotations}\index{annotation} to subjects in external resources, without embedding them into the original resource (here: \termref{OMS}).}
\end{definitions}

\sclause{Logic}\label{c:term-logic}

\begin{definitions}
  \termdefinition{logic}{specification of valid reasoning that comprises signatures\index{signature}, sentences\index{sentence},
models \index{model}, and a \termref{satisfaction relation} between models\index{module} and sentences\index{sentence}.}
  \begin{note}
    Most OMS languages have an underlying logic.
  \end{note}
  \begin{example}
    $\mathcal{SROIQ}(D)$ is the logic underlying OWL 2 DL.
  \end{example}
  \begin{note}
   See annex~\ref{a:lola} for the organization of the
   relation between OMS languages and their logics and serializations.
  \end{note}

\red{ 
  \termdefinition{supports relation}{relation between OMS
      languages\index{OMS language} and logics\index{logic} expressing the \termref{logical
      language aspect} of the former, namely that the constructs of
    the former lead to a \termref{logical theory} in the latter.} 
}
\begin{note}
There is also a supports relation between OMS languages and serializations.
\end{note}

 \termdefinition{institution}{metaframework mathematically formalizing
the notion of a \termref{logic}.}
\begin{note}
 See clause~\ref{c:semantics} for a formal definition.
\end{note}

  \termdefinition{logic translation}{mapping of a source
    \termref{logic} into a target \termref{logic} (mapping
    signatures\index{signature}, sentences\index{sentence} and models\index{model})
    that keeps or encodes the logical content of \termref{OMS}.}

  \termdefinition{logic reduction}{mapping of a source \termref{logic}
    onto a (usually less expressive) target \termref{logic} (mapping
	signatures\index{signature}, sentences\index{sentence} and models\index{model})
    that simply forgets those parts of the logical structure not
    fitting the target \termref{logic}.}

\termdefinition{theoroidal logic translation} translation that maps 
signatures of the source logic to theories (i.e.~signatures and sets of sentences)
of the target logic. 
\begin{example}
 The translation from OWL to multi-sorted first-order logic translates each OWL built-in type
 to its first-order axiomatization as a datatype.
\end{example}

\termdefinition{sublogic}{a \termref{logic} that is a syntactic restriction of another logic, inheriting its semantics.}

\red{
\termdefinition{logic graph}{graph of logics\index{logic}, logic 
translations\index{logic translation} and logic reductions\index{logic reduction}, typically used in a \termref{heterogeneous environment}.}
\begin{note}
  In a logic graph, some of the logic translations and reductions can be
  marked to be {default translations}\index{default translation}.
%  \ednote{Hopefully it is OK to subsume the notion of logic reduction
%  under the term ``translation'' here.}
\end{note}

}

\red{
  \termdefinition{homogeneous OMS}{\termref{OMS} whose parts are all formulated in one and the same \termref{logic}.}
\begin{note}
Opposite of \termref{heterogeneous OMS}.
\end{note}

  \termdefinition{heterogeneous OMS}{\termref{OMS} whose parts are formulated in different logics\index{logic}.}
\begin{note}
Opposite of \termref{homogeneous OMS}.
\end{note}
\begin{example}
See section~\ref{dist-het-onto}.
\end{example}
}

\termdefinition{logic approximation}{mapping of a source \termref{logic} onto a (usually less
expressive) target \termref{logic} that tries to approximate the OMS expressed in the source
\termref{logic} with means of the expressivity of the target \termref{logic}.}
\begin{note}
  A unique maximal approximation need not exist.
\end{note}
\begin{note}
 The target logic typically is a \termref{sublogic} of the source logic.
\end{note}


\end{definitions}
  
\sclause{Interoperability}

%~\todonote[author=Christoph Lange,type=todo]{possibly define some notion of ``interoperability''
%that is tailored to this \OMGSpec/.  At least we need to be able to speak about overall consistency, 
%alignments, etc.}\\
%~\todonote[author=Christoph Lange,type=fyi]{Definitions in earlier drafts were not quite helpful:\textLF
%{\textbullet} OMS integration := ``combination of different OMS into a coherent whole, via alignments''\textLF
%{\textbullet}OMS interoperability := ``relation among OMS (via OMS alignments) with the goal of using them jointly in an application scenario''\textLF
%AENOR commented on the latter: ``The definition of this term needs some revision and more precision 
%in the document as for the real criteria that shall be applied to evaluate the degree of 
%interoperability between OMS.''}\\

\begin{definitions}

\termdefinition{OMS integration} {the union of OMS which preserves the satisfaction and entailment relations among constituent OMS.}

  \termdefinition{logically interoperable}{property of \termref{structured OMS}, which may be written in different OMS languages\index{OMS language} supporting different logics\index{logic}, of being usable jointly in a coherent way (via suitable OMS language translations), such that the notions of their overall consistency and logical entailment have a precise logical semantics.}
\end{definitions}
\begin{note}
Within ISO 19763 and ISO 20943, metamodel interoperability is
equivalent to the existence of mapping, which are statements that the
domains represented by two models intersect and there is a need to
register details of the correspondence between the structures in the
models that semantically represent this overlap. Within these
standards, a model is a representation of some aspect of a domain of
interest using a normative modeling facility and modeling
constructs.

The notion of logical interoperability is distinct from the notion of 
interoperability used in 
ISO/IEC 2381-1 Information Technology Vocabulary -- Part 1: Fundamental Terms,
which is restricted to
the capability to communicate, execute programs, or transfer data among 
various hardware or software entities 
in a manner that requires the user to have little or no knowledge of the 
unique characteristics of those entities.
\end{note}

\termdefinition{OMS interoperability} {relation among OMS (via OMS alignments)
which are logically interoperable.}

\chapter{Symbols}

As listed below, these symbols and abbreviations are generally for the main clauses of the \OMGSpec/. Some annexes may introduce their own symbols and abbreviations which will be grouped together within that annex.

\begin{symbols}
\symboldef{CASL}{Common Algebraic Specification Language, specified by the Common Framework Initiative}
\symboldef{CGIF}{Conceptual Graph Interchange Format}
\symboldef{CL}{Common Logic }
\symboldef{CLIF}{Common Logic Interchange Format}
\symboldef{CORBA}{Common Object Request Broker Architecture}
\symboldef{CURIE}{Compact URI expression}
\symboldef{CWM}{Common Warehouse Metamodel}
\symboldef{DDL}{Distributed description logic}
\symboldef{DOL}{Distributed Ontology, Model and Specification Language}
\symboldef{DTV}{Date-Time Vocabulary}
\symboldef{EBNF}{Extended Backus-Naur Form}
\symboldef{E-connections}{a modular ontology language (closely related to DDL)}
\symboldef{F-logic}{frame logic, an object-oriented ontology language}
\symboldef{IDL}{Interface Definition Language}
\symboldef{IIOP}{Internet Inter-ORB Protocol}
\symboldef{IRI}{Internationalized Resource Identifier}
\symboldef{MDA}{Model Driven Architecture}
\symboldef{MOF}{Meta-Object Facility}
\symboldef{OCL}{Object Constraint Language}
\symboldef{OWL 2}{Web Ontology Language (W3C), version 2: family of knowledge representation languages for authoring ontologies}
\symboldef{OWL 2 DL}{description logic profile of OWL 2}
\symboldef{OWL 2 EL}{a sub-Boolean profile of OWL 2 (used often \eg in medical ontologies)}
\symboldef{OWL 2 Full}{the language that is determined by RDF graphs being interpreted 
using the OWL 2 RDF-Based Semantics \cite{W3C:REC-owl2-rdf-based-semantics-20091027}}
\symboldef{OWL 2 QL}{profile of OWL 2 designed to support fast query answering over large amounts of data}
\symboldef{OWL 2 RL}{fragment of OWL 2 designed to support rule-based reasoning}
\symboldef{OWL 2 XML}{XML-based serialization of the OWL 2 language}
\symboldef{P-DL}{Package-based description logic}
\symboldef{PIM}{Platform-independent Model}
\symboldef{PSM}{Platform-specific Model}
\symboldef{RDF}{Resource Description Framework, a graph data model}
\symboldef{RDFS}{RDF Schema}
\symboldef{RDFa}{a set of XML attributes for embedding RDF graphs into XML documents}
\symboldef{RDF/XML}{an XML serialization of the RDF data model}
\symboldef{RIF}{Rule Interchange Format}
\symboldef{SBVR}{Semantics of Business Vocabulary and Business Rules}
\symboldef{SMOF}{MOF Support for Semantic Structures}
\symboldef{UML}{Unified Modeling Language}
\symboldef{URI}{Uniform Resource Identifier}
\symboldef{URL}{Uniform Resource Locator}
\symboldef{W3C}{World Wide Web Consortium}
\symboldef{XMI}{XML Metadata Interchange}
\symboldef{XML}{eXtensible Markup Language}
\end{symbols}


\chapter{Additional Information}
\section{Changes to Adopted OMG Specifications}
This specification does not require or request any change to any other OMG specification. 

\section{How to Read This Specification}
The initial eight chapters of this specification are \emph{informative} providing  a high-level
 summary of usage scenarios and goals (Chapter \ref{c:goal}) and an overview over the design of
\THIS/  (Chapter \ref{c:design}).

\medskip \noindent 
Chapter \ref{c:abstract-syntax} defines the abstract syntax of \THIS/ (\emph{normative}) in Extended
Backus–Naur Form (EBNF).  
Chapter \ref{a:text-syntax} provides a human friendly text serialization of the abstract syntax of 
\THIS/ (\emph{normative}). 
Annex \ref{a:MOF} contains the abstract syntax specified as an SMOF compliant meta model.
(\emph{informative}).

\medskip \noindent Chapter \ref{c:semantics} defines the
model-theoretic semantics of \THIS/ on the abstract syntax, and also
makes the notion of heterogeneous logical environment (providing
languages, logics and translations) precise (\emph{normative}).

\medskip \noindent Annex \ref{a:lola} specifies an RDF vocabulary for
the terms in chapter~\ref{terms-and-defs}, and for OMS languages and
translation that conform with \THIS/  (\emph{normative}).

\medskip \noindent Various languages are shown to  conform to \THIS/ in
informative annexes: OWL2 (annex \ref{a:owl}), Common Logic
(annex~\ref{a:cl}), RDF and RDF Schema (annex~\ref{a:rdfs}), UML class
diagrams (annex~\ref{a:uml-class}, EMOF (annex~\ref{a:EMOF}), and
%CASL (annex \ref{a:casl}).

\medskip \noindent 
Annex \ref{a:graph}  provides a core graph of logics and translations, covering those OMS languages
whose conformance with \THIS/ is established in the preceding annexes (\emph{informative}). 
Annex \ref{a:ext-graph} extends the graph presented in Annex \ref{a:graph}  by a list of OMS
language whose conformance with \THIS/ will be established by a registry
(\emph{informative}).

\medskip \noindent 
Annex \ref{a:uses} provides of \THIS/ texts, which provide examples for all \THIS/ constructs, which 
are specified in the abstract syntax 
(\emph{informative}).
Annex \ref{a:use-cases} sketches scenarios that outline how \THIS/ is intended to be applied. For 
each scenario, we list its status of implementation, the \THIS/ features it makes use of, and 
provide a brief description
(\emph{informative}).

Annex~\ref{a:tools} gives an overview of available  software tools for
\THIS/.  Annex~\ref{a:loc/id} discusses the implementation of a
linked-data compliant IRI scheme used in one of these tools
(\emph{informative}).

\medskip \noindent 
The bibliography contains \ref{a:bibliography} references to the literature that is cited in this document
(\emph{informative}).




%\section{About this Specification}

\section{Acknowledgments}
\subsection{Submitting and supporting organizations}
The following  OMG  members are submitting this specification:
	\begin{itemize}
		\item Fraunhofer FOKUS
		\item MITRE		
		\item Thematix Partners LLC
	\end{itemize}
The following organizations are supporting this specification: 
	\begin{itemize}
		\item Otto-von-Guericke University Magdeburg 
		\item Athan Services 
	\end{itemize}




\subsection{Participants}
The following people contributed directly to the development of this specification. 
	\begin{itemize}
	\item Tara Athan, Athan Services, USA 
	\item Elisa Kendall, Thematix Partners LLC, USA	
	\end{itemize}
\ednote{[Tara Athan, 2015-06-09] TODO: Add additional participants}
%	






%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%% 
%%%%%%%%%%%%%%%% 

\chapter{Goals and Usage Scenarios} \label{c:goal}


Often, engineering tasks require the use of several different OMS, which represent knowledge about 
a given domain or specify a given system from different perspectives or for different purposes.
(E.g., a software engineer will typically use different OMS to model different aspects of a software
 system,  including its behavior, its components, and its interactions with other systems.)  Further, the OMS are often represented in different OMS languages (e.g., UML class diagrams, OWL, or Common Logic), which may differ in style, expressivity, and different computational properties. 

The use of different OMS within the same context leads to  several 
challenges in the design and deployment of OMS, which have been addressed by current research in 
ontological engineering, formal software specification and formal modeling:
\begin{itemize}
\item How can we support shareability and reusability of OMS within the same domain?
\item How can we merge OMS in different domains, particularly in the cases 
in which the OMS are axiomatized in different logical languages?
\item What notions of modularity play a role when only part of an OMS is being shared or reused?
\item What are the relationships between versions of an OMS axiomatized in different logical languages?
\end{itemize}


To illustrate these challenges, in this clause we present a set of usage scenarios that involve the use of more than one OMS. These scenarios address the areas of ontology design, formal specification, and model-driven development. In spite of their many differences, they  all highlight one common theme:  
 the use of multiple OMS leads to interoperability challenges. 


The purpose of \THIS/ is to provide  a
standardized representation language, which can be used to represent structured OMS and the relations 
between OMS as part of OMS networks in a semantically well-defined way. Thus, tools that implement \THIS/ are able to integrate different OMS into a coherent whole, thereby enabling users of \THIS/ to overcome the different kind of interoperability issues that illustrated by the usage scenarios in this clause.  


\section{Use Case Onto-1: Interoperability Between OWL and FOL Ontologies}

In order to achieve interoperability during ontology development it is often necessary to describe 
concepts in a language more expressive than OWL.  Therefore, it is common practice to informally 
annotate OWL ontologies with FOL axioms (e.g., Keet's mereotopological ontology [Part-Whole], 
Dolce Lite [Dolce-lite], BFO-OWL). OWL is used because of better tool support, FOL because of 
greater expressiveness. However, relegating FOL axioms to  informal annotations means that these 
are not available for machine processing.  Another example of this problem is the following: For 
formally representing concept schemes (including taxonomies, thesauri and classification schemes) 
and provenance information there are the two W3C standards SKOS (Simple Knowledge Organization 
System) and PROV, as well as \ednote{CL: Did we mean something like “ISO 12345” here, i.e.\ some 
specific ISO standard that we reference by number? Terry: (re: footnote 29) Probably the family headed by ISO 11179 Information Technology -- Metadata registries (MDR) (http://metadata-stds.org/)
The 11179 standard is a multipart standard that includes the following parts:·         '          Part 1: Framework
·         Part 2: Classification
·         Part 3: Registry metamodel and basic attributes
·         Part 4: Formulation of data definitions
·         Part 5: Naming and identification principles
·         Part 6: Registration
Other standards in the series are 
ISO 19583  Concepts and usage of metadata
ISO 19763-* Metamodel interoperability
ISO 19773   Metadata modules
ISO 24706   Metadata for technical stds
ISO 24707   Common logic}ISO and other domain-specific  standards for 
metadata representation. The semantics for the SKOS and PROV languages are largely specified as OWL 
ontologies; however, as OWL cannot capture the full semantics, the rest is specified using some 
informal first-order rules. In other words, valid instance models that use SKOS or PROV may be 
required to satisfy both OWL and FOL axioms. When solving reasoning tasks over either SKOS or PROV 
ontologies, OWL reasoners are not able to consider the  FOL axioms. Hence, the information 
contained in these axioms is lost.

\THIS/ allows the user to replace such informal annotations by formal axioms in a suitable ontology 
language. The relation between the ontology and the FOL axioms is that of a heterogeneous 
import. In the result, both the and the FOL axioms are amenable to, e.g., automated consistency 
checks and theorem proving. Hence, all available information can be used in the reasoning process.
For example, the ontology below extends the definition of \texttt{isProperPartOf} as an asymmetric relation
with a first-order axiom (in Common Logic) asserting that the relation is also transitive.

can express transitivity, but not together with asymmetry.

\section{Use Case Onto-2: Ontology Integration by Means of a Foundational Ontology}
One major use case for ontologies in industry is to achieve interoperability and data integration. 
However if ontologies are developed independently and used  within the same domain, the 
differences between the ontologies may actually impede interoperability. One strategy to avoid this 
problem is the use of a shared  foundational ontology (e.g., DOLCE or BFO), which can be used to 
harmonize different domain ontologies. One challenge for this approach is that foundational 
ontologies typically rely on expressive ontology languages (e.g., Common Logic), while domain 
ontologies may be represented in languages that are optimized for performance (e.g., OWL EL). For 
this reason, currently the role of the foundational ontology is mainly to provide a conceptual 
framework that may be reused by the  domain ontologies; further, watered-down versions of the 
foundational ontologies in OWL (like DOLCE-lite or the OWL version of BFO) are used as basis for 
the  development of domain ontologies, be this as is, in an even less expressive version (e.g., a 
DOLCE-lite in OWL 2 EL), or only a relevant subset thereof (e.g., only the branch of endurants). A 
sample orchestration of interactions between the foundational and domain ontologies in various 
languages is depicted in Figure \ref{f:DOL-mapping} below.

\THIS/  provides the framework for integrating different domain ontologies, aligning these to 
foundational ontologies [Alignment1-2] and combining the aligned ontologies into a coherent 
integrated ontology -- even across different ontology languages. Thus, \THIS/  enables ontology 
developers to utilize the complete, and most expressive, foundational ontologies for ontology 
integration and validation purposes. 

The foundational ontology (FO) repository Repository of Ontologies for MULtiple USes (ROMULUS)\footnote{See \url{http://www.thezfiles.co.za/ROMULUS/home.html}}
contains alignments\index{alignment} between a number of foundational ontologies, expressing semantic relations between the aligned
entities. We select three such ontologies, containing spatial and temporal concepts: DOLCE\footnote{See \url{http://www.loa.istc.cnr.it/DOLCE.html}}, GFO\footnote{See \url{http://www.onto-med.de/ontologies/gfo/}} and BFO\footnote{See \url{http://www.ifomis.org/bfo/}}, and present alignments between them 
using \THIS/ syntax:


\section{Use Case Onto-3: Module Extraction From Large Ontologies}\label{onto-3}
Especially in the biomedical domain, ontologies tend to become very large (e.g., SNOMED CT, FMA) 
with over 100000 concepts and relationships. Yet, none of these ontologies covers all aspects of a 
domain, and frequently provide coverage at various levels of specificity, with excessive detail in 
some areas that may not be required for all usage scenarios. Often, for a given knowledge 
representation problem in industry, only relevant knowledge from two such large reference 
ontologies needs to be integrated, so a comprehensive integration would be both unfeasible and 
unwieldy. Hence, parts (modules) of these ontologies are obtained by selecting the concepts and 
relationships (roles) relevant for the intended application. An integrated version will then be 
based on these excerpts from the original ontologies (i.e., modules). For example, the Juvenile 
Rheumatoid Arthritis ontology JRAO has been created using modules from the NCI thesaurus and GALEN 
medical ontology. (See \ednote{CL: can we please have a vector graphic here?}\fref{JRAO}) \THIS/  
supports the description of such subsets (modules) of ontologies, as well as their alignment and 
integration.





\section{Use Case Onto-4: Interoperability Between Closed-World Data and Open-World Metadata}
Data collection has become easier and much more widespread over the years. This data has to be 
assigned a meaning somehow, which occurs traditionally in the  form of metadata annotations. For 
instance, consider geographical datasets derived from satellite data and raw sensor readings. 
Current implementations in, e.g., ecological economics\cite{bagstad_aries_2011} require manual 
annotation of datasets with the information relevant for their processes. While there have been 
attempts to standardize such information\cite{european_comission_inspire_2014}, metadata for 
datasets of simulation results are more difficult to standardize. Moreover, it is 
resource-consuming to link the data to the metadata, to ensure the metadata itself is of good 
quality and consistent, and to actually exploit the metadata when querying the data for data 
analysis. 

The data is usually represented in a database or RDF triple store, which work with a \termref{closed world assumption} on the dataset, and are not expressive enough to 
incorporate the metadata `background knowledge', such as the conditions for validity of the physical laws in the model of the object of observation. These metadata 
require a more expressive language, such as OWL or Common Logic, which operate under an open-world semantics. However, it is unfeasible to translate the 
whole large dataset into OWL or first-order logic. To `meet in the middle', it is possible to declare bridge rules (i.e., a mapping layer) that can link the metadata to 
the data. This approach can be used for intelligent data analysis that combines the data and metadata through querying the system. It enables the analysis of the 
data on the conceptual layer, instead of users having to learn the SQL/SPARQL query languages and how the data is stored. There are various tools and theories 
to realize this, which is collectively called Ontology-Based Data Access/Management, see also [OBDA].

The languages for representing the metadata or ontology, for representing the bridge rules or mapping assertions, and for representing the data are different yet 
they need to be orchestrated and handled smoothly in the system, be this for data analytics for large enterprises, for formulating policies, or in silico biology in the 
sciences. 

\THIS/  provides the framework for expressing such bridge rules in a systematic way, maintaining these, and building tools for them. 


\section{Use Case Onto-5: Verification of Rules Translating Dublin Core Into PROV}
The Dublin Core Metadata terms, which have been formalized as an RDF Schema vocabulary, developed initially by the digital library community, are less 
comprehensive but more widely used than PROV (cf. Use Case Onto-1). The rules for translating Dublin Core to the OWL subset of PROV (and, with restrictions, 
vice versa) are not known to yield valid instances of the PROV data model, i.e. they are not known to yield OWL ontologies consistent with respect to the OWL axioms that 
capture part of the PROV data model. This may disrupt systems that would like to reason about the provenance of an entity, and thus the assessment of the 
entity's quality, reliability or trustworthiness.
The Dublin Core to PROV ontology translation%
\footnote{\url{http://www.w3.org/TR/2013/NOTE-prov-dc-20130430/}}
  is expressed partly by a symbol mapping and partly by FOL rules. These FOL rules are implemented by CONSTRUCT patterns in the SPARQL RDF query language.%
\footnote{E.g., \url{http://www.w3.org/TR/2013/NOTE-prov-dc-20130430/\#dct-creator}} 
SPARQL has a formal specification of the evaluation semantics of its algebraic expressions, which is different from the model-theoretic semantics of the OWL and RDF Schema languages; nevertheless SPARQL CONSTRUCT is a popular and immediately executable syntax for expressing translation rules between ontologies in RDF-based languages in a subset of FOL.
\THIS/  not only supports the reuse of the existing Dublin Core RDF Schema and PROV OWL ontologies as modules of a distributed ontology (= OMS network), but it is also able to support the description of the FOL translation rules in a sufficiently expressive ontology language, e.g. Common Logic, and thus enable formal verification of the translation from Dublin Core to PROV.


\section{Use Case Spec-1: Modularity of Specifications}\label{spec-1}
Often specifications become so large that it is necessary to structure
them in a modular way, for human readability and maintainability, and for more efficient tool support. The lack of a standard for such
modular structuring hinders interoperability among different
development efforts and the reuse of specifications.  \THIS/ provides a
notion of structured modular specification that is equally applicable
to all \THIS/-conforming logical languages.

Structuring pays off even for small specifications. For example, it makes
structuring a simple specification of sorting lists in the 
following way enhances both readability and potential for re-use
of specifications:


In the last step, the structuring operation of hiding is used to
restrict the specification to an export interface: we hide the
predicates \texttt{is\_ordered} and \texttt{permutation}, because they
are only auxiliary and need not be implemented.


\section{Use Case Spec-2: Specification Refinements}\label{spec-2}
Formal software and hardware development methods are often used to
ensure the correct function of systems which have safety-critical
requirements or which may not be easily accessible for repair or
replacement.  Examples of such requirements can be found in
safety-critical areas such as medical systems, or in the automotive,
avionics and aerospace industries, as well as in components used by
those industries such as in microprocessor design.

Typically, a requirement specification is refined into a
design specification and then an implementation, often involving
several intermediate steps (see, e.g. the V-model [V-model], although
this does not require formal specification).  There are numerous
specification formalisms in use, including the OMG's SysML language;
moreover, often during development, the formalism needs to be changed
(e.g. from a specification to a programming language, or from a
temporal logic to a state machine). For each of these formalisms,
notions of refinement have been defined and implemented. However, the
lack of a standardized, logically sound language and methodology for
such refinement hinders interoperability among different development
efforts and the reuse of refinements.  \THIS/ provides the capability to
represent refinement that is equally applicable to all \THIS/-conforming
logical languages, and that covers at least the most relevant of the
industrial use cases of specification refinement.

A simple example is the refinement of the (purely declarative) sorting
specification from use case in section \ref{spec-1} into a specification of a particular sorting
algorithm (for simplicity, we choose insert sort):

Note that hiding is essential here to make the signatures of
both specifications compatible. If we had not hidden the
predicates \texttt{is\_ordered} and \texttt{permutation}
in the \texttt{Sorting} specification, a refinement would
not have been possible, since \texttt{InsertSort} does not
implement these predicates (and it would be rather artificial
to add an implementation for them).

\medskip

Refinements can be composed. A simple example below illustrates this
by expressing that natural numbers with addition form a monoid, and
that natural numbers can be efficiently represented for implementation
as lists of binary digits, together with several equivalent ways of
composing these refinements.




\section{Use Case Model-1: Consistency Among UML Diagrams of Different Types}
\label{model-1}

A typical UML model involves diagrams of different types. Such UML models may have intrinsic errors because diagrams of different types may specify conflicting 
requirements. Typical questions that arise in this context are, e.g.,

\begin{itemize}
\item whether the multiplicities in a class diagram are consistent with each other;
\item wether the attributes and operations in a state machine are
available in a class diagram;
\item	  whether the sequential composition of actions in an interaction diagram is justified by an accompanying OCL specification;
\item 	whether cooperating state machines comply with pre-/post-conditions and invariants;
\item 	whether the behavior prescribed in an interaction diagram is realizable by several state machines cooperating according to a composite structure diagram.
\end{itemize}
Such questions are currently hard to answer in a systematic manner. One method to answer these questions and find such errors is a check for semantic 
consistency. Under some restrictions, the proof of semantic consistency can be (at least partially) performed using model-checking tools like Hugo/RT \cite{knapp-wuttke:models06wsh:2007}. 
Once a formal semantics for the different diagram types has been chosen (see, e.g. \cite{knapp-mossakowski-roggenbach:corr:2014}), it is possible to use \THIS/ to specify in which 
sense the diagrams need to be consistent, and check this by suitable tools.


\ssclause{The ATM Example}
\label{sec:atm-example}

We present as a small example in model-driven development using UML,
taken from \cite{knapp-mossakowski-roggenbach:corr:2014}.  It involves
the design of a traditional automatic teller machine (ATM) connected
to a bank. For simplicity, we only describe the handling of entering a
card and a PIN with the ATM. After entering the card, one has three
trials for entering the correct PIN (which is checked by the
bank). After three unsuccessful trials the card is kept.


Figure~\ref{fig:interaction} shows a possible \emph{interaction}
between an \uml{atm} and a \uml{bank} object, which consists of
four messages: the \uml{atm} requests the \uml{bank} to \uml{verify}
if a card and PIN number combination is valid, in the first case the
\uml{bank} requests to reenter the PIN, in the second case the
verification is successful.  This interaction presumes that the system
has an \uml{atm} and a \uml{bank} as objects. This can, e.g., be
ensured by a \emph{composite structure diagram}, see
Fig.~\ref{fig:system}, which -- among other things -- specifies the
objects in the initial system state.  Furthermore, it specifies that
the communication between \uml{atm} and \uml{bank} goes through the
two ports \uml{bankCom} and \uml{atmCom} linked by a connector.  The
communication protocol on this connector is captured with a
\emph{protocol state machine}, see Fig.~\ref{fig:psm}.  The protocol
state machine fixes in which order the messages \uml{verify},
\uml{verified}, \uml{reenterPIN}, and \uml{markInvalid} between
\uml{atm} and \uml{bank} may occur.  Figure~\ref{fig:class} provides
structural information in form of an interface specifying what is
provided at the \uml{userCom} port of the \uml{atm} instance. An
interface is a set of operations that other model elements have to
implement. In our case, the interface is described in a \emph{class
  diagram}. Here, the operation \uml{keepCard} is enriched with the
OCL constraint \uml{trialsNum >= 3}, which refines its semantics:
\uml{keepCard} can only be invoked if the OCL constraints holds.

Finally, the dynamic behaviour of the \uml{atm} object is specified by
the \emph{behavioral state machine} shown in
Fig.~\ref{fig:state-machine}. The machine consists of five states
including \uml{Idle}, \uml{CardEntered}, etc.  Beginning in the
initial \uml{Idle} state, the user can \emph{trigger} a state change
by entering the \uml{card}. This has the \emph{effect} that the
parameter \uml{c} from the \uml{card} event is assigned to the
\uml{cardId} in the \uml{atm} object (parameter names are not shown on
triggers). Entering a \uml{PIN} triggers another transition to
\uml{PINEntered}.  Then the ATM requests verification from the bank
using its \uml{bankCom} port.  The transition to \uml{Verifying} uses
a \emph{completion event}: No explicit trigger is declared and the
machine autonomously creates such an event whenever a state is
completed, i.e., all internal activities of the state are finished (in
our example there are no such activities).  If the interaction with
the bank results in \uml{reenterPIN}, and the \emph{guard}
\uml{trialsNum < 3} is true, the user can again enter a \uml{PIN}.


The ATM example in Fig.~\ref{fig:atm-example} consists of five different
models, which naturally form a network. Coherence of this network
is expressed as its consistency.
We assume that XMI representations of the
relevant UML models have been stored at
\url{http://www.example.org/uml/}, that is under URL
\url{http://www.example.org/uml/xxx.xmi}, where \url{xxx} is
determined as follows:\medskip

\begin{tabular}{|l|l|l|}\hline
\textbf{Figure} & \textbf{\texttt{xxx}} & \textbf{diagram type}\\\hline
Fig.~\ref{fig:interaction} & sd & sequence diagram\\\hline
Fig.~\ref{fig:system} & cmp & composite structure diagram\\\hline
Fig.~\ref{fig:psm} & psm & protocol state machine\\\hline
Fig.~\ref{fig:class} & cd & class diagram\\\hline
Fig.~\ref{fig:state-machine} & stm & state machine\\\hline
\end{tabular}

Here, \texttt{abstract\_to\_concrete\_atm} is defined in the next
section, and \texttt{stm2cd} and \texttt{psm2cd} are suitable logic
projections extracting the classes, attributes and operations from a
(protocol) state machine, delivering a class diagram.

\section{Use Case Model-2: Refinements Between UML Diagrams of Different Types, and Their Reuse}
\label{model-2}

A problem is a lack of reusability of refinements: Consider a controller for an elevator, which is specified with a UML protocol state machine, enriched with UML 
sequence diagrams and OCL constraints. Assume further that this model is not directly implemented, but first refined to a UML behavior state machine (which then 
can be automatically or semi-automatically transformed into some implementation using standard UML tools). However, there is no standardized language to 
express, document and maintain the refinement relation itself (UML only allows very simple refinements, namely between state machines). This hinders both the 
reuse of such refinements in different contexts, as well as the interoperability of tools proving such refinements to be correct. \THIS/  
addresses these problems by providing a standardized notation with formal semantics for such refinements. Refinements expressed in this language could, e.g., be 
parameterized and reused in different contexts.

Coming to a \THIS/ example, we want to state the fact that the state
machine of the \uml{atm}, shown in Fig.~\ref{fig:state-machine}, is a
refinement of the protocol state machine in Fig.~\ref{fig:psm} as
follows in \THIS/.  We continue the library \uml{ATM} above, again
assuming that XMI representations of the relevant UML models have been
stored at \url{http://www.example.org/uml/},
e.g.\ \url{http://www.example.org/uml/atm.xmi}:


The refinement uses an abstraction of the \uml{atm}, expressed by the
translation via symbol map \texttt{Idle |-> Idle, CardEntered |-> Idle, PINEntered |-> Idle, Verified |-> Idle, Verifying |-> Verifying}, resulting in a two-state machine. Moreover, some detail of the \uml{atm} is hidden using
\syntax{hide}. Then, the protocol state machine can be refined to
the thus abstracted \uml{atm}.

\section{Use Case Model-3: Coherent Semantics for Multi-Language Models}
\label{model-3}
	
Often a single problem area within a given domain must be represented using several formalisms, e.g., because of user community requirements, expressiveness or tool support 
and usage. 
Typically the different representations are written by different people using formalisms that are based on different logics. Thus, it is a challenge to maintain 
consistency across the different representations. 
The need for the use of multiple OMS languages, even within the OMG community, is also reflected by the OMG Ontology Definition Metamodel (ODM), which 
provides a number of syntactic transformations between such languages.
One example is the OMG Date-Time Vocabulary (DTV). DTV has been formulated in different languages, each of which addresses different audiences:
\begin{itemize}
\item	 SBVR: business users
\item 	UML (class diagrams and OCL): software implementers
\item 	OWL: ontology developers and users
\item 	Common Logic: (foundational) ontology developers and users
\end{itemize}
With \THIS/, one can, e.g.,
\begin{itemize}
\item 	formally relate the different formalizations used for DTV, relate the different formalizations using translations,
\item 	check consistency across the different formalizations (using suitable tools),
\item 	extract sub-modules covering specific aspects, and
\item 	specify the OWL version to be an approximation of the Common Logic version (using a heterogeneous interpretation of OMS).
\end{itemize}
Note that the last point does not specify what information is lost in the approximation. Indeed, \THIS/ provides the means to specify requirements on the approximation, e.g., that it maximally preserves the information. 

Coming to a \THIS/ example,
a model like the ATM model developed in section \ref{sec:atm-example} typically is part of an
application context that also contains some common terminology.
This terminology often is specified by an ontology, and then
it is desirable to relate the model to the ontology. Consider
the following financial ontology fragment:


When we want to relate this ontology with the ATM model, 
we need to take care of various aspects:
\begin{itemize}
  \item Translating into shared language (here, we choose Common Logic)
  \item Unifying terminology (Bank vs. FinancialIntermediary)
  \item Connecting related concepts (bank.owns.ATM vs. owns)
  \item Removing irrelevant parts (livestock) 
\end{itemize}


\section{Conclusion}

In the next sections, we discuss  the metalanguage \THIS/, its features that enable the support of a variety of formalisms, with syntax, well-defined semantics and model theory. \THIS/ 
distills best practices of modularity and metarelations (such as refinement and alignment) across the three areas of ontology design, formal 
specification, and model-driven development. It provides the ability to specify the basis for formal interoperability even among heterogeneous OMS and OMS networks. \THIS/ enables the solutions of the problems described in the use cases above. It also enables the development of OMS libraries, tools and workflows that 
allow  a better exchange and reuse of OMS. Eventually, this will also lead to better, easier developed and maintained systems based on these OMS.


\chapter{Design Overview} \label{c:design}
%
This clause is informative. Its purpose is to briefly describe the 
 overall guiding principles and constraints of \THIS/'s syntax and semantics.
%
%
%\section{DOL design}
\label{c:design:overview}
%

We give an overview of the most important and innovative language
constructs of DOL. Details can be found in clause~\ref{c:abstract-syntax}.

\section{DOL in a Nutshell}

As the usage scenarios in clause \ref{c:goal} illustrate, the use of multiple OMS may lead to lack 
 of interoperability. The goal of \THIS/ is to enable users to overcome these interoperability issues by providing a language for representing 
structured OMS and the relations between OMS as part of an OMS network in a semantically well-defined way. One particular challenge that needs to be
addressed is that OMS are written in a wide variety of OMS languages, which differ in style, 
expressivity and logical properties. 
We face this diversity not by proposing a
``universal'' language that is intended to subsume all the others, but by accepting
this pluralism in OMS languages and by formulating means (on a sound and formal semantic basis) to
 compare and integrate OMS written in different formalisms. Thus, \THIS/ is not `yet-another-modeling
language', but a meta-language that is used on top of existing OMS languages. 

The major functions of \THIS/ are the following: 
\begin{itemize}
		\item \THIS/ allows the use of OMS in other OMS languages (e.g., UML class diagrams, CASL, 
		OWL, Common Logic) without requiring any changes. These are called \emph{native OMS}.  
		\item \THIS/ provides for defining new, \emph{structured OMS} based on existing OMS.\footnote{Also native OMS can use the structuring constructs from their OMS language. However, these structuring constructs are often quite limited, and moreover, they differ from OMS language to OMS language.} \THIS/ provides a number of operations for this purpose; e.g.,
		it is possible to define a structured OMS $C$ as the union of an OWL
		ontology $A$ and a Common Logic ontology $B$.
		\item \THIS/ provides for defining connections between two OMS by using 
		\emph{OMS mappings}. \THIS/ provides a variety of mappings; e.g.,  one can align terminology 
		between different OMS or specify that some OMS is an extension of another. A set of OMS
		and OMS mappings may form together an \emph{OMS network}.
		\item Native OMS inherit their semantics from the underlying OMS languages. The \THIS/
		 operations for defining structured OMS, 
		OMS mappings, and OMS networks have a declarative model-theoretic semantics, which is 
		 defined in \cref{c:semantics}.  
\end{itemize}
 
The syntax of \THIS/ roughly follows these functions; native OMS, the various kind of structured OMS, OMS mappings, and OMS networks are the most important syntactic categories of \THIS/. 
They (together with queries and importation) form the items in a \emph{DOL library}.
 





\section{Features of DOL}\label{c:req:overview}

\THIS/ is a language enabling OMS interoperability. 
\THIS/ is
\begin{description}
\item[free] DOL is freely available for unrestricted use.
\item[generally applicable] DOL is neither restricted to OMS in a specific domain, nor to foundational OMS, nor to OMS represented in a specific OMS language, nor to OMS stored in any specific repositories.
\item[open] DOL supports mapping, integrating, and annotating OMS across arbitrary internet locations.  It makes use of existing open standards wherever suitable.  The criteria for extending DOL (see next item) are transparent and explicit.
\item[extensible] DOL provides a framework into which any existing, and, desirably, any future OMS language can be plugged.
\end{description}
\THIS/ is applicable to any OMS language that has a formal, logic-based semantics or a semantics defined by translation to another OMS language with such a formal semantics. The annotation framework of DOL is additionally applicable to the non-logical constructs of such languages. This \OMGSpec/ specifies formal criteria for establishing the conformance of an OMS language with DOL.  The annex establishes the conformance of a number of relevant OMS languages with DOL; a registry shall offer the possibility to add further (also non-standardized) languages. 

\THIS/ provides syntactic constructs for structuring OMS regardless of the logic their sentences are formalized in. 
Since \THIS/ is a meta-language,  it \textit{inherits} the logical language aspects of conforming OMS languages.  It is possible to literally include sentences expressed in such OMS languages in a \THIS/ OMS.


\THIS/ provides an initial vocabulary for expressing relations in correspondences (as part of alignments between OMS).  Additionally, it provides a means of reusing relation types defined externally of this \OMGSpec/.
\THIS/ does not provide an annotation vocabulary, i.e.\ it neither provides annotation properties nor datatypes to be used with literal annotation objects.
% Instead, an informative annex recommends existing annotation vocabularies for use with DOL.
%\CLnote[type=q-all]{We need to revise this following the agreement to drop the XML and RDF serializations.}In the interest of wide applicability and tool support, DOL  supports multiple alternative serializations.  In particular, there is a text serialization targeting human readers and writers, as well as serializations optimized for machine processability.
%The \textbf{text serialization} in particular offers a syntax for abbreviating identifiers of resources within OMS in a way that does not require authors to write down their full global identifiers.
%An OMS implemented in DOL can comprise parts formalized in any OMS language; any serialization of DOL can literally include such parts, regardless of the OMS language serialization they have been written in. \todonote[author=Christoph Lange,date=D:201109200256+02'00',type=fyi]{advanced namespacing is the solution that addresses this requirement} Additionally, an OMS implemented in DOL can refer to any external OMS formalized in any OMS language, as long as they can be identified in a globally unique way.
%Existing OMS in existing XML serializations (\eg XCL) or text serializations (\eg OWL Manchester Syntax) validate as DOL OMS with a minimum amount of syntactic adaptation. Existing OMS files/documents are usable in a DOL context without the need for modification.


%DOL does not provide a new elementary OMS language, but provides a
% layer to be used on top of existing elementary OMS languages which
% enables OMS engineers to formally express mappings between OMS written
% in different languages and stored at different Web locations. The
% purpose of such OMS networks is enabling a greater extent of
% interoperability between data and services in complex application
% settings.

%
% The following features are essential to the design of this \OMGSpec/:
%
% \begin{itemize}
% \item DOL is a language covering OMS modularity, OMS heterogeneity, and
% OMS mapping. In particular, it enables writing structured OMS
% (thereby reusing existing OMS), OMS involving different languages,
% as well as complex mappings and relations between OMS.
% \item DOL is a declarative language with a formal semantics.
% % for modular OMS that consist of structured OMS that are possibly heterogeneous, i.e.\ are written within the same or in different OMS languages, and made available at different Web locations.
% \item DOL provides a superset of the modularization, Web awareness and annotation facilities of a number of commonly used OMS languages, including OWL \cite{OWL2}, RDF \cite{RDF}, Common Logic \cite{ISO/IEC 24707:2007} and UML \cite{UML}.\footnote{See \cref{c:req:extensible} for details.}
% \item DOL is an open, extensible standard that is not restricted to a fixed set of supported OMS language but specifies criteria for any existing or future OMS language to conform with DOL.
% \item Existing OMS in languages conforming with DOL remain as they are; they can be enriched with DOL's modularity and annotation constructs in a non-disruptive way.
% \end{itemize}
%
% \ednote{reformulate this, see RFP}
%
%


\section{OMS Languages}
%DOL gives interoperability a formal grounding and makes heterogeneous OMS and OMS networks and services based on them amenable to checking of coherence (e.g. consistency, conservativity, intended consequences, and compliance).
 OMS languages are declarative languages for making ontological distinctions formally precise, for modeling a domain in an unambiguous way, or for expressing algebraic specifications of software.   OMS languages are distinguished by the following features:

\begin{description}
\item[Logic] Most commonly, OMS languages are based on a description logic or some other subset of first-order logic, but in some cases, higher-order, modal, paraconsistent and other logics are used.
\item[Modularity] A means of structuring an OMS into reusable parts, reusing parts of other OMS, mapping imported symbols to those in the importing OMS, and asserting additional properties about imported symbols.
\item[Annotation] A means of enabling the attachment of human-readable descriptions to OMS symbols, addressing knowledge engineers and service developers, but also end users of OMS-based services.
\end{description}
Whereas the first feature determines the expressivity of the language and the possibilities for automated reasoning (decidability, tractability, etc.), the latter two facilitate OMS engineering as well as the engineering of OMS-based software.

Acknowledging the wide tool support that conforming established languages such as OWL, RDF, Common Logic, UML, MOF, or CASL enjoy, existing OMS in these (and any other) conforming languages remain as they are within the DOL framework. DOL enhances their modularity and annotation facilities to a superset of the modularity and annotation facilities they provide themselves. 
Using DOL's modularity constructs to make statements about modules of existing OMS works by making relevant parts of these OMS, e.g., sets of axioms, identifiable, and then referring to these identifiers from DOL statements.  DOL's modularity constructs are semantically well-founded within a library of formal relationships between the logics underlying the different supported OMS languages.
General annotation of OMS and their parts works in a similar way.  Here, DOL does not provide its own annotation constructs, but once more DOL's general mechanism of making things of interest identifiable can be employed.  Once these things have been identified, the actual annotations can be added using external mechanisms such as RDF.
\ednote{Till, is this standoff markup remark up to date? TM: we promise standoff markup at various places, but we never are specific how this can be written in DOL.\\
CL: I have now emphasized that DOL itself doesn't do annotation but only identification, whereas annotation is left to RDF.}

\section{DOL in the Metamodeling Hierarchy}

DOL uses the metamodeling hierarchy known from model-driven engineering:

The syntax of a DOL conformant language can be written in MOF or EBNF,
which are self-describing.  The semantics of a DOL conformant language
is its presentation as an institution. Institutions themselves are
specified in the language of set theory and category
theory.\footnote{In the future, it may be possible to specify the
  semantics of a DOL conformant language using a semantics-based
  logical framework such as MMT. This would close the loop already at
  M3 also for the semantics.}

\section{Semantic Foundations of DOL}\label{sem-foundations}


A large variety of OMS languages in use can be captured at an abstract level using the concept of 
\emph{institutions}\index{institution} \cite{GoguenBurstall92}.
This allows the development of results independently of the particularities of a logical system and to use the notions of institution and  logical language interchangeably. 
%We first introduce the concept of \emph{logic syntax}.
The main idea is to collect the non-logical
symbols of the language in signatures and to assign to each signature the set of sentences that can be formed with its symbols. 
For each signature, we provide means for extracting the symbols it consists of, together with their kind.
Institutions also provide a model theory, which introduces semantics for
the language and gives a satisfaction relation between the models and
the sentences of a signature.   
% The only restriction imposed is the
% satisfaction condition, which captures the idea that truth is
% invariant under change of notation (and enlargement of context) along
% signature morphisms. This relies on two further components of
% institutions: the translation of sentences along signature morphisms,
% and the reduction of models against signature morphisms (generalizing
% the notion of model reduct known from logic).

It is also possible to complement an institution with a proof theory,
introducing a derivability relation between sentences, formalized as 
an \emph{entailment system} \cite{Meseguer89}. In particular, this
can be done for all logics that have so far been in use in \THIS/.


Since institutions allow the differences between OMS languages to be elided to common abstractions, 
the semantics of basic OMS is presented in a uniform way.  The semantics of structured OMS, 
OMS mappings, OMS networks, and other DOL expressions is defined using model-theoretic constructions
on top of institutions. 


\section{DOL Enables Expression of Logically Heterogeneous OMS and Literal Reuse of Existing OMS}
DOL is a mechanism for expressing logically heterogeneous OMS. It can be used to combine sentences and structured OMS expressed in different conforming OMS languages
and logics into single documents or modules. With DOL, sentences or structured OMS of previously existing OMS in
conforming languages can be reused by literally including them into a DOL OMS. A minimum of wrapping constructs and other annotations (e.g., for identifying the language of a sentence) are provided. 
 See the
abstract syntax category \syntax{OMS} in
clause~\ref{c:abstract-syntax}.

A heterogeneous OMS can import several OMS expressed in different
conforming logics, for which suitable translations have been defined
in the logic graph provided in \aref{a:graph} or in an extension to it
that has been provided when establishing the conformance of some other
logic with DOL.  Determining the semantics of the heterogeneous OMS
requires a translation into a common target language to be applied
(\cf \cref{c:semantics}).  This translation is determined via a lookup
in the transitive closure of the logic graph.  Depending on the
reasoners available in the given application setting, it can, however,
be necessary to employ a different translation.  Authors can express
which one to employ.  In a multi-step translation, it is possible to
implicitly apply as many default translations as possible, and to
concentrate on making explicit only those translations that deviate
from the default.

\section{DOL Includes Provisions for Expressing Mappings Between OMS}\label{c:req:links}

DOL provides a syntax for expressing mappings between OMS.  One use case illustrating both is sketched in  \fref{f:DOL-mapping}.  OMS mappings supported by DOL include:
\begin{itemize}
\item imports (particularly including imports that lead to conservative extensions), see the
abstract syntax categories \syntax{OMSRef} and \syntax{ExtensionOMS} in
clause~\ref{c:abstract-syntax}.
\item interpretations (both between OMS and OMS networks), see the
abstract syntax category \syntax{IntprDefn} in
clause~\ref{c:abstract-syntax}.
\item alignments between OMS, see the
abstract syntax category \syntax{AlignDefn} in
clause~\ref{c:abstract-syntax}.
\item mappings between OMS and their modules, see the
abstract syntax category \syntax{ModuleRelDefn} in
clause~\ref{c:abstract-syntax}.
\end{itemize}
DOL uses symbol maps to express signature translations in such OMS mappings; see the
abstract syntax category \syntax{SymbolMapItems} in
clause~\ref{c:abstract-syntax}.

DOL need not be able to fully represent logical translations but is
capable of referring to them.

DOL can also be used to combine or merge OMS along such OMS mappings, see
the rule for \syntax{combination} for the abstract syntax category
\syntax{OMS} in clause~\ref{c:abstract-syntax}.




\section{DOL Provides a Mechanism for Rich Annotation and Documentation of OMS}\label{c:req:annotation}

DOL provides a mechanism for identifying anything of relevance in OMS by assigning an IRI to it.  With RDF there is a standard mechanism for annotating things identified by IRIs.  Thus, DOL supports  annotations in the full generality specified in \cref{c:terms-annotation}.

%A list of recommended RDF vocabularies for annotating OMS is presented in annex \ref{a:lola}.

\clause{DOL Abstract Syntax}\label{c:abstract-syntax}

\sclause{Abstract Syntax Categories}

DOL provides abstract syntax categories for
\begin{itemize}
\item \red{OMS} (which can be native OMS in some OMS language, or unions, translations, minimizations, combinations, approximations of OMS, among others)
\item OMS mappings 
\item OMS networks
\item \red{queries}
\item libraries (items in libraries are: definitions of OMS, OMS mappings, OMS networks and queries, as well as qualifications choosing the logic,
OMS language and/or serialization)
\item identifiers
\item annotations
\end{itemize}
 
Additionally, the categories of the abstract syntaxes of any conforming OMS languages (\cf \cref{c:conform:logic}) are also DOL abstract syntax categories.

The following subclauses, one per abstract syntax category, specify the abstract syntax of DOL in EBNF. Note that we deviate from the EBNF specification in
 \nisref{ISO/IEC 14977:1996} in favor of a more modern and concise
EBNF syntax.\footnote{\red{More precisely, \nisref{ISO/IEC 14977:1996} requires commas between the (non-)terminals of a right-hand side, which we omit 
for the sake of better readability. Also, we replace the separator \syntax{=}
between left and right hand-side of a rule with \syntax{::=}, and 
use the notation \syntax{N+}
for one or more repetitions of \syntax{N}.}}  
%Note that ISO EBNF lacks an operator for ``at least one repetition''.  This \OMGSpec/ therefore adopts the following convention: Whenever some sequence \syntax{S} is repeated at least once, we give it a non-terminal identifier of its own (\syntax{RepeatedS = S \{ S \} ;}), or group it as in \syntax{LongerExpression = Foo Bar ( S \{ S \} ) ;}.

\sclause{Libraries}\label{c:libraries}

A \termref{library} (\syntax{Library}) consists of a collection of (named)  OMS and mappings between these.  More specifically, a
library consists of a name, followed by a list of
\syntax{LibraryItem}s.  A \syntax{LibraryItem} is either a
definition of an OMS  (\syntax{OMSDefn}), 
a mapping between OMS
(\syntax{MappingDefn}), 
\red{a definition of an OMS network  (\syntax{NetworkDefn}),}
a definition related to queries 
(\syntax{QueryRelatedDefn})
or a \syntax{Qualification} selecting a specific
OMS language, logic and/or syntax that is used to interpret the
subsequent \syntax{LibraryItem}s.  Alternatively, a library can also be the verbatim inclusion of an OMS written in
an OMS language that conforms with DOL (\syntax{NativeOMS}; \cf \ref{c:conform:logic}).

\begin{lstlisting}[language=ebnf,escapeinside={()}]  % abstract syntax

Library                  = [ PrefixMap ] , LibraryDefn
                         | NativeOMS ;
LibraryDefn              = 'library' , LibraryName , Qualification , { LibraryItem } ;
NativeOMS  = ($<$)language specific($>$) ;
LibraryItem              = LibImport | OMSDefn | NetworkDefn | MappingDefn | QueryRelatedDefn | Qualification ;
LibImport                = 'lib-import' , LibraryName ;
Qualification            = LanguageQual | LogicQual | SyntaxQual ;
LanguageQual             = 'lang-select' , LanguageRef ;
LogicQual                = 'logic-select' , LogicRef ;
SyntaxQual               = 'syntax-select' , SyntaxRef ;
LibraryName              = IRI ;

PrefixMap        = 'prefix-map' , { PrefixBinding } ;
PrefixBinding    = 'prefix-binding' , BoundPrefix , IRIBoundToPrefix ,
                   [ Separators ] ;
BoundPrefix      = 'bound-prefix' , [ Prefix ] ;
IRIBoundToPrefix = 'full-iri' , FullIRI ;
Separators       = 'separators' , LibraryOMSSeparator , OMSSymbolSeparator ;
LibraryOMSSeparator = SeparatorString ;
OMSSymbolSeparator  = SeparatorString ;
SeparatorString  = SeparatorChar , { SeparatorChar } ;
SeparatorChar    = ipchar | gen-delims , - , '#' ;
                   ($<$ \rm as defined in \nisref{IETF/RFC 3987} $>$)
\end{lstlisting}
%% ~\todonote[type=fyi,author=Christoph Lange]{Things changed from HetCASL:\textLF
%%   • logic-select now mandatory (no default logic) and tree-scoped MC: what does this mean? To make Hets-lib conform with this, we should have .het files equivalent to .dol files with logic selected to be CASL\textLF
%%   • download-items (encourage linked data best practices instead)\textLF
%%   • item-name-map (to be replaced by namespaces??)\textLF
%%   • lib-version (to be replaced by metadata annotations, \eg OMV)\textLF
%%   • indirect-mapping (will always use full IRIs, and abbreviate them by syntactic namespaces)}

At the beginning of a library, one can declare a \syntax{PrefixMap} for abbreviating long IRIs; see \cref{c:identifiers} for further details.

\sclause{OMS Networks}\label{c:networks}
\red{
Inside a library, one can define OMS networks (\syntax{NetworkDefn}).
A \syntax{NetworkDefn} names an
OMS network consisting of  OMS and OMS mappings. OMS networks may build on previously-defined
OMS networks, and they can be used in \syntax{combination}s.  
}
\begin{lstlisting}[language=ebnf,escapeinside={()}]  % abstract syntax

NetworkDefn            = 'network-defn', NetworkName , [ ConsStrength ] , Network ;
NetworkName            = IRI ;
Network                = 'network', NetworkElements , ExcludeExtensions ;
NetworkElements        = 'network-elements' , { NetworkElement } ;
NetworkElement         = 'network-element' , [ Id ] , OMSOrMappingorNetworkRef ;
ExcludeExtensions    = 'exclude-imports' , { ElementRef } ; 
ElementRef   = 'path', OMSOrMappingorNetworkRef, OMSOrMappingorNetworkRef 
               | OMSOrMappingorNetworkRef ;
OMSOrMappingorNetworkRef  = IRI ;
\end{lstlisting}

An OMS network by default also includes all inclusions (generated by
\syntax{ExtensionOMS}) between the involved OMS---unless these are
explicitly excluded.

\sclause{OMS}\label{c:focused-OMS}

An OMS (\syntax{OMS}) can be one of the following:
\begin{itemize}
\item a basic OMS \syntax{BasicOMS} written inline, in a conforming serialization of a conforming OMS 
language (which is defined outside this standard)\footnote{In this place, any OMS in a conforming serialization of a conforming OMS language is permitted.  
However, DOL's module sublanguage should be given preference over the module sublanguage of 
the respective conforming OMS language; \eg DOL's extension construct should be preferred over OWL's import construct.},
\item a translation of an OMS into a different signature or OMS
language,
\item a reduction of an OMS to a smaller signature and/or less
expressive logic (that is,
some non-logical symbols are hidden, but the semantic effect of sentences involving these is kept),
\item a module extracted from an OMS, using a restriction signature,
\item an approximation of an OMS, in a subsignature or sublogic, with the effect that sentences not expressible in the subsignature resp.\ sublogic are replaced with a suitable approximation,
\item \red{a filtering of an OMS, with the effect that some signature symbols and axioms are removed from the OMS,}
\item an extension of an OMS with a basic or a minimizable OMS, optionally named and/or marked as conservative, monomorphic, definitional, weakly definitional or implied,
\item a union of several OMS (the major difference between a union and extension is that the members of the unions need to be self-contained OMS, while the extensions may reuse the signature of the extended OMS), 
\item a reference to an OMS existing on the Web,
\item an OMS qualified with the OMS language that is used to express it,
\item a combination of an OMS network (technically, this is a colimit, see \cite{ZimmermanEtAl06}),
\item a minimization of an OMS, forcing the subsequently declared
  non-logical symbols to be interpreted in a minimal way, while the non-logical symbols declared so far are fixed (alternatively, the non-logical symbols to be minimized and to be varied can be explicitly declared). \red{Variants are
maximization, freeness (minimizing also data sets and equalities on these), and cofreeness
(maximizing also data sets and equalities on these),}
\item \red{the application of a substitution to an OMS.}


\end{itemize}
% derived from CASL (see CASL reference manual)
% and HetCASL (see HetCASL summary)

\begin{lstlisting}[language=ebnf,escapeinside={()}]  % abstract syntax

BasicOMS = ($<$)language specific($>$) ;
MinimizableOMS       = BasicOMS
                     | 'oms-ref' , OMSRef , [ ImportName ] ;
ExtendingOMS         = MinimizableOMS
                     | MinType , MinimizableOMS ;
OMS                  = ExtendingOMS
                     | 'minimize-symbols' , OMS , Minimization
                     | 'translation' , OMS , Translation
                     | 'reduction' , OMS , Reduction
                     | 'module-extract' , OMS , Extraction 
                     | 'approximation' , OMS , Approximation
                     | 'filtering', OMS, Filtering
                     | 'union' , OMS , [ ConsStrength ] , OMS 
                     | 'extension' , OMS , ExtensionOMS 
                     | 'qual-oms' , { Qualification } , OMS
                     | 'combination' , Network
                     | 'application', OMS, SubstName ;

Minimization         = MinType, CircMin , CircVars ;
MinType              = 'minimize' | 'maximize' | 'free' | 'cofree' ;
CircMin              = Symbol , { Symbol } ;
CircVars             = { Symbol } ;

Translation          = 'renaming' , { LogicTranslation } , [ SymbolMapItems ] ;
LogicTranslation     = 'logic-translation' , OMSLangTrans ;

Reduction            = 'hidden' , { LogicReduction } , [ SymbolItems ]
                     | 'revealed' , SymbolItems  ;
LogicReduction       = 'logic-reduction' , OMSLangTrans ;

SymbolItems          = 'symbol-items' , Symbol , { Symbol } ;
SymbolMapItems       = 'symbol-map-items' , SymbolOrMap , { SymbolOrMap } ;

Extraction           = 'extraction', QualInterfaceSignature ;

Approximation        = 'approx' , [ QualInterfaceSignature ] , [ LogicRef ] ;

Filtering            = 'select' , BasicOMS 
                     | 'reject' , BasicOMS ;

ExtensionOMS         = extension-oms , [ ExtConsStrength ] , [ ExtensionName ] , 
                                       ExtendingOMS ;

ConsStrength         = Conservative 
		     | 'monomorphic'  
		     | 'weak-definitional' 
		     | 'definitional' ;

ExtConsStrength      = ConsStrength | 'implied' ;

Conservative         = 'consequence-conservative' | 'model-conservative' 
                     | 'not-consequence-conservative' | 'not-model-conservative' ;

QualInterfaceSignature   = 'keep-signature' , InterfaceSignature 
                         | 'remove-signature' , InterfaceSignature ;

InterfaceSignature   = SymbolItems ;
ImportName           = IRI ;
ExtensionName        = IRI ;
\end{lstlisting}
%% \ednote{Alternatively, we could use one type of \syntax{InterfaceSignature}
%% only, and instead use different constructors for \syntax{Extraction}
%% and \syntax{Approximation}. This would be a bit more verbose, but a bit
%% more coherent with position of non-terminals in the concrete syntax.}

An OMS definition \syntax{OMSDefn} names an  OMS.  

It can be
optionally marked as inconsistent, consistent, monomorphic or having a unique model using 
\syntax{ConsStrength}.\footnote{More precisely, \syntax{'consequence-conservative'}
here requires the OMS to have only tautologies as signature-free logical consequences, while \syntax{'not-consequence-conservative'} expresses that this is not the case. 
\syntax{'model-conservative'}
requires satisfiability of the OMS, \syntax{'not-model-conservative'} its
unsatisfiability.
\syntax{'definitional'} expresses the unique model property; this may be interesting for characterizing
OMS (e.g.\ returned by model finders) that are used to describe single models.}. An
\syntax{SymbolItems}, used in an OMS \syntax{Reduction}, is a
list of non-logical symbols that are to be hidden. A \syntax{LogicReduction}
denotes a logic reduction to a
less expressive OMS language. A \syntax{SymbolMapItems}, used in
OMS \syntax{Translation}s,  maps symbols to symbols,
%% \CLnote[type=fyi]{On 2012-07-18 we decided 
%% not to specify lambda-style symbol-to-term mappings for now.  Would be convenient, but specifying its semantics 
%% in an OMS language independent way would require additional institution infrastructure – and the same effect can be 
%% achieved by auxiliary definitional extensions, cf.\ Colore (so promote this, informatively, as a ``best practice''?) TM: Alternatively, we could use a recent notion of institutional monad. This builds an extended signature with all terms. Then one can use ordinary signature morphisms into such extended signatures.} 
%or a logic
%translation. 
An OMS language translation \syntax{OMSLangTrans} 
can be either specified by its name, or be inferred as the \termref{default
translation} to a given target (the source will be inferred as the 
OMS language of the current OMS).

\begin{lstlisting}[language=ebnf,escapeinside={()}]  % abstract syntax

OMSDefn          = 'oms-defn' , OMSName , [ ConsStrength ] , OMS ;
Symbol           = IRI ;
SymbolMap        = 'symbol-map' , Symbol , Symbol ;
SymbolOrMap      = Symbol | SymbolMap ;
Term             = ($<$)an expression specific to an OMS language($>$) ;
Sentence         = ($<$)an expression specific to an OMS language($>$) ;
                 
OMSName          = IRI ;
                 
OMSRef           = IRI ;
ExtensionRef     = IRI ;
                 
LoLaRef          = LanguageRef | LogicRef ;
                 
LanguageRef      = IRI ;
LogicRef         = IRI ;
SyntaxRef        = IRI ;
                 
OMSLangTrans     = 'named-trans' , OMSLangTransRef
                 | 'default-trans' , LoLaRef ; 
                 
OMSLangTransRef  = IRI ;
                 
\end{lstlisting}


\sclause{OMS Mappings}\label{c:oms-mappings}

An OMS mapping provides a connection between two OMS. An OMS mapping definition is the definition of 
either a named interpretation (\syntax{IntprDefn}, \red{\syntax{Entailment}} or 
\syntax{EquivDefn}), a named declaration of the  relation between a module of an OMS and the whole 
OMS (\syntax{ModuleRelDefn}), or a named \termref{alignment} (\syntax{AlignDefn}).

The \syntax{SymbolMapItems} in an interpretation always must lead to a signature morphism; a proof 
obligation expressing that the (translated) source OMS logically follows from the target OMS is 
generated.  \red{An entailment is a variant where all symbols are mapped identically, while an 
equivalence states that the model classes of two OMS are in bijective correspondence.}

\red{
Interpretations, entailments and equivalences between OMS networks are also possible. An 
interpretation between OMS networks has to specify both a mapping between the nodes of the OMS 
network, as well as, for each node, a symbol map from the OMS of that node to the target OMS to 
which it is mapped.
%\ednote{In equivalences between OMS networks, should we allow for node mappings 
%as well? In  \cite{MossakowskiTarlecki09}, this is allowed.
%--- No, since we do not allow for signature morphisms either.}
}

In contrast to this functional style of mapping symbols, an alignment provides a relational 
connection between two OMS,  using a set of \syntax{Correspondence}s. Each correspondence may relate 
some OMS non-logical symbol to another one (possibly given by a term) with an optional confidence 
value. Moreover, the relation between the two non-logical symbols can be explicitly
specified (like being equal, or only being subsumed) in a similar way to the Alignment API \cite{AlignmentAPI}. 
\red{The relations that can be used in a correspondence are equivalence, disjointness, subsumption, membership (the last two with a
variant for each direction) or a user-defined relation that is stored in a registry and must be prefixed with
\url{http://www.omg.org/spec/DOL/correspondences/}.
A default correspondence can be used; it is applied to all pairs of non-logical symbols with 
the same local names. The default relation in a correspondence is equivalence, unless  a different 
relation is specified in a surrounding 
'CorrespondenceBlock'.
Using an \syntax{AlignCard}, left and right injectivity and totality of the
\termref{alignment} can be specified (the default is left-injective, right-injective, left-total  and right-total).
With \syntax{AlignSem}, different styles of networks of aligned ontologies (to be interpreted in 
a logic-specific way) of alignments can be specified: whether a single domain is assumed, all domains are embedded into a global domain,
or whether several local domains are linked (``contextualized'') by relations.}

A \syntax{ModuleRelDefn} declares that a certain OMS
actually is a module of some other OMS with respect
to the \syntax{InterfaceSignature}.


\begin{lstlisting}[language=ebnf,escapeinside={<>},mathescape]  % abstract syntax

MappingDefn          = IntprDefn | Entailment | EquivDefn | ModuleRelDefn | AlignDefn;

IntprDefn            = 'intpr-defn' , IntprName , [ Conservative ] , 
                        IntprType , { LogicTranslation } , [ SymbolMapItems ]                     
                     | 'refinement' , IntprName , Refinement ;
IntprName            = IRI ;
IntprType            = 'intpr-type' , OMS , OMS ;

Refinement           = 'ref-oms' , OMS 
                     | 'ref-network' , Network
                     | 'ref-composition' , Refinement , Refinement
                     | 'simple-oms-ref' , OMS , RefMap , Refinement 
                     | 'simple-network-ref' , Network , RefMap , Refinement ;
RefMap               = 'refmap-oms' , [ LogicTranslation ] , [ SymbolMapItems ] 
                     | 'refmap-network' , { NodeMap } ;
NodeMap              = 'node-map', OMSName , OMSName , 
                                   { LogicTranslation } , [ SymbolMapItems ] ;


Entailment           = 'entailment' , EntailmentName , EntailmentType ;
EntailmentType       = 'oms-oms-entailment', OMS , OMS 
                     | 'network-oms-entailment', Network , OMSName , OMS 
                     | 'network-network-entailment', Network, Network ;
EntailmentName       = IRI ;

EquivDefn            = 'equiv-defn' , EquivName , EquivType ;
EquivName            = IRI ;
EquivType            = 'oms-equiv' , OMS , OMS , OMS
                     | 'network-equiv' , Network , Network , Network ;

ModuleRelDefn        = 'module-defn' , ModuleName , [ Conservative ] , ModuleType ,
                                       InterfaceSignature ;
ModuleName           = IRI ;
ModuleType           = 'module-type' , OMS , OMS ;

AlignDefn            = 'align-defn' , AlignName , [ AlignCard ] , AlignType, 
                                    AlignSem,   { Correspondence } ; <\footnote{Note that this grammar uses ``type'' as in ``the type of a function'', whereas the Alignment API uses ``type'' for
	 the totality/injectivity of the relation/function.  For the latter, this grammar uses ``cardinality''.}>
AlignName            = IRI ;
AlignCards           = AlignCardForward , AlignCardBackward ; 
AlignCardForward     = 'align-card-forward' , AlignCard ;
AlignCardBackward    = 'align-card-backward' , AlignCard ;
AlignCard            = 'injective-and-total'
                     | 'injective'
                     | 'total'
                     | 'neither-injective-nor-total' ;
AlignType            = 'align-type' , OMS , OMS ;
AlignSem            = 'single-domain' 
                    | 'global-domain' 
                    | 'contextualized-domain' ; 

Correspondence       = CorrespondenceBlock
                     | SingleCorrespondence
                     | 'default-correspondence' ; 

CorrespondenceBlock  = 'correspondence-block' , [ RelationRef ] , [ Confidence ],
                                                Correspondence, { Correspondence } ; 
SingleCorrespondence = 'correspondence' , SymbolRef , [ RelationRef ] , [ Confidence ] ,
                                          TermOrSymbolRef , [ CorrespondenceID ] ;
CorrespondenceID     = IRI ;
SymbolRef            = IRI ;
TermOrSymbolRef      = Term | SymbolRef ;
RelationRef          = 'subsumes' | 'is-subsumed' | 'equivalent' | 'incompatible' 
                     | 'has-instance' | 'instance-of' | 'default-relation' | IRI ; 
Confidence           = Double ;
\end{lstlisting}
\begin{lstlisting}[language=ebnf,escapeinside={()},mathescape]  % abstract syntax

Double               = ($<$ a number $\in [0,1]$ $>$) ;
\end{lstlisting}

A symbol map in an interpretation is \required to cover all non-logical symbols of the source OMS; 
the semantics specification in \cref{c:semantics} makes this assumption\footnote{Mapping a 
non-logical symbol twice is an error. Mapping two source non-logical symbols to the same target 
non-logical symbol is legal, this then is a non-injective OMS mapping.}. 

%Alignments 

\sclause{Queries}
\red{
Queries are a means to extract information from an OMS.  DOL's \syntax{QueryDefn}s cover 
``select''-type queries that deliver an answer substitution for the query variables. (Answer) 
substitutions can be stored separately, using a \syntax{SubstDefn}. A
\syntax{ResultDefn} expresses that certain answer substitutions are
the result of a query. Optionally, a result can be expressed to be
complete, meaning that it comprises all answer substitutions to the query.
}
\begin{lstlisting}[language=ebnf,escapeinside={<>},mathescape]  % abstract syntax

QueryRelatedDefn     = QueryDefn | SubstDefn | ResultDefn ;
QueryDefn            = 'select-query-defn', QueryName, Vars, Sentence, 
                                            OMS, [OMSLangTrans] ;
SubstDefn            = 'subst-defn', SubstName, OMS, OMS, SymbolMap ;
ResultDefn           = 'result-def', ResultName, SubstName, { SubstName }, 
                                     QueryName, [ Complete ] ;
QueryName            = IRI ;
SubstName            = IRI ;
ResultName           = IRI ;
Vars                 = { Symbol } ;
Complete             = 'complete' ;
\end{lstlisting}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%~\CLnote{some text that was left over here, but I don't recall what we meant by it: recommendations for dealing with OMS language dialects}

\sclause{Identifiers}\label{c:identifiers}

This section specifies the abstract syntax of identifiers of DOL OMS and their elements.

\ssclause{IRIs}\label{c:iris}

In accordance with best practices for publishing OMS on the Web, identifiers of OMS and their 
elements \should not just serve as \emph{names}, but also as \emph{locators}, which, when 
dereferenced, give access to a concrete representation of an OMS or one of its elements.  (For the 
specific case of RDF Schema and OWL OMS, these best practices are documented in 
\cite{W3C:NOTE-swbp-vocab-pub-20080828}.  The latter is a specialization of the linked data 
principles, which apply to any machine-processable data published on the Web 
\cite{BernersLee:LinkedData2006}.)  It is recommended that publicly accessible DOL OMS be published 
as linked data.

%\todonote[type=q-aut,author=Christoph Lange]{Does this motivation/justification sound reasonable to 
%you? --- Yes.}
Therefore, in order to impose fewer conformance requirements on applications, DOL requires the use of
 IRIs for identification per \nisref{IETF/RFC 3987:2005}.
  It is \recommended that libraries use 
IRIs that translate to URLs when applying the algorithm for mapping IRIs to URIs specified in 
\nisref{IETF/RFC 3987:2005, Section 3.1}.  DOL descriptions of any element of a library that is 
identified by a certain IRI \should be \emph{located} at the corresponding URL, so that agents can 
locate them.  As IRIs are specified with a concrete syntax only in \nisref{IETF/RFC 3987:2005}, DOL 
adopts the latter into its abstract syntax as well as all of its concrete syntaxes 
(serializations).
%\CLnote[type=q-all]{I meant to say: for IRIs, the abstract syntax is the same as 
%the concrete syntax.}.

%% We don't do "semantic namespaces" for now.  (Agreed in 2012-02-23 meeting)
% For identification, DOL preferably employs IRIs that have the following three components:\footnote{This IRI syntax has originally been designed by Florian Rabe and Michael Kohlhase \cite{Rabe:MMT2011}, independently from this \OMGSpec/.\todonote[type=todo,author=Christoph Lange]{if we leave this reference in place, we might additionally refer to the paper that describes the semantics of MMT and provides more design rationale background}}

% \begin{description}
% \item[namespace] an IRI that identifies the complete OMS
% \item[module] a name that identifies a module within an OMS
% \item[symbol] a name that identifies a non-logical symbol, named import, or sentence within a module\todonote[type=todo,author=Christoph Lange]{list the other things we would like to identify in this component}
% \end{description}
% It is recommended that these ``DOL IRIs'' be used whenever an OMS or a module of an OMS is primarily implemented in DOL.

In accordance with semantic web best practices such as the OWL Manchester Syntax 
\cite{W3C:NOTE-owl2-manchester-syntax-20091027}, this \OMGSpec/ does not allow relative IRIs, and does 
not offer a mechanism for defining a base IRI, against which relative IRIs could be resolved.

Concerning these languages, note that they allow arbitrary IRIs in principle, but in practice they 
strongly recommend using IRIs consisting of two components \cite{W3C:NOTE-swbp-vocab-pub-20080828}:
\begin{description}
\item[namespace] an IRI that identifies an OMS,\footnote{See annex~\ref{a:loc/id} for a specific linked-data compliant URL scheme for DOL.}
usually ending with \syntax{\#} or \syntax{/}
\item[local name] a name that identifies a non-logical symbol within an OMS
\end{description}

\begin{lstlisting}[language=ebnf,escapeinside={()}]  % abstract syntax

IRI     = 'full-iri' , FullIRI | 'curie' , CURIE ; (\footnote{specified below in \cref{c:curies}}) 
FullIRI = ($<$ as defined by the IRI production in \nisref{IETF/RFC 3987:2005} $>$) ;
\end{lstlisting}

\ssclause{Abbreviating IRIs using CURIEs}\label{c:curies}

As IRIs tend to be long, and as syntactic mechanisms for abbreviating them have been standardized, 
it is \recommended that applications employ such mechanisms and support expanding abbreviatory
notations into full IRIs.  For specifying the \emph{semantics} of DOL, this \OMGSpec/ assumes full IRIs 
everywhere, but the DOL abstract \emph{syntax} adopts CURIEs (compact URI expressions) as an 
abbreviation mechanism, as it is the most flexible one that has been standardized to date.  

The CURIE abbreviation mechanism works by binding prefixes to IRIs.  A CURIE consists of a 
\emph{prefix}, which may be empty, and a \emph{reference}.  If there is an in-scope binding for the 
prefix, the CURIE is valid and expands into a full IRI, which is created by concatenating the IRI 
bound to the prefix and the reference.

DOL adopts the CURIE specification of RDFa Core 1.1 \nisref{W3C/TR REC-rdfa-core:2013, Section 6} with the following changes:
\begin{itemize}
\item DOL does not support the declaration of a ``default prefix'' mapping %\CLnote[type=q-aut]{Are such explanatory notes OK here? --- Yes}
(covering CURIEs such as \syntax{:name}).
\item DOL does support the declaration  of a ``no prefix'' mapping (covering CURIEs such as 
\syntax{name}). \red{If there is no explicit declaration for the ``no prefix'', it defaults to a 
context-sensitive expansion mechanism, which always prepends the library IRI (in the context of a 
structured OMS where named OMS are referenced) resp.\ the current OMS IRI (in the context of a basic
OMS) to a symbol name. Both the separator between the library and the OMS name and that between the 
OMS name and the symbol name can be declared (using the keyword \syntax{separators}), and both default to ``//''.}

\item DOL does not make use of the \syntax{safe\_curie} production.
\item DOL does not allow binding a relative IRI to a prefix.
\item Concrete syntaxes of DOL are encouraged but \notrequired to support CURIEs.\footnote{This is 
a concession to having an RDF-based concrete syntax among the normative concrete syntaxes.  RDFa is 
the only standardized RDF serialization to support CURIEs so far.  Other serializations, such as 
RDF/XML or Turtle, support a subset of the CURIE syntax, whereas some machine-oriented 
serializations, including N-Triples, only support full IRIs.}
\end{itemize}

CURIEs can occur in any place where IRIs are allowed, as stated in \cref{c:iris}.  Informatively, 
we can restate the CURIE grammar supported by DOL as follows:
\begin{lstlisting}[language=ebnf,escapeinside={()}]
CURIE     = MaybeEmptyCURIE , - ;
MaybeEmptyCURIE = [ Prefix ] , RefWithoutComma ;
RefWithoutComma = Reference , - , StringWithComma ;
StringWithComma = { UChar } , ',' , { UChar } ;
UChar     = ($<$ any Unicode \nisref{ISO/IEC 10646} character $>$) ;
Prefix    = NCName , ':' ; ($<$ \rm see ``NCName'' in \nisref{W3C/TR REC-xml-names:2009}, Section 3 $>$)
Reference = Path , [ Query ] , [ Fragment ] ;
Path      = ipath-absolute | ipath-rootless | ipath-empty ;
            ($<$ \rm as defined in \nisref{IETF/RFC 3987} $>$)
Query     = '?' , iquery ; ($<$ \rm as defined in \nisref{IETF/RFC 3987} $>$)
Fragment  = '#' , ifragment ; ($<$ \rm as defined in \nisref{IETF/RFC 3987} $>$) 
\end{lstlisting}
%\ednote{This is concrete syntax. Shouldn't it be moved to chapter \ref{{a:text-syntax}}? --- I have copied it there, altough this is code
%duplication.}

Note that outside the context of a basic OMS the prefix/reference separator of a CURIE is always the colon (\syntax{:}); only for serializations of OMS languages other than DOL it may be redefined as stated in \cref{c:conform:serialization}.

Prefix mappings can be defined at the beginning of a library (specified in \cref{c:libraries}; 
these apply to all parts of the library, including basic OMS as clarified in \cref{c:map-ids}).  
%Their syntax is:

Bindings in a prefix map are evaluated from left to right.  Authors \shouldnot bind the same prefix twice, but if they do, the later binding wins.

\ssclause{Mapping identifiers in basic OMS to IRIs}\label{c:map-ids}

While DOL uses IRIs as identifiers throughout, OMS languages do not necessarily do; for example:
\begin{itemize}
\item OWL \nisref{W3C/TR REC-owl2-syntax:2009, Section 5.5} does use IRIs.
\item Common Logic \nisref{ISO/IEC 24707:2007} supports them but does not enforce their use.
\item F-logic \cite{flogic} does not use them at all.
\end{itemize}
However, DOL OMS mappings as well as 
%\CLnote[type=todo]{maybe clarify which ones, by checking the grammar for all occurrences of SymbolRef}
certain operations on OMS require making unambiguous references to non-logical symbols of basic OMS (\syntax{SymbolRef}).  Therefore, DOL provides a function that maps global identifiers used within basic OMS to IRIs.  This mapping affects all non-logical symbol identifiers (such as class names in an OWL ontology), but not locally-scoped identifiers such as bound variables in Common Logic ontologies.  DOL reuses the CURIE mechanism for abbreviating IRIs for this purpose (\cf \cref{c:curies}).

The IRI of a non-logical symbol identifier in a basic OMS $O$ is determined by the following function:
\begin{algorithmic}
  \REQUIRE $D$ is a library
  \REQUIRE $O$ is a basic OMS in serialization $S$
  \REQUIRE $\mathit{id}$ is the identifier in question, identifying a symbol in $O$ according to the specification of $S$
  \ENSURE $i$ is an IRI
  \IF{$\mathit{id}$ represents a full IRI according to the specification of $S$}
    \STATE $i\leftarrow\mathit{id}$
  \ELSE
    \STATE \COMMENT{first construct a pattern $\mathit{cp}$ for CURIEs in $S$, then match $\mathit{id}$ against that pattern}
    \IF{the declaration of DOL-conformance of $S$ redefines the prefix/reference separator character $\mathit{cs}$ (cf.\ \cref{c:conform:serialization})}
      \STATE $\mathit{sep}\leftarrow \mathit{cs}$
    \ELSIF{$S$ forbids prefixed CURIEs}
      \STATE $\mathit{sep}\leftarrow\text{undefined}$
    \ELSE
      \STATE $\mathit{sep}\leftarrow\mathit{:}$ \COMMENT{the standard CURIE separator character}
    \ENDIF
    \STATE \COMMENT{The following statements construct a modified EBNF grammar of CURIEs; see \nisref{ISO/IEC 14977:1996} for EBNF, and \cref{c:curies} for the original grammar of CURIEs.}
    \IF{$\mathit{sep}$ is defined}
      \STATE $\mathit{cp}\leftarrow [ \mathit{NCName}, \mathit{sep} ] , \mathit{Reference}$
    \ELSE
      \STATE $\mathit{cp}\leftarrow \mathit{Reference}$
    \ENDIF 
    \IF{$\mathit{id}$ matches the pattern $\mathit{cp}$, where $\mathit{ref}$ matches $\mathit{Reference}$}
      \IF{the match succeeded with a non-empty $\mathit{NCName}$ $\mathit{pn}$}
        \STATE $p\leftarrow\mathit{concat}(pn, \mathit{:})$
      \ELSE
        \STATE $p\leftarrow\text{no prefix}$
      \ENDIF
      \IF{$O$ binds $p$ to an IRI $\mathit{pi}$ according to the specification of $S$}
        \STATE $\mathit{nsi}\leftarrow\mathit{pi}$
      \ELSE
        \STATE $P \leftarrow$ the innermost prefix map in $D$, starting from the place of $O$ inside $D$, and going up the abstract syntax tree towards the root of $D$
        \WHILE{$P$ is defined}
          \IF{$P$ binds $p$ to an IRI $\mathit{pi}$}
            \STATE $\mathit{nsi}\leftarrow\mathit{pi}$
            \STATE \textbf{break} out of the \textbf{while} loop 
          \ENDIF
          \STATE $P \leftarrow$ the next prefix map in $D$, starting from the place of the current $P$ inside $D$, and going up the abstract syntax tree towards the root of $D$
        \ENDWHILE
        \RETURN an error
      \ENDIF
      \STATE $i\leftarrow\mathit{concat}(\mathit{nsi}, \mathit{ref})$
    \ELSE
      \RETURN an error
    \ENDIF
  \ENDIF
  \RETURN $i$
\end{algorithmic}

This mechanism applies to basic OMS given inline in a library document (\syntax{BasicOMS}), not to OMS in external documents (\syntax{NativeOMS}); the latter \shall be self-contained.

While CURIEs used for identifying parts of a library (\cf \cref{c:curies}) are merely syntactic 
sugar, the prefix map for a basic OMS is essential to determining the semantics of the basic OMS 
within the library.  Therefore, any DOL serialization \shall provide constructs for expressing such 
prefix maps, even if the serialization does not support prefix maps otherwise.

%% ~\todonote[author=Christoph Lange,date=D:201111081514+01'00',type=todo]{somewhere we need to mention semantic annotations to embedded fragments in conforming OMS languages, \eg \%implied}



%% \sclause{Annotations}\label{s:annotations}

%% \todonote{this subclause will be moved to annex M}
%% ~\todonote[author=Christoph Lange,date=D:201108061340+02'00',type=todo]{Properly integrate this text from our LaRC 2011 paper} Annotations always have a subject, which is identified by an IRI. Where the given OMS language does not provide a way of assigning IRIs to a desired subject of an annotation (\eg if one wants to annotate an import in OWL), a library may employ RDF annotations that use XPointer or \nisref{IETF/RFC 5147} as a means of non-destructively referencing pieces of XML or text by URI.\footnote{We intend to utilize the extensibility of the XPointer framework by developing additional XPointer schemes, \eg for pointing to subterms of Common Logic sentences.}


\clause{DOL Text Serialization}\label{a:text-syntax}

\sclause{Document Type}

\begin{description}
\item[MIME type] \mimetype{application/dol+text}
\item[Filename extension] .dol
\end{description}

\sclause{Concrete Syntax}\label{a:dol-text:concrete}

At several places, the concrete syntax uses the non-terminal
\syntax{'end'} to mark the end of a definition or declaration. Tools
may make this \syntax{'end'} optional. However, in this standard,
we insist on the \syntax{'end'}, because it may be needed to effectively
disambiguate heterogeneous texts.

 
\ssclause{Libraries}

\begin{lstlisting}[language=ebnf,escapeinside={()},morecomment={[l]{\%\%\ }}]
Library                 = [ PrefixMap ] , LibraryDefn
                         | NativeOMS ;
LibraryDefn             = 'library' , LibraryName , Qualification , { LibraryItem } ;
NativeOMS = ($<$) language and serialization specific ($>$) ;
LibraryItem             = LibImport | OMSDefn | NetworkDefn | MappingDefn 
                          | QueryRelatedDefn | Qualification ;
LibImport                = 'import' , LibraryName ;
Qualification            = LanguageQual | LogicQual | SyntaxQual ;
LanguageQual             = 'language' , LanguageRef ;
LogicQual                = 'logic' , LogicRef ;
SyntaxQual               = 'serialization' , SyntaxRef ;
LibraryName             = IRI ;
\end{lstlisting}

\begin{lstlisting}[language=ebnf,escapechar=+,morecomment={[l]{\%\%\ }}]
PrefixMap                = '%prefix(' , { PrefixBinding } , ')%' ;
PrefixBinding            = BoundPrefix , IRIBoundToPrefix , [ Separators ] ;
BoundPrefix              = ':' | Prefix ; +$<$\rm see definition in \cref{c:curies}$>$\CLnote[type=q-aut]{I think that, in contrast to OWL Manchester, we can allow prefix names that match keywords of the DOL syntax, as we are enclosing the whole prefix map into an annotation construct -- right?}+ 
IRIBoundToPrefix         = '<' , FullIRI , '>' ;
Separators               = 'separators' , String , String ;
                           +$<$\rm see definition in \cref{c:curies}$>$+
\end{lstlisting}

Note that we denote the empty prefix (called ``no prefix'' in \nisref{W3C/TR REC-rdfa-core:2013, Section 6}) by a colon inside the prefix map, but completely omit it in CURIEs.  This is the style of the OWL Manchester syntax \cite{W3C:NOTE-owl2-manchester-syntax-20091027} but differs from the RDFa Core 1.1 syntax.

\vspace{1em}

\ssclause{Networks}

\begin{lstlisting}[language=ebnf,escapeinside={()},morecomment={[l]{\%\%\ }}]

NetworkDefn            = 'network' , NetworkName , '=' , 
                         [ ConsStrength ] , Network ;
NetworkName            = IRI ;
Network                = NetworkElements , [ ExcludeExtensions ] ;
NetworkElements        = NetworkElement , { ',' , NetworkElement } ;
NetworkElement         = [ Id , ':' ] , OMSOrMappingorNetworkRef ;
ExcludeExtensions      = 'excluding' , ElementRef , { ',' , ElementRef } ;
ElementRef             = IRI , '->' , IRI 
                         | OMSOrMappingorNetworkRef;
OMSOrMappingorNetworkRef        = IRI ;
Id                     = Letter , { LetterOrDigit } ;
\end{lstlisting}

\ssclause{OMS}\label{a:dol-text:OMS}

While in most cases the translation from concrete to abstract syntax
is obvious (the structure is largely the same), we note that both
\syntax{\%consistent} and \syntax{\%mcons} are translated to
\syntax{model-conservative}, while both \syntax{\%inconsistent} and
\syntax{\%notmcons} are translated to
\syntax{not-model-conservative}. Moreover, both \syntax{closed-world}
and \syntax{minimize} are translated to \syntax{minimize}.

                       
\begin{lstlisting}[language=ebnf,escapeinside={()},mathescape]
BasicOMS = ($<$)language and serialization specific($>$) ;
MinimizableOMS      = BasicOMS
                     | OMSRef , [ ImportName ] ; 
                     
ExtendingOMS        = MinimizableOMS
                     | MinimizeKeyword , '{' , MinimizableOMS , '}' ;
                     
OMS                 = ExtendingOMS
                     | OMS , Minimization 
                     | OMS , Translation
                     | OMS , Reduction
                     | OMS , Approximation
                     | OMS , Filtering
                     | OMS , 'and' , [ ConsStrength ] , OMS 
                     | OMS , 'then' , ExtensionOMS
                     | { Qualification } , ':' , GroupOMS
                     | 'combine' , NetworkElements , [ ExcludeExtensions ]  
                     | OMS , 'with' , SubstName
                     | GroupOMS ;

Minimization         = MinimizeKeyword , CircMin , [ CircVars ] ;
MinimizeKeyword      = 'minimize' | 'closed-world' | 'maximize' | 'free' | 'cofree' ;
CircMin = Symbol , {  Symbol } ;
CircVars  = 'vars' ,  ( Symbol , { Symbol } ) ;

GroupOMS            = '{' , OMS , '}'
                     | OMSRef ;

Translation          = 'with' , { LogicTranslation } , SymbolMapItems
                     | 'with' , LogicTranslation , { LogicTranslation } ;
LogicTranslation     = 'translation' , OMSLangTrans ;
                      
Reduction            = 'hide' , { LogicReduction } , SymbolItems 
                     | 'hide' , LogicReduction , { LogicReduction } 
                     | 'reveal' ,  SymbolItems ;
LogicReduction       = 'along' , OMSLangTrans ;

SymbolItems          = Symbol , { ',' , Symbol } ;
SymbolMapItems       = SymbolOrMap , { ',' , SymbolOrMap } ;

Extraction           = 'extract' , InterfaceSignature
                     | 'remove' , InterfaceSignature ;

Approximation        = 'forget' , InterfaceSignature , [ 'keep' , LogicRef ] 
                     | 'keep' , InterfaceSignature , [ 'keep' , LogicRef ] 
                     | 'keep' , LogicRef ;

Filtering            = 'select' , BasicOMS 
                     | 'reject' , BasicOMS ;

ExtensionOMS         = [ ExtConsStrength ] , [ ExtensionName ] , ExtendingOMS ;

ConsStrength         = Conservative
                     | '%mono'
                     | '%wdef'
                     | '%def' ;
ExtConsStrength      = ConsStrength | '%implied' ;
Conservative         = '%ccons'
                     | '%mcons'  
                     | '%notccons'  
                     | '%notmcons'  
                     | '%consistent'  
                     | '%inconsistent' ; 

InterfaceSignature   = SymbolItems ;

ImportName           = '%(' , IRI , ')%' ;
ExtensionName        = '%(' , IRI , ')%' ;

OMSkeyword          = 'ontology' | 'onto' | 'specification' | 'spec' | 'model' | 'oms' ;

OMSDefn             = OMSkeyword , OMSName , '=' , [ ConsStrength ] , 
                                   OMS , 'end'  ; 

Symbol               = IRI ;
SymbolMap            = Symbol , '|->' , Symbol ;
SymbolOrMap          = Symbol
                     | SymbolMap ;
Term                 = ($<$)an expression specific to an OMS language($>$) ;
Sentence             = ($<$)an expression specific to an OMS language($>$) ;

OMSName             = IRI ;

OMSRef              = IRI ;

LanguageRef          = IRI ;
LogicRef             = IRI ;
SyntaxRef            = IRI ;

LoLaRef              = LanguageRef
                     | LogicRef ;
\end{lstlisting}

\begin{lstlisting}[language=ebnf,mathescape]
OMSLangTrans        = OMSLangTransRef
                     | '->' , LoLaRef ;

OMSLangTransRef     = IRI ;
\end{lstlisting}

%\ednote{\%safe is more a statement about an import of a module, 
%and hence should be a statement in an OMS network. Recall:
%ModuleProperties     =  '\%safe' ; }

The above grammar allows for some grouping ambiguity when using operators in
OMS definitions. These ambiguities are resolved according to the following
list, listing operators in decreasing order of precedence:
\begin{itemize}
  \item \syntax{minimize}, \syntax{maximize}, \syntax{free}, and \syntax{cofree}. 
  \item \syntax{extract}, \syntax{forget}, \syntax{hide}, \syntax{keep},
    \syntax{reject}, \syntax{remove}, \syntax{reveal}, \syntax{select}, and
    \syntax{with}.
  \item \syntax{and}.
  \item \syntax{then}.
\end{itemize}
Multiple occurrences of the same operator are grouped in a left associative
manner. In all other cases operators on the same precedence level are not
implicitly grouped and have to be grouped explicitly. Omitting such an explicit
grouping results in a parse error.

\ssclause{OMS Mappings}\label{a:dol-text:mappings}
\index{alignment}
\newcommand*{\lessthan}{<}
\newcommand*{\greaterthan}{>}
\begin{lstlisting}[language=ebnf,mathescape]
MappingDefn             = IntprDefn | Entailment | EquivDefn | ModuleRelDefn | AlignDefn ;

IntprDefn            = IntprKeyword , IntprName , [ Conservative ] , ':' , IntprType ,  'end'
                     | IntprKeyword , IntprName , [ Conservative ] , ':' , IntprType , '=' ,
                       { LogicTranslation } , [ SymbolMapItems ] ,  'end' 
                     | IntprKeyword , IntprName , '=' , Refinement ,  'end' ;

IntprKeyword         = 'interpretation' | 'view' | 'refinement' ;
IntprName            = IRI ;
IntprType            = GroupOMS , 'to' , GroupOMS ;

Refinement           = GroupOMS 
                     | NetworkName
                     | Refinement , 'then' , Refinement
                     | GroupOMS , 'refined' , [RefMap] , 'to' , Refinement 
                     | NetworkName , 'refined' , [RefMap] , 'to' , Refinement ;
RefMap               = 'via' , LogicTranslation , [ SymbolMapItems ]
                     | 'via' , [ LogicTranslation ] , SymbolMapItems
                     | 'via' , NodeMap , { ',' , NodeMap } ;
NodeMap              = OMSName , '|->' , OMSName , [ 'using' , { LogicTranslation } , [ SymbolMapItems ] ] ;

Entailment           = 'entailment' , EntailmentName , '=' , EntailmentType , 'end' ;
EntailmentName       = IRI ;
EntailmentType       = GroupOMS , 'entails' , GroupOMS
                     | OMSName , 'in' , Network , 'entails' , GroupOMS
                     | Network , 'entails' , Network ;

EquivDefn            = 'equivalence' , EquivName , ':' , EquivType ,  'end' ;
EquivName            = IRI ;
EquivType            = GroupOMS , '<->' , GroupOMS  , '=' , OMS 
                     | Network , '<->' , Network , '=' , Network ;

ModuleRelDefn        = 'module' , ModuleName , [ Conservative ] , ':' , ModuleType ,
                       'for' , InterfaceSignature ;
ModuleName           = IRI ;
ModuleType           = GroupOMS , 'of' , GroupOMS ;

AlignDefn            = 'alignment' , AlignName , [ AlignCards ] , ':' , AlignType ,  'end'
                     | 'alignment' , AlignName , [ AlignCards ] , ':' , AlignType , '=' ,
                       Correspondence , { ',' , Correspondence } ,  
                       'assuming' , AlignSem , 'end' ;

AlignName            = IRI ;
AlignCards           = AlignCardForward , AlignCardBackward ;
AlignCardForward     = AlignCard ;
AlignCardBackward    = AlignCard ;
AlignCard            = '1' | '?' | '+' | '*' ;
AlignType            = GroupOMS , 'to' , GroupOMS ;
AlignSem            = 'SingleDomain' | 'GlobalDomain'  | 'ContextualizedDomain' ;

Correspondence       = CorrespondenceBlock
                     | SingleCorrespondence
                     | '*' ;
CorrespondenceBlock  = 'relation' , [ RelationRef ] , [ Confidence ] , 
                       '{' , Correspondence , { ',' , Correspondence } , '}' ;
SingleCorrespondence = SymbolRef , [ RelationRef ] ,
                       [ Confidence ] , TermOrSymbolRef , [ CorrespondenceId ] ;
CorrespondenceId     = '%(' , IRI , ')%' ;
SymbolRef            = IRI ;
TermOrSymbolRef      = Term | SymbolRef ;
RelationRef          = '>' | '<' | '=' | '%' | 'ni' | 'in' | IRI ;
Confidence           = Double ; 
\end{lstlisting}
\begin{lstlisting}[language=ebnf,escapeinside={()}]
Double               = ($<$ a number $\in [0,1]$ $>$) ;
\end{lstlisting}

\ssclause{Queries}

\begin{lstlisting}[language=ebnf,escapeinside={<>},mathescape]
QueryRelatedDefn     = QueryDefn | SubstDefn | ResultDefn ;
QueryDefn            = 'query' , QueryName , '=' , 'select' , Vars , 
                                'where' , Sentence , 'in' , GroupOMS , 
                                ['along' , OMSLangTrans] , 'end' ;
SubstDefn            = 'substitution' , SubstName , ':' , GroupOMS , 'to' , GroupOMS , 
                                       '=' , SymbolMapItems , 'end' ;
ResultDefn           = 'result' , ResultName , '=' , SubstName , { ',' , SubstName } ,
                                 'for' , QueryName , [ '%complete' ] , 'end' ;
QueryName            = IRI ;
SubstName            = IRI ;
ResultName           = IRI ;
Vars                 = Symbol , { ',' , Symbol } ;
\end{lstlisting}

\sclause{Identifiers}

\begin{lstlisting}[language=ebnf,escapeinside={()}]
IRI     = '<' , FullIRI , '>' | CURIE ;
FullIRI = ($<$ an IRI as defined in \nisref{IETF/RFC 3987:2005} $>$) ;
CURIE     = MaybeEmptyCURIE , - ;
MaybeEmptyCURIE = [ Prefix ] , RefWithoutComma ;
RefWithoutComma = Reference , - , StringWithComma ;
StringWithComma = { UChar } , ',' , { UChar } ;
UChar     = ($<$ any Unicode \nisref{ISO/IEC 10646} character $>$) ;
Prefix    = NCName , ':' ; ($<$ \rm see ``NCName'' in \nisref{W3C/TR REC-xml-names:2009}, Section 3 $>$)
Reference = Path , [ Query ] , [ Fragment ] ;
Path      = ipath-absolute | ipath-rootless | ipath-empty ;
            ($<$ \rm as defined in \nisref{IETF/RFC 3987} $>$)
Query     = '?' , iquery ; ($<$ \rm as defined in \nisref{IETF/RFC 3987} $>$)
Fragment  = '#' , ifragment ; ($<$ \rm as defined in \nisref{IETF/RFC 3987} $>$)
\end{lstlisting}

In a CURIE without a prefix, the \syntax{reference} part is \notallowed to match any of the keywords of the DOL syntax (cf.\ clause \label{c:keywords}).

\sclause{Lexical Symbols}

The character set for the DOL text serialization is the UTF-8 encoding of Unicode \nisref{ISO/IEC 10646}.  However, OMS can always be input in the Basic Latin subset, also known as US-ASCII.\footnote{In this case, IRIs will have to be mapped to URIs following section 3.1 of \nisref{IETF/RFC 3987:2005}.}  For enhanced readability of OMS, the DOL text serialization particularly supports the native Unicode glyphs that represent common mathematical operators.%\todonote[author=Christoph Lange,type=q-aut]{@Till: I took part of that from the CASL reference manual.  I don't think we want/need to specify more than that.  I wouldn't say anything about ``display formats of lexical symbols'', for example.}

\ssclause{Key words and signs}\label{c:keywords}

The lexical symbols of the DOL text serialization include various key words and signs that occur as terminal symbols in the context-free grammar in \aref{a:dol-text:concrete}.  Key words and signs that represent mathematical signs are displayed as such, when possible, and those signs that are available in the Unicode character set may also be used for input.

\sssclause{Key words}

Key words are always written lowercase. The following key words are reserved, and are not available for use as variables or as CURIEs with no prefix\footnote{In such a case, one can still rename affected variables, or declare a prefix binding for affected CURIEs, or use absolute IRIs instead.  None of these rewritings changes the semantics.}, although they can be used as parts of tokens. 

{\ttfamily %
and
end
hide
interpretation
library
logic
minimize
network\\
model
onto
ontology
spec
specification
reveal
then
to
vars
view
with
keep
forget
select
reject
%
for
result
substitution
% #
% ?
% :
% >
% <
% ,
% =
along
where
query
ni
in
% \%(
% )\%
% }
% {
% *
relation
% +
% 1
assuming
alignment
of
module
% < - >
equivalence
entails
entailment
using 
% |->
via
refined
refinement
% - >
oms
\%complete
\%inconsistent
\%consistent
\%notmcons
\%notccons
\%mcons
\%ccons
\%implied
\%def
\%wdef
\%mono
remove
extract
translation
cofree
free
maximize
closed-world
combine
excluding
separators
\%prefix(
serialization
language
import
}

\sssclause{Key signs}

Table~\ref{tab:key-signs} following key signs are reserved, and are not available for use as complete identifiers.  Key signs that are outside of the Basic Latin subset of Unicode may alternatively be encoded as a sequence of Basic Latin characters.

\newcolumntype{T}{>{\ttfamily}{l}}
\ctable[
  caption={Key Signs},
  label={tab:key-signs},
]{TTT}{
}{\FL
  \rmfamily Sign & \rmfamily Unicode Code Point & \rmfamily Basic Latin substitute \ML
  \{   & U+007B LEFT CURLY BRACKET & \NN
  \}   & U+007D RIGHT CURLY BRACKET & \NN
  :    & U+003A COLON & \NN
  =    & U+003D EQUALS SIGN & \NN
  ,    & U+002C COMMA & \NN
  \rmfamily ↦ & U+21A6 RIGHTWARDS ARROW FROM BAR & |-> \NN
  \rmfamily → & U+2192 RIGHTWARDS ARROW & -> \NN
}

\sclause{Integration of Serializations of Conforming Languages}
\label{sec:existing-serialization}
Any document providing an OMS in a serialization of a DOL conforming
language can be used as-is in DOL, by reference to its IRI.

The following cases apply for injecting identifiers into fragments of OMS languages, depending on the conformance level of the respective serialization of the OMS language used in terms of section~\ref{c:conform:serialization}:
\begin{description}
\item[XML conformance] Identifiers are added to XML elements by using the IRI-valued \textit{dol:id} XML attribute from the \url{http://www.omg.org/spec/DOL/1.0/xml} namespace, or, if the serialization does not support this attribute, by adding a \textit{dol:id} XML element as the first child, containing exactly one text node with the IRI.
\item[RDF conformance] The RDF data model itself enables the assignment of IRI identifiers to all resources.
\item[Text conformance] Identifiers are added by inserting a special comment immediately\footnote{The serialization \may allow whitespace between the keyword and the comment.} after the structural OMS element to be annotated, or, if this is not allowed and no ambiguity arises from inserting the comment \emph{before} the structural element, by doing the latter.  The complete comment \shall read \texttt{\%(I)\%} if the language uses the \texttt{\%} character to introduce comments, where \texttt{I} is the identifier IRI.  If the language uses a different comment syntax, the \emph{content} of the comment \shall start with \texttt{\%(I)\%}, possibly preceded by whitespace.
\item[Standoff markup conformance] Standard mechanisms such as XPointer (\nisref{W3C/TR REC-xptr-framework:2003}) or \nisref{IETF/RFC 5147} shall be used as means of non-destructively assigning a URI to pieces of XML or text in the given OMS serialization.
\end{description}
\ednote{TODO: injection of identifiers addressed, but we also had \%implies etc.  The latter will probably be handled in a similar way, but I don't know how \emph{exactly}.}

Where the given OMS language does not provide a way of assigning IRIs to a desired subject of an annotation (\eg if one wants to annotate an import in OWL), a library may employ RDF annotations that use XPointer or \nisref{IETF/RFC 5147} as means of non-destructively referencing pieces of XML or text by URI.\footnote{We intend to utilise the extensibility of the XPointer framework by developing additional XPointer schemes, \eg for pointing to subterms of Common Logic sentences.}


\part*{Annex}
\addcontentsline{toc}{part}{Annex}

\appendix

\chapter[LoLa RDF Vocabulary]{Annex (normative): LoLa, an RDF vocabulary that implements the DOL terminology}\label{a:lola}


This annex specifies LoLa, an RDF vocabulary that implements the terms and definitions from \cref{terms-and-defs}.
Applications of LoLa include modeling statements about OMS in RDF, e.g., when annotating OMS, or when describing new conforming logics, OMS languages, serializations, translations, etc., in the \termref{registry} stipulated by chapter~\ref{c:conformance}.
LoLa is currently maintained as an OWL ontology and, prospectively, as an OMS library implemented in DOL, at \url{https://ontohub.org/meta/lola/ontology}.\footnote{The preferred location for LoLa snapshots being part of this OMG standard is \url{http://www.omg.org/spec/DOL/Current/lola}.}.
For a full treatment of the background and design considerations of LoLa please see~\cite{LMK:LoLaModularOntologyLogLangTrans12}.

The tables in this annex list the classes and object properties of LoLa and thus the essential parts of its implementation.  All classes and object properties are assumed to be in the LoLa namespace unless stated otherwise.

\tref{tab:logic-vocab-classes} lists the classes of LoLa.  Each row of the table translates into the following OWL declarations (given in OWL Manchester syntax~\cite{W3C:NOTE-owl2-manchester-syntax-20091027}).  The definitions of the classes can be found in \cref{terms-and-defs}, sometimes under different names if stated so in the table.  Classes rendered in italics are abstract superclasses that have no direct correspondence in the terminology.

\begin{lstlisting}[language=owl2Manchester]
Class: ...
  SubClassOf: ...
\end{lstlisting}

\newcommand*{\ClassDocumentation}[1]{\textit{#1}}
\ctable[
caption={LoLa Classes},
mincapwidth=\textwidth,
label={tab:logic-vocab-classes},
pos=h,
]{p{.27\textwidth}p{.45\textwidth}p{.22\textwidth}}{% table footnotes
}{\FL
  Class & Superclass & Section \ML
  \textit{Language} & & \NN
  OMSLanguage & \textit{Language} & \ref{c:native-oms} \NN
  Logic & & \ref{c:term-logic} \NN
  Serialization & & \ref{c:term-serializations} \NN
  Mapping & & \ref{c:mappings} (OMS mapping) \NN
  LanguageMapping & Mapping & \NN
  LogicMapping & Mapping & \NN
  Translation & Mapping & \NN
  Reduction & Mapping & \NN
  DefaultMapping & Mapping & \ref{c:terms-features} \NN
  WeaklyExactMapping & Mapping & \ref{s:foundations} \NN
  ExactMapping & WeaklyExactMapping & \ref{s:foundations} \NN
  FaithfulMapping & Mapping & \ref{c:terms-features} \NN
  ModelExpansiveMapping & FaithfulMapping & \ref{c:terms-features} \NN
  ModelBijectiveMapping & ModelExpansiveMapping & \NN
  Embedding & ModelBijectiveMapping, LogicMapping, Translation & \ref{s:foundations} \NN
  PlainMapping & Mapping & \NN
  SimpleTheoroidalMapping & Mapping & \ref{c:term-logic} \LL
}

\tref{tab:logic-vocab-prop} lists the object properties of LoLa.  Each row of the table translates into the following OWL declarations (given in OWL Manchester syntax).  The definitions of the properties can be found in \cref{terms-and-defs}, sometimes under different names if stated so in the table.

\begin{lstlisting}[language=owl2Manchester]
ObjectProperty: ...
  Domain: ...
  Range: ...
  SubPropertyOf: ...
\end{lstlisting}

%\todonote[type=q-aut,author=Christoph Lange]{we need to define ``sublogic'' as a term – how?  I guess that would include the notion of an ``OWL profile''. TM: has been defined in section 4}
% \newcommand*{\PropertyDocumentation}[1]{\NN\multicolumn{3}{p{\linewidth}}{\textit{#1}}}
\ctable[
caption={LoLa Properties},
width=\linewidth,
mincapwidth=\textwidth,
label={tab:logic-vocab-prop},
pos=h,
]{lllX}{% table footnotes
}{\FL
  Property & Domain & Range & Section \ML
  isSubLogicOf & Logic & Logic & \ref{c:term-logic} \NN
  % \PropertyDocumentation{The subject is a sublogic of the object}\ML
  supportsLogic & Language & Logic & \ref{c:term-logic} \NN
  % \PropertyDocumentation{The subject OMS language has a semantics specified in terms of the object logic.}\ML
  specifiesSemanticsOf & Logic & Language & inverse of supportsLogic \NN
  % \PropertyDocumentation{The subject logic is used to specify the semantics of the object OMS language; inverse of supportsLogic.}\ML
  supportsSerialization & Language & Serialization & \ref{c:term-serializations} \NN
  % \PropertyDocumentation{OMS in the subject OMS language can be serialized in the object serialization.  Note that the serialization should be as specific as possible, \ie one should not say that ``OWL can be serialized in XML'' and ``Common Logic can be serialized in XML'', but instead ``OWL can be serialized in OWL/XML'' and ``Common Logic can be serialized in XCL'', taking into account that OWL/XML and XCL are two different XML languages.}\ML
  serializes & Serialization & Language & \ref{c:term-serializations} \NN
  % \PropertyDocumentation{The subject logic is used to specify the semantics of the object OMS language; inverse of supportsSerialization.}\LL
}

\infannex{Conformance of OWL 2 DL With DOL}\label{a:owl}

The semantic conformance of OWL 2 DL (as specified in \nisref{W3C/TR REC-owl2-syntax:2009}) with DOL
is established in \cite{OntoGraph}.

The OWL/XML serialization satisfies the criteria for XML conformance.  The mapping of OWL 2 DL to RDF
graphs satisfies the criteria for RDF conformance\CLnote{This is not exactly true, as some things,
e.g. imports, cannot be identified.}.  The OWL 2 Manchester syntax satisfies the criteria for text
 conformance.
%~\CLnote{also need conformance propositional logic; use PL ``profile'' of the CASL ``IFIP standard''}

OWL can be formalized as an institution as follows:
\begin{definition}\label{DL} \defsty{OWL 2 DL.} 
\OWL~2~DL is the description logic (DL) based fragment of the web ontology language \OWL. 
We start with the simple description logic $\ALC$, and then proceed
to the more complex description logic \SROIQ which is underlying \OWL~2~DL.
Signatures of the description logic $\ALC$ consist of a set  ${\mathcal A}$ of
atomic concepts, a set ${\mathcal R}$ of roles and a set ${\mathcal
I}$ of individual constants. Signature morphisms are tuples of
functions, one for each signature component.
Models are  first-order structures $I = (\Delta^I, .^I)$ with universe $\Delta^I$
that interpret concepts as unary and roles as binary predicates
(using $.^I$). $I_1\leq I_2$ if $\Delta^{I_1}=\Delta^{I_2}$ and all
concepts and roles of $I_1$ are subconcepts and subroles of those in $I_2$.
Sentences are subsumption relations $C_1\sqsubseteq C_2$ between
concepts, where concepts follow the grammar
%\CLnote[type=q-aut]{This grammar should also be adapted to ISO EBNF.}
$$C ::= {\mathcal A} \,|\, \top\,|\, \bot \,|\, C_1 \sqcup C_2 \,|\, C_1 \sqcap C_2 \,|\, \neg C 
    \,|\, \forall R . C \,|\, \exists R . C$$
These kind of sentences are also called TBox sentences.
 Sentences can also be ABox sentences, which are
membership assertions of individuals in concepts (written $a:C$ for
$a\in{\mathcal I})$ or pairs of individuals in roles (written $R(a,b)$
for $a,b\in{\mathcal I}, R\in{\mathcal R}$).   Satisfaction is the
standard satisfaction of description logics.

The logic \SROIQ \cite{SROIQ}, which is the logical core of the Web Ontology
Language 2 DL\footnote{See also \url{http://www.w3.org/TR/owl2-overview/}}, extends $\ALC$
with the following constructs: (i) complex role inclusions such as $R \circ S \sqsubseteq S$
as well as simple role hierarchies such as $R \sqsubseteq S$,
assertions for symmetric, transitive, reflexive, asymmetric and
disjoint roles (called RBox sentences, denoted by $\mathcal{SR}$), as well as the construct
$\exists R . \mathsf{Self}$ (collecting the set of `$R$-reflexive
points'); (ii) nominals, i.e.\ concepts of the form $\{a\}$, where $a\in\mathcal{I}$ (denoted by $\mathcal{O}$); (iii) inverse
roles (denoted by $\mathcal{I}$); qualified and unqualified number
restrictions ($\mathcal{Q}$). For details on the rather complex
grammatical restrictions for \SROIQ (e.g.\ regular role inclusions,
simple roles) compare \cite{SROIQ}.

\emph{profiles} are syntactic restrictions of \OWL~2~DL that support specific modeling and reasoning tasks, %\cite{w3c:owl2-profiles}, 
and which are accordingly based on DLs with appropriate computational properties. Specifically, \OWL~2~EL is designed for ontologies containing large numbers of concepts or relations, \OWL~2~QL to support query answering over large amounts of data, and \OWL~2~RL to support scalable reasoning using rule languages (EL, QL, and RL for short) .
 
We sketch the logic ELDL which is underlying the EL profile.\footnote{To be exact, EL adds various `harmless' expressive means and syntactic sugar to ELDL resulting in the DL ELDL. % \cite{BaaderEtAl-OWLED08DC}; for further details see also \cite{w3c:owl2-profiles}.
} 
ELDL is a syntactic restriction of ALC to existential restriction, concept
intersection, and the top concept:
%\ednote{TM@OK: please be  a bit more precise here, perhaps write some grammar: C ::= ⊤ | A | C ⊓ D | ∃r.C, footnote about added sugar in OWL EL profile} Note that EL is a very relevant ontology language; large medical ontologies like SNOMED\ednote{CL@TM: FYI, it's SNO not SNOW} CT are epxressed in \EL.\ednote{TM@OK: add RL and QL if there is space}
%\ednote{Text entfernt: ``I.e.\ its concepts follow the following grammar'' -- versteht sich IMHO von selbst, nachdem man das obige \ALC-Beispiel gelesen hat}
$$C ::= {\mathcal A} \,|\, \top \,|\,  C_1 \sqcap C_2 \,|\, \exists R . C$$
Note that ELDL does not have disjunction or negation, and is therefore a sub-Boolean logic.
\qed\end{definition}

Remark: strictly speaking, the institution defined above is
\emph{{OWL} 2 DL without restrictions} in the sense of
\cite{DBLP:conf/owled/SchneiderRS13}. The reason is that in an
institution, the sentences can be used for arbitary formation of
theories. This is related to the presence of DOL's union operator on
OMS.  OWL 2 DL's specific restrictions on theory formation can be
modeled \emph{inside} this institution, as a constraint on OMS.  This
constraint is generally not preserved under unions or
extensions. DOL's multi-logic capability allows the clean distinction
between ordinary OWL 2 DL and {OWL} 2 DL without restrictions.


%\infannex{Bibliography}
\newpage

\clearpage

\bibliographystyle{plain} 
\renewcommand{\bibname}{References}
\label{a:bibliography}
\bibliography{dol,rfc}
\addcontentsline{toc}{chapter}{References}
%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%


%%%
%%% Index of Keywords, taken out 
%%%

% \newpage
% \clearpage
%
% %\backmatter
% \printindex
% \addcontentsline{toc}{chapter}{Keyword index}
% \blankpage
%
\end{document}