\documentclass{article}

\usepackage{isolatin1,xspace,url}

\usepackage{../../utils/hetcasl}

\newcommand{\CASL}{\textsc{Casl}\xspace}

\newcommand{\CASLDL}{\textsc{Casl\_DL}\xspace}

\begin{document}

\author{Klaus L�ttich}

\title{Design and Notes for the \CASLDL Node in Hets}

\maketitle

\section{Issues (with implementation options)}

\textbf{Note:} The following issues very often mention the not jet

complete OWL DL logic (node) of Hets. Clearly the development of

\CASLDL and OWL DL support in Hets must be closely coupled.

\subsection{Each OWL DL-File is one Named Spec}

Where do we get the name from:

\begin{itemize}

\item Name derived from URI of the OWL DL-File.

\item Ontologies in OWL DL can be named. We should encourage people

to do so and use that one.

\item (Given as annotation to the Ontology in the OWL DL-File.)

\end{itemize}

But is every named spec an OWL DL-file? Do we generate OWL DL-files

for parametrised specifications? An Annotation should map

specification names to URIs and only these specs are exorted to OWL

DL files. (each of these URIs should have a Namespace abbrev for the

disambiguation when an imported ontology is extended)

How to treat circlar imports in the development graph. The OWL DL

parser will parse each URI pointing to an OWL file importes or not

only once. This even applies if an OWL DL file is not loaded form

the document inherent base URI which is seen as the URI of the

ontology in any case.

\subsection{Structuring an ontology inside an OWL DL-File}

Annotations (on the OWL DL side) can point to parts that are

extensions. \emph{not in the paper}

So we could reflect some structuring made in \CASLDL. But

keeping track of parametrised specifications is not easy.

\subsection{Structuring on the \CASLDL side}

flattened into a set of named theories each resulting into one OWL

DL file. After conversion back from spme genrated OWL DL files the

structuring is lost. (or we have to add many Annotations to the

generated OWL DL output)

\subsection{Cardinality Restrictions}

\begin{itemize}

\item An instantiation of GenCardinality must be traced. All

renamings should end up in a table that could resemble a

minCardinality[pred\_name] for translation to OWL DL. \emph{paper

conforming}

\item new FORMULA variants, that have directly the semantics of

Cardinality Restrictions. No tracing is needed. Only the the

embedding into \CASL is a little bit harder, as the instantiation

has to be generated. \emph{Not paper conforming}

\end{itemize}

\subsection{Namespaces} (1) global to library or (2) local to a named

specification or (3) to a basic specification?

\begin{enumerate}

\item means globally available but namespaces have to be

unified. Only possible as gobal annotations. Are they available in

the right place, need they still be in the \CASLDL-Signature?

Namespaces of different OWL DL-files need to be integrated.

(abbrevs should not collide, point to different URIs) The java

parser may (/ will) do this.

\item with annos this is not easy. Here it must be possible to

have all annos available during the analysis.

\item with annos this is not easy. Here it must be possible to

have all annos available during the analysis.

\end{enumerate}

\subsection{Symbols in / from different OWL DL files}

In OWL DL files symbols are unique in terms of URIs. But in \CASLDL

we want shorter ids than URIs. So we could use the last part of each

URI (\url{http://host/path#symbol}) but these symbols are no longer

unique. We could either use the name of the specification (OWL DL)

that declares this name. But a redeclaration is allways allowed. Or

the namespace abbrevs generated by the OWL DL parser could be

used. For a set of theories (containing ontologies) developed in

\CASLDL and translated to OWL DL the declaration of symbols is

seperated into different OWL DL files if we translate a development

graph into a set of OWL DL files.

\begin{itemize}

\item Namespace abbrevs go as first Id in compound

Identifier. Collides a little bit with minCardinality[pred\_name],

if this is an predicate Identifier obtained from an

instantiation. \newline (maybe minCardinality[OWL,pred\_name])

\item Namespace abbrevs are added as prefix to the Identifier with an

underscore only if needed for distinction and the real mapping of

identifiers into Namespaces (different OWL DL files) is written

down after a new keyword.

\end{itemize}

\subsection{Renaming of predefined concepts}

During symbol map analysis it must be ensured that \Id{Thing} and

\Id{Nothing} are never renamed and that they are always associated

with \verb|owl:Thing| and \newline \verb|owl:Nothing|.

\subsection{AnnotationProperties}

On the OWL DL side so called AnnotionProperties can be declared and

used. One of them is used for \CASLDL sort marking. But what to do

with the other AnnotationProperties?

Options:

\begin{enumerate}

\item keeping them as annotations in \CASLDL

\item declaring them as special binary relations, that could relate

with every symbol (sort name, pred name, op name)

\end{enumerate}

\section{Implementation decisions}

\subsection{Needed Annotations}

\begin{description}

\item[Namespaces] \

{\small"\KW{\%owl\_namespace(}" (QURI "=$>$" SIMPLE\_ID )+ "\KW{)\%}"}

mapping URIs to abbreviations that are kept during the translation

from and to OWL DL and that are used in compounds for the distinction

of symbols that would otherwise clash.

\item[Mapping of spec names to URIs (files)]\

{\small"\KW{\%owl\_export(}" (SIMPLE\_ID "=$>$" "(" QURI "," FILE\_PATH

")" )+ "\KW{)\%}"}

Each named spec that should be transformed to an OWL DL file must get

an URI and file path. The URI is used as the base URI of the xml (owl)

document.

\end{description}

QURI ::= "\textbackslash"" URI "\textbackslash""

\subsection{Needed Formula Extensions}

For Cardinality Restrictions three symbols are introduced which are

also reserved symbols then. They will be parsed as a predication of a

compound id with exactly one compound and two arguments: (1) a

variable quantified over Thing or a subsort of it and (2) a number

literal denoting the number of relations for each member of the

characterized class (type: \Id{nonNegativeInteger}).

\begin{hetcasl}

\Id{minCardinality}[PRED\_NAME](\Id{x}, NUMBER\_LITERAL)\\

\Id{maxCardinality}[PRED\_NAME](\Id{x}, NUMBER\_LITERAL)\\

\Id{cardinality}[PRED\_NAME](\Id{x}, NUMBER\_LITERAL)

\end{hetcasl}

\subsection{Needed Sign Extensions}

\begin{itemize}

\item Namespace abrreviation maps (maybe better as part of the

GlobalAnnos record)

\item renamed symbols mapped to their real name (OWL DL name) with

namespace abbrev (or URI)

\end{itemize}

\section{\CASLDL prelude}

A library of specifications in \CASLDL and \CASL named

\SId{CASL\_DL/Prelude}.

\subsection{\CASL specifications}

\SId{GenCardinality} from the WADT04 paper.

Theories of the known datatypes where all the opearations are hidden

except those needed for the construction of literals. These datatypes

are than collected under the supersort \Id{DATA}

\subsection{\CASLDL specifications}

Basic classes \Id{Thing} and \Id{Nothing} and their axiomatization.

A specification that embeds the \CASL specification of predefined

datatypes into \CASLDL (as predefined symbols that cannot be

changed).

A combining specification that provides access to \Id{Thing},

\Id{Nothing} and \Id{DATA} including all subsorts of \Id{DATA} and all

``literals'' in one of these. This specification will be called

something like \SId{CASL\_DL\_prelude}

\noindent\textbf{-- OR --}

Maybe its better not to have this embedding specification at

all and apply something behind the scenes to get the mixfix and static

analysis working with the predefined stuff visible.

\end{document}