224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\documentclass{article}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\usepackage{isolatin1,xspace,url}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\newcommand{\CASL}{\textsc{Casl}\xspace}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\newcommand{\CASLDL}{\textsc{Casl\_DL}\xspace}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\begin{document}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\author{Klaus L�ttich}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\title{Proposals for changes collected from Hets Users}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\date{March 8, 2005}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\section{Introduction}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus LuettichThese document tries to describe request from different Hets users. It
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichalso tries to propose how to solve these issues. Most of these
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichrequests are related to ontology development and therefore are
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichcontributed by people from LOA in Trento, Italy. But some are just deficiencies
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichwhich was not thought of during the development of \CASL and its
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus LuettichReferenceManual.
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\section{Labels of instantiated formulas}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\paragraph{Problem:}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus LuettichIf a prarmetrised specification is is instantiated with different
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichparameters in the same specification all axiom labels from the
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichparametrised specifications point to different instantiations of these
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichaxioms. If such theories are translated to Isabelle for proving
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichseveral axioms have the same label. For this problem the \CASL
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus LuettichReference Manual and Hets do not offer any solution.
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\paragraph{Proposed solution:} Treating underscores as seperators in
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichaxiom labels and substituting words (only alphabetic charactars) which
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichare the same string as ids mentioned as sort, pred and / or
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichop symbols in the signature of parameter specifications with their
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichactual instances.
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus LuettichConsider the following example:
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\begin{hetcasl}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\SPEC \SId{GSpec} [\SORT[KW] \Id{s}] =\\
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\>\PRED \Id{R} : \Id{s} \Ax{\times} \Id{s}\\
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\>\FORALL \Id{x}: \Id{s}\\
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\>\BULLET \Id{R}(\Id{x}, \Id{x}) \hspace*{4cm} \casllabel{Ax1\_s}\\
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\SPEC \SId{Combination} =\\
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\> \SId{GSpec} [\SORT[KW] \Id{A}]\\
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\> \SId{GSpec} [\SORT[KW] \Id{B}]\\
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus LuettichCombination has than this theory:
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\begin{verbatim}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichforall x : A . R(x, x) %(Ax1_A)%
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichforall x : B . R(x, x) %(Ax1_B)%
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\end{verbatim}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\section{Quick indexing of (all) symbols in a theory}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\paragraph{Problem:} If you want to join two theories which have
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichoverlaps in their signatures such tthat for many sorts the same names
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichwere used. And even the symbols for predicates overlap. Giving a
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichcomplete mapping of all distinct ids of sorts, preds and / or ops to
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichdifferent ids can be very tedious and it could easily lead to errors
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichas one can overlook some symbols which have the same id.
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\paragraph{Proposed solution:} Add a compound to all ids or only to
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichthe sorts, preds or ops. this could be achieved by a new keyword in
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichsymbol mappings of translations: \KW{indexed\_by} It could be used as
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettichin this example:
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\input{IndexingExample}
224d2b804fd6f92d9d553a3d6fe54dd14a73dde2Klaus Luettich\end{document}