CASL_DL-Notes.tex revision 73e5a7717d33e96b2759e7656a0c33617100a45d
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\documentclass{article}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\usepackage{isolatin1,xspace,url}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\usepackage{../../utils/hetcasl}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\newcommand{\CASL}{\textsc{Casl}\xspace}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\newcommand{\CASLDL}{\textsc{Casl\_DL}\xspace}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\begin{document}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\author{Klaus L�ttich}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\title{Design and Notes for the \CASLDL Node in Hets}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\section{Issues (with implementation options)}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\textbf{Note:} The following issues very often mention the not jet
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichcomplete OWL DL logic (node) of Hets. Clearly the development of
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\CASLDL and OWL DL support in Hets must be closely coupled.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{Each OWL DL-File is one Named Spec}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich Where do we get the name from:
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \begin{itemize}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \item Name derived from URI of the OWL DL-File.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \item Ontologies in OWL DL can be named. We should encourage people
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich to do so and use that one.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \item (Given as annotation to the Ontology in the OWL DL-File.)
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \end{itemize}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich But is every named spec an OWL DL-file? Do we generate OWL DL-files
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich for parametrised specifications? An Annotation should map
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich specification names to URIs and only these specs are exorted to OWL
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich DL files. (each of these URIs should have a Namespace abbrev for the
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich disambiguation when an imported ontology is extended)
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich How to treat circlar imports in the development graph. The OWL DL
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich parser will parse each URI pointing to an OWL file importes or not
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich only once. This even applies if an OWL DL file is not loaded form
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich the document inherent base URI which is seen as the URI of the
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich ontology in any case.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{Structuring an ontology inside an OWL DL-File}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich Annotations (on the OWL DL side) can point to parts that are
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich extensions. \emph{not in the paper}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich So we could reflect some structuring made in \CASLDL. But
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich keeping track of parametrised specifications is not easy.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{Structuring on the \CASLDL side}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich flattened into a set of named theories each resulting into one OWL
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich DL file. After conversion back from spme genrated OWL DL files the
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich structuring is lost. (or we have to add many Annotations to the
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich generated OWL DL output)
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{Cardinality Restrictions}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \begin{itemize}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \item An instantiation of GenCardinality must be traced. All
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich renamings should end up in a table that could resemble a
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich minCardinality[pred\_name] for translation to OWL DL. \emph{paper
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \item new FORMULA variants, that have directly the semantics of
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich Cardinality Restrictions. No tracing is needed. Only the the
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich embedding into \CASL is a little bit harder, as the instantiation
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich has to be generated. \emph{Not paper conforming}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{Namespaces} (1) global to library or (2) local to a named
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich specification or (3) to a basic specification?
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \begin{enumerate}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \item means globally available but namespaces have to be
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich unified. Only possible as gobal annotations. Are they available in
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich the right place, need they still be in the \CASLDL-Signature?
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich Namespaces of different OWL DL-files need to be integrated.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich (abbrevs should not collide, point to different URIs) The java
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich parser may (/ will) do this.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \item with annos this is not easy. Here it must be possible to
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich have all annos available during the analysis.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \item with annos this is not easy. Here it must be possible to
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich have all annos available during the analysis.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \end{enumerate}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{Symbols in / from different OWL DL files}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich In OWL DL files symbols are unique in terms of URIs. But in \CASLDL
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich we want shorter ids than URIs. So we could use the last part of each
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich URI (\url{http://host/path#symbol}) but these symbols are no longer
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich unique. We could either use the name of the specification (OWL DL)
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich that declares this name. But a redeclaration is allways allowed. Or
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich the namespace abbrevs generated by the OWL DL parser could be
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich used. For a set of theories (containing ontologies) developed in
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \CASLDL and translated to OWL DL the declaration of symbols is
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich seperated into different OWL DL files if we translate a development
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich graph into a set of OWL DL files.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \begin{itemize}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \item Namespace abbrevs go as first Id in compound
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich Identifier. Collides a little bit with minCardinality[pred\_name],
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich if this is an predicate Identifier obtained from an
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich instantiation. \newline (maybe minCardinality[OWL,pred\_name])
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \item Namespace abbrevs are added as prefix to the Identifier with an
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich underscore only if needed for distinction and the real mapping of
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich identifiers into Namespaces (different OWL DL files) is written
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich down after a new keyword.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich \end{itemize}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{Renaming of predefined concepts}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus LuettichDuring symbol map analysis it must be ensured that \Id{Thing} and
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\Id{Nothing} are never renamed and that they are always associated
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichwith \verb|owl:Thing| and \newline \verb|owl:Nothing|.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{AnnotationProperties}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus LuettichOn the OWL DL side so called AnnotionProperties can be declared and
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichused. One of them is used for \CASLDL sort marking. But what to do
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichwith the other AnnotationProperties?
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\begin{enumerate}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\item keeping them as annotations in \CASLDL
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\item declaring them as special binary relations, that could relate
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich with every symbol (sort name, pred name, op name)
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\end{enumerate}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\section{Implementation decisions}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{Needed Annotations}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\begin{description}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\item[Namespaces] \
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich{\small"\KW{\%owl\_namespace(}" (QURI "=$>$" SIMPLE\_ID )+ "\KW{)\%}"}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichmapping URIs to abbreviations that are kept during the translation
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichfrom and to OWL DL and that are used in compounds for the distinction
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichof symbols that would otherwise clash.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\item[Mapping of spec names to URIs (files)]\
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich{\small"\KW{\%owl\_export(}" (SIMPLE\_ID "=$>$" "(" QURI "," FILE\_PATH
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich ")" )+ "\KW{)\%}"}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus LuettichEach named spec that should be transformed to an OWL DL file must get
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichan URI and file path. The URI is used as the base URI of the xml (owl)
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\end{description}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus LuettichQURI ::= "\textbackslash"" URI "\textbackslash""
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{Needed Formula Extensions}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus LuettichFor Cardinality Restrictions three symbols are introduced which are
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichalso reserved symbols then. They will be parsed as a predication of a
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichcompound id with exactly one compound and two arguments: (1) a
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichvariable quantified over Thing or a subsort of it and (2) a number
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichliteral denoting the number of relations for each member of the
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichcharacterized class (type: \Id{nonNegativeInteger}).
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\begin{hetcasl}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\Id{minCardinality}[PRED\_NAME](\Id{x}, NUMBER\_LITERAL)\\
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\Id{maxCardinality}[PRED\_NAME](\Id{x}, NUMBER\_LITERAL)\\
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\Id{cardinality}[PRED\_NAME](\Id{x}, NUMBER\_LITERAL)
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{Needed Sign Extensions}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\begin{itemize}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\item Namespace abrreviation maps (maybe better as part of the
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich GlobalAnnos record)
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\item renamed symbols mapped to their real name (OWL DL name) with
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich namespace abbrev (or URI)
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\section{\CASLDL prelude}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus LuettichA library of specifications in \CASLDL and \CASL named
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\SId{CASL\_DL/Prelude}.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{\CASL specifications}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\SId{GenCardinality} from the WADT04 paper.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus LuettichTheories of the known datatypes where all the opearations are hidden
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichexcept those needed for the construction of literals. These datatypes
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichare than collected under the supersort \Id{DATA}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\subsection{\CASLDL specifications}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus LuettichBasic classes \Id{Thing} and \Id{Nothing} and their axiomatization.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus LuettichA specification that embeds the \CASL specification of predefined
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichdatatypes into \CASLDL (as predefined symbols that cannot be
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus LuettichA combining specification that provides access to \Id{Thing},
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\Id{Nothing} and \Id{DATA} including all subsorts of \Id{DATA} and all
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich``literals'' in one of these. This specification will be called
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichsomething like \SId{CASL\_DL\_prelude}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\noindent\textbf{-- OR --}
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus LuettichMaybe its better not to have this embedding specification at
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichall and apply something behind the scenes to get the mixfix and static
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettichanalysis working with the predefined stuff visible.
73e5a7717d33e96b2759e7656a0c33617100a45dKlaus Luettich\end{document}