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