UserGuide.tex revision 8d576513b8c89016a3d678378ed75cac0e2e1aef
56f499bbc75665b431ab11e7f9f3fb05f2607c52Paolo Torrini\documentclass{article}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\usepackage{alltt}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\usepackage{casl}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\usepackage{xspace}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\usepackage{color}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\usepackage{url}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\usepackage{threeparttable,hhline}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\usepackage[pdfborder=0 0 0,bookmarks,
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrinipdfauthor={Till Mossakowski, Christian Maeder, Klaus Lüttich},
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipdftitle={Hets User Guide}]
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski{hyperref} %% do not load more packages after this line!!
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newcommand{\QUERY}[1]%{}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newcommand{\eat}[1]{}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand{\IEXT}[1] {\\#1\I}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newcommand{\IEND} {\I\END}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newenvironment{EXAMPLEFORMAT} {}{}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski%% Added by MB to have some extra vertical space after the ``main'' examples
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski%% following the points (and some others in the text):
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
5175cc8f6f6980c8f39123859284391ff51f5f55Paolo Torrini\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newenvironment{DETAILSFORMAT} {}{}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \begin{minipage}{0.9\textwidth}\it}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini {\end{minipage}\par\medskip}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand{\SLIDESMALL} {}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand{\SLIDESONLY}[1] {}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% SIMULATING SMALL-CAPS FOR BOLD, EMPH
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski%\newcommand {\CoFI}{CoFI\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%%%%% Klaus macros
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%%%%% end of Klaus macros
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newcommand{\LCF}{LCF\xspace}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newcommand{\ASF}{ASF\xspace}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand{\SDF}{SDF\xspace}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\newcommand{\CCC}{CCC\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{document}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\title{{\bf \protect{\LARGEHets} User Guide}\\
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski-- Version 0.85 --}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\author{Till Mossakowski, Christian Maeder, Klaus L\"{u}ttich\\[1em]
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiDFKI Lab Bremen, Bremen, Germany.\\[1em]
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiComments to: hets-users@informatik.uni-bremen.de \\
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski(the latter needs subscription to the mailing list)
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\section{Introduction}
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe Heterogeneous Tool Set (\protect\Hets) is the main analysis tool
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskifor the specification language heterogeneous \CASL. Heterogeneous
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\CASL (\HetCASL) combines the specification language \CASL
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\cite{CASL-UM,CASL/RefManual} with \CASL extensions
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiand sublanguages, as well as completely different logics and even
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiprogramming languages such as Haskell. \HetCASL
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski(see Fig.~\ref{fig:lang} for a simple subset)
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiextends the structuring mechanisms of \CASL:
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\emph{Basic specifications} are
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiunstructured specifications or modules written in a specific logic.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe graph of currently supported logics and logic translations (the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskilatter are also called comorphisms) is shown in
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiFig.~\ref{fig:LogicGraph}, and the degree of support by \Hets in
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiFig.~\ref{fig:Languages}.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{figure}[ht]
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{verbatim}
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiSPEC ::= BASIC-SPEC
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski | SPEC then SPEC
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski | SPEC then %implies SPEC
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski | SPEC with SYMBOL-MAP
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski | SPEC with logic ID
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiDEFINITION ::= logic ID
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski | spec ID = SPEC end
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski | view ID : SPEC to SPEC = SYMBOL-MAP end
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski | view ID : SPEC to SPEC = with logic ID end
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiLIBRARY = DEFINITION*
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\end{verbatim}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\caption{Syntax of a simple subset of the heterogeneous
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskispecification language.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskispecific syntax, while \texttt{ID} stands for some form of
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiidentifiers.\label{fig:lang}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiWith \emph{heterogeneous structured specifications}, it is possible to
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskicombine and rename specifications, hide parts thereof, and also
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiprescribe the structure of implementations. \emph{Specification
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski libraries} are collections of named structured and architectural
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskispecifications.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\Hets consists of logic-specific tools for the parsing and static
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskianalysis of the different involved logics, as well as a
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskilogic-independent parsing and static analysis tool for structured and
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskito call the logic-specific tools whenever a basic specification is
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\Hets is based on the theory of institutions \cite{GoguenBurstall92},
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiwhich formalize the notion of a logic. The theory behind \Hets is laid
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiout in \cite{Habil}. A short overview of \Hets is given in
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\cite{MossakowskiEA06,MossakowskiEtAl07b}.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\section{Logics supported by Hets}
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe following list of logics (formalized as so-called institutions
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\cite{GoguenBurstall92}) is currently supported by \Hets:
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{figure}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \begin{center}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski \includegraphics[scale=0.4]{LogicGraph}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\caption{Graph of logics currently supported by \Hets. The more an
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\label{fig:LogicGraph}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{figure}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{center}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{tabular}{|l|c|c|c|}\hline
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\CASL & x & x & - \\\hline
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\CoCASL & x & x & - \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\ModalCASL & x & x & - \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\HasCASL & x & x & - \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiHaskell & x & x & -\\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\CspCASL & (x) & - & - \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiConstraint\CASL & x & (x) & - \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%Structured specifications & x & x & (x) \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%Architectural specifications & x & x & -\\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\CASLDL & x & - & - \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniOWL DL basic & x & (x) & - \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiOWL DL structure & x & (x) & - \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiPropositional & x & x & x \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiSoftFOL & - & - & x \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\Isabelle & - & - & x \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\begin{description}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\item[CASL] extends many sorted first-order logic with partial
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski functions and subsorting. It also provides induction sentences,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski expressing the (free) generation of datatypes.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%It is mainly designed and used for the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%specification of requirements for software systems. But it is also
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%used for the specification of \Dolce (Descriptive Ontology for
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%representation. \cite{Gangemi:2002:SOD} Further it is now used to
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%specify calculi for time and space.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiWe have implemented the \CASL logic in such a way that much of the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiimplementation can be re-used for \CASL extensions as well; this
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiis achieved via ``holes'' (realized via polymorphic variables) in the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskitypes for signatures, morphisms, abstract syntax etc. This eases
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiintegration of \CASL extensions and keeps the effort of integrating
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\CASL extensions quite moderate.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskisuited for the specification of process types and reactive systems.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe central proof method is coinduction.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\item[ModalCASL] \cite{ModalCASL}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski is an extension of \CASL with multi-modalities and
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiterm modalities. It allows the specification of modal systems with
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiKripke's possible worlds semantics. It is also possible to express
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskicertain forms of dynamic logic.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\item[HasCASL] is a higher order extension of \CASL allowing
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski polymorphic datatypes and functions. It is closely related to the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski programming language Haskell and allows program constructs being
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski embedded in the specification.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskithe language is summarized in \cite{HasCASL/Summary}, the semantics
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiin \cite{Schroder05b,Schroder-habil}.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\item[Haskell] is a modern, pure and strongly typed functional
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski programming language. It simultaneously is the implementation
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski language of \Hets, such that in the future, \Hets might be applied
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe definitive reference for Haskell is \cite{PeytonJones03},
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski with the process algebra CSP.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\item[ConstraintCASL] is an experimental logic for the specification
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiof qualitative constraint calculi.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski World Wide Web Consortium (W3C, \url{http://www.w3c.org}). It is
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski used for knowledge representation and the Semantic Web
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \cite{berners:2001:SWeb}.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiHets calls an external OWL DL parser
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski written in JAVA to obtain the abstract syntax for an OWL file and its
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski imports. The JAVA parser is also doing a first analysis classifying
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski Hets only supports the last two, more restricted variants.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski structuring of the OWL imports is displayed as Development Graph.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\item[CASL-DL] \cite{OWL-CASL-WADT2004}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiis an extension of a restriction of \CASL, realizing
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskia strongly typed variant of OWL DL in \CASL syntax.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \CASL with cardinality restrictions for the description of sorts and
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski unary predicates. The restrictions are based on the equivalence
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski and binary predicates, predefined datatypes and concepts (subsorts
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski of the topsort Thing) are allowed. It is used to bring OWL DL and
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski \CASL closer together.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\item[Propositional] is classical propositional logic, with
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskithe zChaff SAT solver \cite{Herbstritt03} connected to it.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski proving (ATP) systems for first-order logic with equality: (1) \SPASS
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski MathServe Broker\footnote{which chooses an appropriate ATP upon a
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski classification of the FOL problem} \cite{ZimmerAutexier06}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini These together comprise some of the most advanced theorem provers
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski for first-order logic.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski for higher-order logic.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\end{description}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiPropositional, SoftFOL and \Isabelle are currently the only logics
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskicoming with a prover. Proof support for the other logics can be
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskiobtained by using logic translations to a prover-supported logic.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiAn introduction to \CASL can be found in the \CASL User Manual
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\cite{CASL-UM}; the detailed language reference is given in
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskiexplain both the \CASL logic and language of basic specifications as
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskiwell as the logic-independent constructs for structured and
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskiarchitectural specifications. The corresponding document explaining the
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\HetCASL language constructs for \emph{heterogeneous} structured specifications
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskiis the \HetCASL language summary \cite{Mossakowski04}; a formal
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskisemantics as well as a user manual with more examples are in preparation.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiSome of \HetCASL's heterogeneous constructs will be illustrated
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskiin Sect.~\ref{sec:HetSpec} below.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\section{Logic translations supported
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\label{comorphisms}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiLogic translations (formalized as institution comorphisms
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\cite{GoguenRosu02}) translate from a given source logic to a given
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskitarget logic. More precisely, one and the same logic translation
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskimay have several source and target \emph{sub}logics: for
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskieach source sublogic, the corresponding sublogic of the target
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskilogic is indicated.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiA graph of the most important logics and sublogics, together with their
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskicomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\begin{figure}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski \begin{center}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski \includegraphics[scale=0.4]{SublogicGraph}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\caption{Graph of most important sublogics currently supported by \Hets,
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskitogether with their comorphisms.}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\label{fig:SublogicGraph}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiIn more detail, the following list of logic translations is currently
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskisupported by \Hets:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{tabular}{|l|p{5cm}|}\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniCASL2CoCASL & inclusion \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniCASL2CspCASL & inclusion \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCASL2HasCASL & inclusion \\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniCASL2Modal & inclusion \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniCASL2PCFOL & coding of subsorting by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual}\\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniCASL2SubCFOL & coding of partial functions by error elements
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting) \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniCASL2TopSort & coding of subsorting by a top sort and unary
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipredicates for the subsorts \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniCFOL2IsabelleHOL & coding of \CASL to Isabelle
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(translation $(7)$ of \cite{Mossakowski02}) \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiCoCFOL2IsabelleHOL & coding of \CoCASL to Isabelle, similar to CFOL2IsabelleHOL \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%CoPCFOL2CoCFOL & coding of partial functions by error elements,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%similar to PCFOL2CFOL \\\hline
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski%%CspCASL2IsabelleHOL & \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%%CspCASL2Modal & \\\hline
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiHasCASL2HasCASL & coding of \HasCASL axiomatic recursive definitions
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinias \HasCASL recursive program definitions \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHasCASL2IsabelleHOL & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell2IsabelleHOL & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07}\\\hline
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiModal2CASL & the standard translation of modal logic
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskito first-order logic \cite{blackburn_p-etal:2001a} \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%PCFOL2CFOL & coding of partial functions by error elements
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%(translation $(4a')$ of \cite{Mossakowski02}) \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniPCoClTyConsHOL2IsabelleHOL & coding of \HasCASL to Isabelle/HOL\\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniSuleCFOL2SoftFOL & coding of CASL to SoftFOL \cite{LuettichEA06a},
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinimapping types to soft types \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniSuleCFOL2SoftFOLIndcuction & dto., but with instances of induction
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniaxioms for all proof goals\\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniProp2CASL & inclusion \\\hline
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniProp2CNF & conversion of propositional formulas to conjunctive normal form\\\hline
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\section{Getting started}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe latest \Hets version can be obtained from the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\Hets tools home page
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski Since \Hets is being
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\Hets currently is available for Linux, Solaris and
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThere are three possibilities to install \Hets:
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\begin{enumerate}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe Java-based \Hets installer. Download a \texttt{.jar} file and
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskijava -jar \texttt{file.jar}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskidouble-click on the \texttt{.jar} file.
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiThe installer will lead you through the installation with
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskia graphical interface. It will download and install further
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskisoftware (if not already installed on your computer):
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\begin{tabular}{|l|l|l|}\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiCASL-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiTcl/Tk & graphics widget system & \url{http://www.scriptics.com/software/tcltk/} \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiIf you do not have Sun Java, you can just download the hets binary.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiYou have to unpack it with \texttt{bunzip2} and then put it at
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskisome place coverd by your \texttt{PATH}. You also have to
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiinstall the above mentioned software and set
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiseveral environment variables, as explained on the installation page.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiIf you want to compile \Hets from the sources, please follow the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskilink ``Hets: source code and information for developers''
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskion the \Hets web page, download the sources (as tarball or from
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskisvn), and follow the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiinstructions in the \texttt{INSTALL} file.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\end{enumerate}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\section{Analysis of Specifications}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiConsider the following \CASL
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskispecification:
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\begin{BIGEXAMPLE}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\I\SPEC \NAME{Strict\_Partial\_Order} =
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\begin{ITEMS}[\PRED]
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\I\SORT \( Elem \)
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski\(\[ \FORALL x,y,z : Elem \\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\begin{COMMENT}
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till MossakowskiNote that there may exist \(x, y\) such that\\
01bcb1d665a9e3d5aae8cc4c79dbe8991eed6d17Till Mossakowskineither \(x < y\) nor \(y < x\).
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\end{BIGEXAMPLE}
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\Hets can be used for parsing and
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskichecking static well-formedness of specifications.
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski \index{parsing}%
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski \index{static!analysis}%
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski \index{analysis, static}%
8241bc853cd629fb5c6299e6b8d5d546ee731343Till MossakowskiLet us assume that the example is in a file named
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\texttt{Order.casl} (actually, this file is provided
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskiwith the \Hets distribution).
8241bc853cd629fb5c6299e6b8d5d546ee731343Till MossakowskiThen you can check the well-formedness of the
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskispecification by typing (into some shell):
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\Hets checks both the correctness of this specification
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski with respect to the \CASL syntax, as
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskiwell as its correctness with respect to the static semantics (e.g.\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiwhether all identifiers have been declared before they are used,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiwhether operators are applied to arguments of the correct sorts,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiwhether the use of overloaded symbols is unambiguous, and so on).
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe following flags are available in this context:
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\begin{description}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing -- the static analysis
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski static analysis of (heterogeneous) structured specifications, but
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski leave out the analysis of basic specifications. This can be used
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski for prototyping issues, namely to quickly produce a development graph
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski showing the dependencies among the specifications (cf.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski Sect.~\ref{sec:DevGraph}) even if the individual specifications are
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski not correct yet.
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
8241bc853cd629fb5c6299e6b8d5d546ee731343Till MossakowskiUse \texttt{DIR} as the directory for specification libraries
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski(equivalently, you can set the variable \texttt{HETS\_LIB} before
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowskicalling \Hets).
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\item[\texttt{--casl-amalg=ANALYSIS}]
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski For the analysis of architectural specification (a quite advanced
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski amalgamability checking
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski algorithm for \CASL logic; it is a comma-separated list of zero or
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski more of the following options:
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski \begin{description}
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski \item[\texttt{sharing}] perform sharing analysis for sorts,
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski operations and predicates.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \item[\texttt{cell}] perform cell condition check; implies
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \texttt{sharing}. With this option on, the subsort embeddings are
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \item[\texttt{colimit-thinness}] perform colimit thinness check;
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski implies \texttt{sharing}. The colimit thinness check is less
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski complete and usually takes longer than the full cell condition
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski check (\texttt{cell} option), but may prove more efficient in case
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski of certain specifications.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \end{description}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski If \texttt{ANALYSIS} is empty then amalgamability analysis for
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \CASL is skipped.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski The default value for \texttt{--casl-amalg} is
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski \texttt{cell}.
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\end{description}
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\Hets accepts plain text input files with the following endings:\\
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\begin{tabular}{|l|c|c|}\hline
8241bc853cd629fb5c6299e6b8d5d546ee731343Till MossakowskiEnding & default logic & structuring language\\\hline
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\texttt{.hs} & Haskell & Haskell\\\hline
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiinterchangeable, the former should be used for libraries of
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiof heterogeneous specifications (that use the \CASL structuring
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskito \HasCASL in the following way:
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\begin{verbatim}
8241bc853cd629fb5c6299e6b8d5d546ee731343Till Mossakowski\end{verbatim}
8241bc853cd629fb5c6299e6b8d5d546ee731343Till MossakowskiThe subsequent specifications are then parsed and analysed as
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\HasCASL specifications. Within such specifications,
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiit is possible to use references to named \CASL specifications;
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskithese are then automatically translated along the default
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(There are also heterogeneous constructs
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor explicit translations between logics, see \cite{Mossakowski04}.)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniA \CspCASL specification consists of a \CASL specification
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinifor the data part and a \Csp process built over this data part.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniTherefore, \HetCASL provides a heterogeneous language construct
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\texttt{data} as follows:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{verbatim}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilibrary Buffer
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini free type List[Elem] ::= nil | cons(Elem; List[Elem])
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini ops last: List -> ? Elem;
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini rest: List -> ? List
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini channel read, write : Elem
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini process Buf(List): read, write, List;
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini EmptyBuffer : read,write, List;
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini Buf(l)= read? x :: Elem -> Buf(cons(x,nil)) []
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini (if l=nil then STOP else
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini write!last(l) -> Buf(rest(l)))
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini EmptyBuffer = Buf(nil)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{verbatim}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHere, the construct \texttt{data List} refers to the \CASL specification
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\texttt{List}, which is implicitly embedded into \CspCASL.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe ending \texttt{.hs} is available for directly reading in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHaskell programs % and HasSLe specifications,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniand hence supports the Haskell module system.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe logic Haskell has to be chosen explicitly, and the \CASL structuring
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinisyntax needs to be used:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{verbatim}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskilibrary Factorial
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinispec Factorial =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifac :: Int -> Int
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifac n = foldl (*) 1 [1..n]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{verbatim}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniNote that according to the Haskell syntax, Haskell function
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinideclarations and definitions need to start with the first column of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\section{Development Graphs}\label{sec:DevGraph}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniDevelopment graphs are a simple kernel formalism for (heterogeneous)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinistructured theorem proving and proof management.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniA development graph consists of a set of nodes (corresponding to whole
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinistructured specifications or parts thereof), and a set of arrows
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicalled \emph{definition links}, indicating the dependency of each
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniinvolved structured specification on its subparts. Each node is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniassociated with a signature and some set of local axioms. The axioms
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof other nodes are inherited via definition links. Definition links
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniare usually drawn as black solid arrows, denoting an import of another
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinispecification.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniComplementary to definition links, which \emph{define} the theories of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirelated nodes, \emph{theorem links} serve for \emph{postulating}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinirelations between different theories. Theorem links are the central
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidata structure to represent proof obligations arising in formal
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniTheorem links can be \emph{global} (drawn as solid arrows) or
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{local} (drawn as dashed arrows): a global theorem link
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinipostulates that all axioms of the source node (including the inherited
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniones) hold in the target node, while a local theorem link only postulates
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithat the local axioms of the source node hold in the target node.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniBoth definition and theorem links can be \emph{homogeneous},
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinii.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe logic changes along the arrow. Technically, this is the case
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifor Grothendieck signature morphisms $(\rho,\sigma)$ where
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini$\rho\not=id$. This case is indicated with double arrows.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniTheorem links are initially displayed in red.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe \emph{proof
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini calculus} for development graphs
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\cite{MossakowskiEtAl05,Habil} is given by rules
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithat allow for proving global theorem links by decomposing them
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniinto simpler (local and global) ones. Theorem links that have been
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniproved with this calculus are drawn in green. Local theorem links can
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinibe proved by turning them into \emph{local proof goals}. The latter
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinican be discharged using a logic-specific calculus as given by an
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinientailment system for a specific institution. Open local
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniproof goals are indicated by marking the corresponding node in the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidevelopment graph as red; if all local implications are proved, the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrininode is turned into green. This implementation ultimately is based
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinion a theorem \cite{Habil} stating soundness and relative completeness
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof the proof calculus for heterogeneous development graphs.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe following option lets \Hets show the development graph of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinia specification library:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window.\end{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniLet us extend the above library \texttt{Order.casl}. One use of the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilibrary might be to express the fact that the natural numbers form a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinistrict partial order as a view, as follows:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{BIGEXAMPLE}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{BIGEXAMPLE}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{EXAMPLE}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\IEXT{\NAMEREF{Natural}} \THEN
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\(\[ \FORALL x,y:Nat \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \. 0 < suc(x) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \. \neg x < 0 \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \. suc(x) < suc(y) \IFF x < y
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{EXAMPLE}%[\SLIDESMALL]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\NAMEREF{Natural\_Order\_2} =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\I{} \( Elem \MAPSTO Nat\)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAgain, these specifications can be checked with \Hets. However, this
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinionly checks syntactic and static semantic well-formedness -- it is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniby a strict partial ordering relation. Checking this requires theorem
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniproving, which will be discussed below.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniHowever, before coming to theorem proving, let us first inspect the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniproof obligations arising from a specification. This can be done with:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\texttt{hets -g Order.casl}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(assuming that the above two specifications and the view
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinihave been added to the file
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\Hets now displays a so-called development graph
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(which is just an overview graph showing the overall structure
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof the specifications in the library), see Fig.~\ref{fig:dg0}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{figure}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{center}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\includegraphics[scale=0.7]{dg-order-0}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\caption{Sample development graph.\label{fig:dg0}}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniNodes in a development graph correspond to \CASL specifications.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniArrows show how specifications are related by the structuring
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe black arrow denotes an ordinary import of
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinispecifications (generated by the extension), while the red arrow
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidenotes a proof obligation (corresponding to the view).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThis proof obligation needs to be discharged in order to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinishow that the view is well-formed (then its color turns into green).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAs a more complex example, consider the following loose specification
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof a sorting function, taken from the \CASL User Manual
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\cite{CASL-UM}, Chap.~6:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{BIGEXAMPLE}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\I\SPEC \NAMEREF{List\_Order\_Sorted}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{ITEMS}[\WITHIN]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{ITEMS}[\PRED]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\I\PRED \( \_\_is\_sorted : List \)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\(\[ \FORALL e,e': Elem; L : List \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \. empty~is\_sorted \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \. cons(e,empty)~is\_sorted \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \. cons(e,cons(e',L))~is\_sorted \IFF
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{ITEMS}[\OP]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\I\OP \( order : List \TOTAL List \)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{BIGEXAMPLE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe following specification of sorting by insertion also is taken from
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe \CASL User Manual \cite{CASL-UM}, Chap.~6:
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{BIGEXAMPLE}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\SPEC \NAMEREF{List\_Order}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\phantomsection
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\begin{ITEMS}[\WITHIN]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{ITEMS}[\OP]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\I\OP \( insert : Elem \* List \TOTAL List \)
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\(\[ \FORALL e,e':Elem; L:List \\
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \ELSE cons(e, cons(e',L)) \] \\
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{ITEMS}[\OP]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\I\OP \( order : List \TOTAL List \)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\(\[ \FORALL e:Elem; L:List \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \. order(empty) = empty \\
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini \. order(cons(e,L)) = insert(e, order(L)) \]\)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{BIGEXAMPLE}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniBoth specifications are related. To see this, we first inspect
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitheir signatures. This is possible with:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\texttt{hets -g Sorting.casl}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniassuming that \texttt{Sorting.casl} contains the above specifications.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{figure}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{center}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\includegraphics[scale=0.7]{dg-order-1}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIn the above-mentioned development graph, we have two types of nodes.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe named ones correspond to named specifications, but there
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniare also unnamed nodes corresponding to anonymous basic
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinispecifications like the declaration of the $insert$ operation in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\NAMEREF{List\_Order} above. Basically, there is an
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniunnamed node for each structured specification that is not named.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAgain, the black arrows denote an ordinary import of specifications
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(corresponding to the extensions and unions in the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskispecifications), while the blue arrows denote hiding (corresponding to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe local specification).
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniBy clicking on the nodes, one can inspect their signatures.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\NAMEREF{List\_Order} have the same signature. Hence, it
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniis legal to add a view:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{EXAMPLE}%[\SLIDESMALL]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniWe have already added this view to \texttt{Sorting.casl}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe corresponding
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniproof obligation between \NAMEREF{List\_Order\_Sorted} and
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini as a red arrow.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHere is a summary of the types of nodes and links occurring in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinidevelopment graphs:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Named nodes] correspond to a named specification.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Unnamed nodes] correspond to an anonymous specification.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Elliptic nodes] correspond to a specification in the current library.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Rectangular nodes] are external nodes corresponding
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini to a specification downloaded from
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinianother library.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Red nodes] have open proof obligations.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Green nodes] have all proof obligations resolved.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Black links] correspond to reference to other specifications
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Blue links] correspond to hiding (hiding definition links).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Red links] correspond to open proof obligations (theorem links).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Green links] correspond to proved proof obligations (theorem links).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Yellow links] correspond to open proof obligations involving hiding (hiding theorem links).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Solid links] correspond to global (definition or theorem)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilinks in the sense of \cite[IV:4]{CASL/RefManual}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Single links] have homogeneous signature morphisms (staying within
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinione and the same logic).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Double links] have heterogeneous signature morphisms (moving between
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniWe now explain the menus of the development graph window.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniMost of the pull-down menus of the window are uDraw(Graph)-specific
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinitheir function can be looked up in the uDraw(Graph) documentation\footnote{see
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe exception is the Edit menu. Moreover, the nodes and links
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof the graph have attached pop-up menus, which appear when
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniclicking with the right mouse button.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Edit] This menu has the following submenus:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[undo] Undo the last development graph proof step (see under Proofs)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[redo] Restore the last undone development graph proof step (see
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini under Proofs)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[reload] Reload the specification library (Attention! all proofs are lost. A change management keep proofs is in preparation.)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Unnamed nodes]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe ``Hide/show names'' menu is a toggle:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniyou can switch on or off the display of names for nodes that
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniare initially unnamed. The newly named nodes get names that
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniare derived from named neighbour nodes.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniWith the ``Hide nodes'' submenu, it is possible
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinito reduce the complexity of the graph by hiding all unnamed nodes;
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinionly nodes corresponding to named specifications remain displayed.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniPaths between named nodes going through unnamed nodes
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniare displayed as links. With the ``Show nodes'' submenu, the unnamed
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrininodes re-appear.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Proofs] This menu allows to apply some of the deduction rules
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini for development graphs, see Sect. IV:4.4 of the \CASL Reference
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Manual \cite{CASL/RefManual} or one of
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}. While support for
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini local and global (definition or theorem) links is stable, support
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini for hiding links and checking conservativity is still experimental.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini In most cases, it is advisable to use ``Automatic'', which
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini automatically applies the rules in the correct order. As a result,
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini the the open theorem links (marked in red) will be reduced to local
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini proof goals, that is, they become green, and instead, some of the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini node will get red, indicating open local proof goals.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini Besides the deduction rules, the menu contains entries for computing
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini a colimit approximation for the development graph and for
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini computing normal forms of all nodes (needed when dealing with hiding).
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Translate Graph] translates the whole development graph
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinialong a logic comorphism.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Show Logic Graph] shows the graph of logics and logic comorphisms
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinicurrently supported by \Hets.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show Library Graph] shows the graph of libraries that have
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinibeen loaded into \Hets, and their dependencies. For library,
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe corresponding development graphs can be shown using its node menu.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniAlso, a list of specifications and views can be shown.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{description}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Pop-up menu for nodes]
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniHere, the number of submenus depends on the type of the node:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Show signature] Shows the signature of the node.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Show local axioms] Shows the local axioms of the node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show theory] Shows the theory of the node (including axioms
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniimported from other nodes). Warning: axioms imported via hiding links
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniare not part of the theory; they can be made visible only by re-adding
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe hidden symbols, using the proof rule \emph{Theorem-Hide-Shift}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Translate theory] Translates the theory of a node to another logic.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniA menu with the possible translation paths will be displayed.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph of the signature of the node.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinifor the signature and the axioms of the node.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Show origin] Shows the kind of \CASL structuring construct that
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniled to the node.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Show proof status] Show open and proven local proof goals.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Check consistency] Check the consistency of the theory of the node.
c60dd75d214d1b29462ee2262d4e0f468a962450Paolo Torrini\item[Show just subtree] (Only for named nodes) Reduce the complexity
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof the graph by just showing the subtree below the current node.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Undo show just subtree] (Only for named nodes) Undo the reduction.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Show referenced library] (Only for external nodes) Open a new window
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinishowing the development graph for the library the external node refers to.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini%\item[Show spec] Show the structured specification of the node.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini% (not fully implemented yet)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Show number of node] Show the internal number of the node.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Pop-up menu for links]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniAgain, the number of submenus depends on the type of the link:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Show morphism] Shows the signature morphism of the link. It consists
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof two components: a logic translation and a signature morphism in the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitarget logic of the logic translation.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniIn the (most frequent) case
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniof an intra-logic signature morphism, the logic translation component is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinijust the identity.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Show origin] Shows the kind of \CASL structuring construct that
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniled to the link.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Show proof status] (Only for theorem links) Show the proof status.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\item[Check conservativity] (Experimental) Check whether the
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinitheory of the target node of the link
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniis a conservative extension of the theory of the source node.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[Show ID of this edge] Shows the internal number of the edge.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThese numbers are also used in the proof status information for
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\section{Reading, Writing and Formatting}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\Hets provides several options controlling the types of files
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithat are read and written.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{description}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\texttt{ITYPE} as the type of the input file. The default is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\texttt{het} (\HetCASL plain text). \texttt{ast} is for reading
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniin abstract syntax trees in ATerm format, while \texttt{ast.baf}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinireads in the compressed ATerm format.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe possible input types are:
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{verbatim}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini (casl|het|owl|hs|prf|omdoc|hpf|[tree.]gen_trm[.baf])
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrini\end{verbatim}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniSpecify \texttt{DIR} as destination directory for output files.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\texttt{OTYPES} is a comma separated list of output types:
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\begin{verbatim}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini | (sig|th)[.delta]
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini | pp.(het|tex)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini | graph.(exp.dot|dot)
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\end{verbatim}
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniThe default is \texttt{prf} (a synonym for \texttt{dg.taf}), which
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimeans that the development graph of the library is stored in textual
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniATerm format (\texttt{taf}). This format can be read in when a
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinilibrary is downloaded from another library, avoiding the need to
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinire-analyse the downloaded library. You can also directly read in
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinithe \texttt{prf} format (both from the command line, by calling
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\Hets on the \texttt{prf} file, and from the GUI, using the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniFile-Open menu.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe \texttt{env} format is currently not used.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinimarkup format and data model for Open Mathematical Documents. It
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torriniserves as semantics-oriented representation format and ontology
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinilanguage for mathematical knowledge. Currently, \CASL specifications
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinican be output in this format; support for further logics is planned.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe \texttt{hs} format is used for Haskell modules. Executable \CASL or
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\HasCASL specifications can be translated to Haskell.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniWhen the \texttt{thy} format is selected, \Hets will try to translate
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinieach specification in the library to \Isabelle, and write one \Isabelle
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrini\texttt{.thy} file per specification.
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo TorriniWhen the \texttt{comptable.xml} format is selected, \Hets will extract
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinithe composition and inverse table of a Tarskian relation algebra from
278efe81d7d9f2e475e76c74c0db8622ccef99ebPaolo Torrinispecification(s) (selected with the \texttt{-n} or \texttt{--spec}
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinioption). It is assumed that the relation algebra is
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinigenerated by basic relations, and that the specification is written
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniin the \CASL logic. A sample specification of a relation
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torrinialgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo Torriniavailable from \texttt{www.cofi.info/Libraries}.
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe output format is XML, the URL of the DTD is included in the
7e80cfe2052409faa4ff745448c2f5ec8dd909f9Paolo TorriniThe \texttt{pp} format is for pretty printing, either as plain text
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski(\texttt{het}), \LaTeX input (\texttt{tex}) or HTML (\texttt{html}).
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiA formatter with pretty-printed output currently is available only for
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskithe \CASL logic. For example, it is possible to generate a pretty
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiprinted \LaTeX\ version of \texttt{Order.casl} by typing:
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThis will generate a file \texttt{Order.pp.tex}. It can be included
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskicoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe \texttt{dfg} format is used by the \SPASS theorem prover
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\cite{WeidenbachEtAl02}.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiformat for first-order theorem provers.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskichooses a translation option. \texttt{TRANS} is a colon-separated list
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiwithout blanks of one or more comorphism names (see Sect.~\ref{comorphisms}).
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item[\texttt{-R}, \texttt{--recursive}] output also imported libraries.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe other output formats are for future usage.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\end{description}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\section{Miscellaneous Options}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{description}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiSet the verbosity level according to \texttt{Int}. Default is 1.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item[\texttt{-q}, \texttt{--quiet}]
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiBe quiet -- no diagnostic output at all. Overrides -v.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiPrint usage information and exit.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski \texttt{Int} megabytes (needed in case of a stack overflow).
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThis must be the first option.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskideclaration. The default is \CASL.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskichooses a list of named specifications for processing
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\item[\texttt{-I}, \texttt{--interactive}] run \Hets in interactive mode
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\end{description}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\section{Proofs with \Hets}\label{sec:Proofs}
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe proof calculus for development graphs (Sect.~\ref{sec:DevGraph})
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskireduces global theorem links to local proof goals. Local proof goals
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski(indicated by red nodes in the development graph) can be eventually
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskidischarged using a theorem prover, using the ``Prove'' menu of a red node.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe graphical user interface (GUI) for calling a prover is shown in
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiFig. \ref{fig:proof_window} --- we call it ``Proof Management GUI''.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe list on the left shows all goal names prefixed with the proof
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskistatus in square brackets. A proved goal is indicated by a `+', a `-'
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiindicates a disproved goal, a space denotes an open goal, and a
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski`$\times$' denotes an inconsistent specification (aka a fallen `+';
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskisee below for details).
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{figure}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\includegraphics[width=\textwidth]{proofmanagement1}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\caption{Hets Goal and Prover Interface\label{fig:proof_window}}
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiIf you open this GUI when processing the goals of one node for the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskifirst time, it will show all goals as open. Within this list you can
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiselect those goals that should be inspected or proved. The button
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski`Display' shows the selected goals in the ASCII syntax of this
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitheory's logic in a separate window. With the `Prove' button the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiactual prover is launched. This is described in more detail in the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiparagraphs below. By pressing the `Show Proof Details' button a window
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiis opened where for each proved goal the used axioms, its proof
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiscript, and its proof are shown --- the level of detail depends on the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiused theorem prover. The `Status:' shows either `No prover running' or
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski`Waiting for prover' in black or blue. If you press the `Close' button
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskithe window is closed and the status of the goals' list is integrated
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiinto the development graph. If all goals have been proved, the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiselected node turns from red into green.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe list `Pick Theorem Prover:' lets you choose one of the connected
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiprovers (currently, these are \Isabelle, MathServe Broker, \SPASS,
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiVampire, and zChaff, described below). By pressing `Prove' the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiselected prover is launched and the theory along with the selected
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskigoals is translated via the shortest possible path of comorphisms into
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskithe provers logic. The button `More fine grained selection...' lets
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiyou pick a (composed) comorphism in a separate window from where the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiprover is launched then.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiSince the amount and kind of sentences sent to an ATP system is a
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskimajor factor for the performance of the ATP system, it is possible to
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiselect the axioms and proven theorems that will comprise the theory
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiof the next proof attempt. Based on this selection the sublogic may
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskivary and also the available provers and comorphisms to provers. Former
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskitheorems that are imported from other specifications are marked with
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskithe prefix `(Th)'. Since former theorems do not add additional logical
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskicontent, they may be safely removed from the theory.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\subsection[Automated Theorem Proving Systems]
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski{Automated Theorem Proving Systems\\(Logic SoftFOL)}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\label{sec:ATP}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{figure}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\includegraphics[width=\textwidth]{spassGUI1}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiAll ATPs integrated into \Hets share the same GUI, with only a slight
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskimodification for the MathServe Broker: it does not have input
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskifields for extra options. Figure~\ref{fig:SPASS_GUI} shows the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiinstantiation for \SPASS, where in the lower part of the window the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskibatch mode can be controlled. The upper part shows on the left the
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskilist of goals (with the same status indicators as in the Proof
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiManagement GUI), and on the right a proof attempt of the selected goal
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiis controlled and the result of the last proof attempt is displayed.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe status line indicates `Open', `Running', `Proved', `Disproved',
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski`Open (Time is up!)', and `Proved (Theory inconsistent!)'. The list of
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiused axioms is actually only filled by \SPASS. The help button displays
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiinformation about the extra options accepted by the ATP system. The
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskibutton `Show Details' shows the whole output of the ATP system. `Save
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiProver Configuration' allows you to save the configuration and status
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiof each proof for documentation. By pressing the button `Exit Prover'
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskithe status of these proofs and goals is transferred back to the
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiProof Management GUI.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiThe MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiZimmer provides a unified interface to a range of different ATP
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskisystems; the most important systems are listed in
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiTable~\ref{tab:MathServe}, along with their capabilities. These
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskicapabilities are derived from the \emph{Specialist Problem Classes}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski(SPCs) defined upon the basis of logical, language and syntactical
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiproperties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
846fb262bddd024972b6d4820762bd85ebe0f352Till MossakowskiOnly two of the Web services provided by the MathServe system are used
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiby \Hets currently: Vampire and the brokering system. The ATP systems
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiare offered as Web Services using standardized protocols and formats
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskisuch as SOAP, HTTP and XML. Currently, the ATP system Vampire may be
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiaccessed from \Hets via MathServe; the other systems are only reached
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowskiafter brokering.
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski\begin{table}[t]
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski \begin{threeparttable}
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski \begin{tabular}{|l|c|p{7cm}|}\firsthline
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski ATP System & Version & Suitable Problem Classes\tnote{a}\\
846fb262bddd024972b6d4820762bd85ebe0f352Till Mossakowski \hhline{|=|=|=|}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski DCTP & 10.21p & effectively propositional \\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski EP & 0.91 & effectively propositional; real first-order, no
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski equality; real first-order, equality\\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski Otter & 3.3 & real first-order, no equality\\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \SPASS & 2.2 & effectively propositional; real first-order, no
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski equality; real first-order, equality\\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski Vampire & 8.0 & effectively propositional; pure equality, equality
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski clauses contain non-unit equality clauses; real first-order, no
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski equality, non-Horn\\\hline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski Waldmeister & 704 & pure equality, equality clauses are unit
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski equality clauses\\\lasthline
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \end{tabular}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski %\renewcommand{\thempfootnote}{\arabic{mpfootnote}}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski %\footnotetext%[\value{footnote}\stepcounter{footnote}]
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \begin{tablenotes}\footnotesize
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski {The list of problem classes for each ATP system is not
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski exhaustive, but only the most appropriate problem classes are
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski named according to benchmark tests made with MathServe by
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski J\"urgen Zimmer.}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \end{tablenotes}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \end{threeparttable}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \caption{ATP systems provided as Web services by MathServe}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\vspace*{-4mm}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski \label{tab:MathServe}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\subsubsection*{\SPASS}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe ATP system \SPASS \cite{WeidenbachEtAl02} is a resolution-based
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiprover for first-order logic with equality. Furthermore, it provides a soft
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskityping mechanism with subsorting that treats sorts as unary
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskipredicates. The ATP \SPASS should be installed locally and available
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskithrough your \verb,$PATH, environment variable.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\subsubsection*{Vampire}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe ATP system Vampire is the winner of the last 5 CADE ATP System
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiCompetitions (CASC) (2002--2006) in the devisions \verb,FOF, and
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\verb,CNF,. It is a resolution based ATP system supporting the calculi
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiof ordered binary resolution and superposition for handling equality.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\url{http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskifor detailed information. The connection to Vampire is achieved by
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiusing an Web service of the MathServe system.
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\subsubsection*{MathServe Broker}
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% The classes ``effectively propositional'' and ``real first-order''
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% apply to first-order problems that are distinguished by the finiteness
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% of the Herbrand universe; an effectively propositional problem has
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% only constants (generated by finitely many terms) whereas a real
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski% first-order problem contains true functions with an infinite Herbrand
6a4b188beb6b1e3bd94867074c27995a01f529c2Till MossakowskiThe brokering service chooses the most appropriate ATP system
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskiupon a classification based on the SPCs, and on a training with the
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowskilibrary Thousands of Problems for Theorem Provers (TPTP)
6a4b188beb6b1e3bd94867074c27995a01f529c2Till Mossakowski\cite{ZimmerAutexier06}. The TPTP format
\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
The \Isabelle theory file conforms to the Isabelle/Isar syntax
version, where e.g.\ error handling is ignored. For technical reasons
the static analysis of basic specifications) and/or translates (along
of the \Hets home page at \url{http://www.dfki.de/sks/hets}.
%\input{hets.tex}