\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}
[and when translating to CASL-DL,
the named spec is put into a file/CASL library that contains
only this named spec? Till] [No, if you parse an OWL DL file the
resulting abstract syntax will include all imported
specifications. This makes the handling of parsing and analysis
between Hets and an external parser much easier. So we generate a
development graph from this import structure. The parser already
handles cyclic imports as it does not read a known OWL DL file
hence it skips the import in food.owl. This development graph has
two nodes: food and wine where wine is an extension of
food. \emph{while writing this I recognized that splitting an
abstract syntax like this is not possible. There can be
mutally recursive defined symbols.} So circular imports lead to
one theory in Hets and we have to split such a theory back into
circular imports afterwards. Klaus]
[Although it seems to be the only way, it sounds a bit complicated.
Perhaps you could leave out the ``splitting back'' in a first
approximation. Till]
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 theory (spec) an OWL DL-file? [Yes, unless we
have a way to distingiush several named specs with one OWL DL file,
which seems not to be the case. Till ] Do we generate OWL DL-files
for parametrised specifications? [Yes. Till] [This is not very
useful. As there is no notion of parametrisation in OWL DL these
ontologies can't be used. The formal parameter specification
normally provides no meaning in terms of known concepts. Klaus]
[The reulting theory is just a loose theory, which may be useful
even without instantiation. Till] An
Annotation should map specification names to URIs and only these
theories are exported to OWL DL files. [But aren't auxilary specs
needed as well? Till] (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 development graph must be acyclic. Hence,
cyclic imports are not supported, unless the theories
are not really cyclic. Till]
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.
[I will implement some naming scheme for internal nodes soon.
Perhaps that helps a little. Till] [What will this naming scheme
look like? Can we discuss that before you start implementing it? Klaus]
[I have already done this. Till]
\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}
[don't know which one is better. Till] [Extendenting FORMULA seems
easier to me. So I implement that. Klaus]
\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}
[I vote for 1. Perhaps having only one DL spec per library
eases things? Other OWL tools also should have the problem
of name space integration w.r.t. imported files ?!? Till] [A
unification is done by the parser we currently consider, but all
imports become integrated into one abstract syntax. Klaus]
\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}
[I vote for the second possibility, because it keeps names shorter
whenever possible. Till] [I agree. Klaus]
\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 \
this means providing a declaration and an application annotation for
AnnotationProperties (see below).
\item declaring them as special binary relations, that could relate
with every symbol (sort name, pred name, op name)
\end{enumerate}
[I vote for 1. Why should annotations be integrated into models
via predicates? Till] [These AnnotationProperties have to be declared
on the OWL DL side like ordinary other properties. And they are
applied like other properties. We have no place in the Signature yet
for storing annotations that are passed over morphisms. Klaus]
[Sounds strange to me. But if this the way OWL DL works, we have
to support it. Till]
\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.
\item[Declaration and application of OWL Annotation Properties]\
OWL allows the declaration of untyped annotation properties. They can
be applied to all symbols / entities like the ontology as a whole and
to classes, properties and individuals. We will map them in \CASLDL to
\CASL annotations.
{\small"\KW{\%owl\_annotation\_properties(}" SIMPLE\_ID + "\KW{)\%}"}
{\small"\KW{\%owl\_annotations(}" (SIMPLE\_ID "(" CID "," ANNO-LITERAL ")") + "\KW{)\%}"}
\end{description}
QURI ::= "\textbackslash"" URI "\textbackslash""
ANNO-LITERAL ::= DATA-LITERAL $|$ URI $|$ INDIVIDUAL-ID
CID is a \CASL Id that must be declared in the current specification (library).
DATA-LITERAL is a literal allowed for a subsort of \Id{Data}.
INDIVIDULA-ID is the Id of a declared constant operation.
\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.
[I would vote for the first possibility. In CASL, there are no
predefined things, and we should keep this principle for
CASL-DL. Till] [This complicates checking the CASL\_DL language. Every
renaming of the predefined OWL DL datatypes and Symbols must be
rejected; every hiding, too. Klaus]
[But this can be implemented as an easy restriction on signature
morphisms. Till]
\end{document}