UserGuide.tex revision 1e276df94eadfeab45099f4482f76a9958bedb9c
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage[show]{ed} % set to hide for producing a released version
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{alltt}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{color}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{url}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{threeparttable,hhline}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage[pdfborder=0 0 0,bookmarks,
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskipdfauthor={Till Mossakowski, Christian Maeder, Mihai Codescu},
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichpdftitle={Hets User Guide}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich{hyperref} %% do not load more packages after this line!!
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\QUERY}[1]%{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\eat}[1]{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\IEXT}[1] {\\#1\I}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\IEND} {\I\END}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{EXAMPLEFORMAT} {}{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%% Added by MB to have some extra vertical space after the ``main'' examples
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%% following the points (and some others in the text):
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{DETAILSFORMAT} {}{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \begin{minipage}{0.9\textwidth}\it}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {\end{minipage}\par\medskip}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\SLIDESMALL} {}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\SLIDESONLY}[1] {}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% SIMULATING SMALL-CAPS FOR BOLD, EMPH
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\newcommand {\CoFI}{CoFI\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%%%% Klaus macros
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\newcommand{\SROIQ}{$\mathcal{SROIQ}$(\textbf{D})\xspace}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\newcommand{\DL}{DL\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%%%% end of Klaus macros
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LCF}{LCF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\ASF}{ASF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SDF}{SDF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CCC}{CCC\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{document}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\title{{\bf \protect{\LARGEHets} User Guide}\\
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder-- Version 0.95 --}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\author{Till Mossakowski, Christian Maeder, Klaus L\"{u}ttich\\[1em]
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederDFKI Lab Bremen, Bremen, Germany.\\[1em]
d78a2b8c5a63f3e63393e5cc44a5e9b253ac459bChristian MaederComments to: hets-users@informatik.uni-bremen.de \\
464c78620a182d2e8fbd125098045eae8788e2bdTill Mossakowski(the latter needs subscription to the mailing list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Introduction}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe central idea of the Heterogeneous Tool Set (\protect\Hets) is to
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiprovide a general framework for formal methods integration and proof
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskimanagement. One can think of \Hets acting like a motherboard where
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskidifferent expansion cards can be plugged in, the expansion cards here
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskibeing individual logics (with their analysis and proof tools) as well
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskias logic translations. Individual logics and their analysis and proof
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskitools can be plugged into the \Hets motherboard using an
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiobject-oriented interface based on institutions
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\cite{GoguenBurstall92}. The \Hets motherboard already has plugged in
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskia number of expansion cards (e.g., the theorem provers Isabelle, SPASS
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiand more, as well as model finders). Hence, a variety of tools is
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiavailable, without the need to hard-wire each tool to the logic at
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{figure}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{center}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \includegraphics[width=0.45\textwidth]{hets-motherboard}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\caption{The \Hets motherboard and some expansion cards}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\Hets supports a number of input languages directly, such as \CASL,
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiCommon Logic, OWL-DL, Haskell, and Maude. For heterogeneous
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskispecification, \Hets offers language heterogeneous \CASL.
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederHeterogeneous \CASL (\HetCASL) generalises the structuring
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\CASL \cite{CASL-UM,CASL/RefManual} to arbitrary logics
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski(if they are formalised as institutions and plugged into
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskithe \Hets motherboard), as well as to heterogeneous
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskicombination of specification written in different logics.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiFig.~\ref{fig:lang} for a simple subset of the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\HetCASL syntax, where \emph{basic specifications} are unstructured
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskispecifications or modules written in a specific logic. The graph of
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskicurrently supported logics and logic translations (the latter are also
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskicalled comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskidegree of support by \Hets in Fig.~\ref{fig:Languages}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{figure}[ht]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{verbatim}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiSPEC ::= BASIC-SPEC
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | SPEC then SPEC
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | SPEC then %implies SPEC
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | SPEC with SYMBOL-MAP
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | SPEC with logic ID
30256573a343132354b122097b0ee1215dda1364Till MossakowskiDEFINITION ::= logic ID
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | spec ID = SPEC end
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | view ID : SPEC to SPEC = SYMBOL-MAP end
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | view ID : SPEC to SPEC = with logic ID end
30256573a343132354b122097b0ee1215dda1364Till MossakowskiLIBRARY = DEFINITION*
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{verbatim}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\caption{Syntax of a simple subset of the heterogeneous
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederspecification language.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispecific syntax, while \texttt{ID} stands for some form of
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiidentifiers.\label{fig:lang}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiWith \emph{heterogeneous structured specifications}, it is possible to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicombine and rename specifications, hide parts thereof, and also
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprescribe the structure of implementations. \emph{Specification
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski libraries} are collections of named structured and architectural
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets consists of logic-specific tools for the parsing and static
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskianalysis of the different involved logics, as well as a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic-independent parsing and static analysis tool for structured and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito call the logic-specific tools whenever a basic specification is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets is based on the theory of institutions \cite{GoguenBurstall92},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiwhich formalize the notion of a logic. The theory behind \Hets is laid
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiout in \cite{Habil}. A short overview of \Hets is given in
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\cite{MossakowskiEA06,MossakowskiEtAl07b}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Logics supported by Hets}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe following list of logics (formalized as so-called institutions
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\cite{GoguenBurstall92}) is currently supported by \Hets:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \includegraphics[scale=0.4]{LogicGraph}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\caption{Graph of logics currently supported by \Hets. The more an
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\label{fig:LogicGraph}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{figure}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{tabular}{|l|c|c|c|}\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\CASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CoCASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\ModalCASL & x & x & - \\\hline
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\HasCASL & x & x & - \\\hline
881ab7022a03f9a6fa697d3067d05d61844929cbChristian MaederHaskell & (x) & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\CspCASL & x & x & - \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\CspCASL\_Trace & - & - & x \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\CspCASL\_Failure & - & - & - \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederConstraint\CASL & x & (x) & - \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederTemporal & x & (x) & - \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiRelScheme & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederDFOL & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederExtModal & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederLF & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder%Structured specifications & x & x & (x) \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder%Architectural specifications & x & x & -\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASLDL & x & - & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiDMU & x & - & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiOWL DL & x & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederPropositional & x & x & x \\\hline
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst SchulzSoftFOL & x & - & x \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederMaude & x & x & - \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiVSE & x & x & x \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\Isabelle & (x) & - & x \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maeder\begin{description}
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz\item[CASL] extends many sorted first-order logic with partial
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski functions and subsorting. It also provides induction sentences,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski expressing the (free) generation of datatypes.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%It is mainly designed and used for the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%specification of requirements for software systems. But it is also
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%used for the specification of \Dolce (Descriptive Ontology for
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%representation. \cite{Gangemi:2002:SOD} Further it is now used to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%specify calculi for time and space.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiWe have implemented the \CASL logic in such a way that much of the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiimplementation can be re-used for \CASL extensions as well; this
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiis achieved via ``holes'' (realized via polymorphic variables) in the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitypes for signatures, morphisms, abstract syntax etc. This eases
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiintegration of \CASL extensions and keeps the effort of integrating
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\CASL extensions quite moderate.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskisuited for the specification of process types and reactive systems.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe central proof method is coinduction.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[ModalCASL] \cite{ModalCASL}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski is an extension of \CASL with multi-modalities and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiterm modalities. It allows the specification of modal systems with
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiKripke's possible worlds semantics. It is also possible to express
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicertain forms of dynamic logic.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[HasCASL] is a higher order extension of \CASL allowing
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski polymorphic datatypes and functions. It is closely related to the
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski programming language Haskell and allows program constructs being
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski embedded in the specification.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe language is summarized in \cite{HasCASL/Summary}, the semantics
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederin \cite{Schroder05b,Schroder-habil}.
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu\item[Haskell] is a modern, pure and strongly typed functional
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu programming language. It simultaneously is the implementation
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski language of \Hets, such that in the future, \Hets might be applied
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe definitive reference for Haskell is \cite{PeytonJones03},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski with the process algebra CSP.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[ConstraintCASL] is an experimental logic for the specification
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiof qualitative constraint calculi.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski World Wide Web Consortium (W3C, \url{http://www.w3c.org}). It is
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder used for knowledge representation and the Semantic Web
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \cite{berners:2001:SWeb}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHets calls an external OWL DL parser
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder written in JAVA to obtain the abstract syntax for an OWL file and its
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder imports. The JAVA parser is also doing a first analysis classifying
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Hets only supports the last two, more restricted variants.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski structuring of the OWL imports is displayed as Development Graph.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[CASL-DL] \cite{OWL-CASL-WADT2004}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiis an extension of a restriction of \CASL, realizing
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedera strongly typed variant of OWL DL in \CASL syntax.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \CASL with cardinality restrictions for the description of sorts and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski unary predicates. The restrictions are based on the equivalence
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder and binary predicates, predefined datatypes and concepts (subsorts
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder of the topsort Thing) are allowed. It is used to bring OWL DL and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \CASL closer together.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Propositional] is classical propositional logic, with
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe zChaff SAT solver \cite{Herbstritt03} connected to it.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski proving (ATP) systems for first-order logic with equality: (1) \SPASS
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski MathServe Broker\footnote{which chooses an appropriate ATP upon a
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski classification of the FOL problem} \cite{ZimmerAutexier06}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski These together comprise some of the most advanced theorem provers
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski for first-order logic.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
30256573a343132354b122097b0ee1215dda1364Till Mossakowski for higher-order logic.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{description}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\ednote{TODO Till: update list}
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederVarious logics are supported with proof tools. Proof support for the
533d6033bec94a46d13b73cafe40953f699757c7Christian Maederother logics can be obtained by using logic translations to a
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescuprover-supported logic.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichAn introduction to \CASL can be found in the \CASL User Manual
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\cite{CASL-UM}; the detailed language reference is given in
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettichthe \CASL Reference Manual \cite{CASL/RefManual}. These documents
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiexplain both the \CASL logic and language of basic specifications as
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiwell as the logic-independent constructs for structured and
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiarchitectural specifications. The corresponding document explaining the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\HetCASL language constructs for \emph{heterogeneous} structured specifications
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichis the \HetCASL language summary \cite{Mossakowski04}; a formal
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsemantics as well as a user manual with more examples are in preparation.
c57bde4abc9029546fa396c4eccacf969e126b96Mihai CodescuSome of \HetCASL's heterogeneous constructs will be illustrated
533d6033bec94a46d13b73cafe40953f699757c7Christian Maederin Sect.~\ref{sec:HetSpec} below.
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\section{Logic translations supported
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\label{comorphisms}
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederLogic translations (formalized as institution comorphisms
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\cite{GoguenRosu02}) translate from a given source logic to a given
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescutarget logic. More precisely, one and the same logic translation
6eb84b5a2295c866c59905963b9342bc120b75ebEwaryst Schulzmay have several source and target \emph{sub}logics: for
9db773679fcc0a65c04b99f5699d3db382b6be7aEwaryst Schulzeach source sublogic, the corresponding sublogic of the target
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzlogic is indicated.
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederA graph of the most important logics and sublogics, together with their
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maedercomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder\begin{figure}
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder \begin{center}
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu \includegraphics[scale=0.4]{SublogicGraph}
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu\caption{Graph of most important sublogics currently supported by \Hets,
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescutogether with their comorphisms.}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\label{fig:SublogicGraph}
de55550f7d117195f127481d18ec2d5e8d2317ffMihai CodescuIn more detail, the following list of logic translations is currently
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maedersupported by \Hets:
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\ednote{TODO Mihai,Till: check VSE, Maude, DFOL descr. or ref.}
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu\begin{tabular}{|l|p{8cm}|}\hline
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian MaederCASL2CoCASL & inclusion \\\hline
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian MaederCASL2CspCASL & inclusion \\\hline
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian MaederCASL2HasCASL & inclusion \\\hline
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian MaederCASL2Isabelle & inclusion on sublogic CFOL=
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu(translation $(7)$ of \cite{Mossakowski02}) \\\hline
4317329b15d986d363c78acf8e4b330f33cccf9dChristian MaederCASL2Modal & inclusion \\\hline
4317329b15d986d363c78acf8e4b330f33cccf9dChristian MaederCASL2PCFOL & coding of subsorting (SubPCFOL=) by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual} \\\hline
4317329b15d986d363c78acf8e4b330f33cccf9dChristian MaederCASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzpredicates for the subsorts \\\hline
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst SchulzCASL2Propositional & translation of propositional FOL \\\hline
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst SchulzCASL2SoftFOL & coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzmapping types to soft types \\\hline
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst SchulzCASL2SoftFOLInduction & same as CASL2SoftFOL but with instances of induction
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzaxioms for all proof goals \\\hline
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst SchulzCASL2SubCFOL & coding of partial functions by error elements
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting, i.e. sublogic SubPCFOL=) \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiCASL2VSE & inclusion on sublogic CFOL= \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiCASL2VSEImport & inclusion on sublogic CFOL= \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiCASL2VSERefine & refining translation of CASL.CFOL= to VSE \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiCASL\_DL2CASL & inclusion \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCoCASL2Isabelle & extended translation similar to CASL2Isabelle \\\hline
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill MossakowskiCspCASL2CspCASL\_Failure & inclusion \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCspCASL2CspCASL\_Trace & inclusion \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCspCASL2Modal & translating the CASL data part to ModalCASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDFOL2CASL & translating dependent types \\\hline
30256573a343132354b122097b0ee1215dda1364Till MossakowskiDMU2OWL & interpreting Catia output as OWL \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{tabular}{|l|p{7cm}|}\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederHasCASL2HasCASLNoSubtypes & coding out subtypes \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHasCASL2HasCASLPrograms & coding of \HasCASL axiomatic recursive definitions
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskias \HasCASL recursive program definitions \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHasCASL2IsabelleOption & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHaskell2Isabelle & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07} \\\hline
30256573a343132354b122097b0ee1215dda1364Till MossakowskiMaude2CASL & inclusion \\\hline
30256573a343132354b122097b0ee1215dda1364Till MossakowskiModal2CASL & the standard translation of modal logic
30256573a343132354b122097b0ee1215dda1364Till Mossakowskito first-order logic \cite{blackburn_p-etal:2001a} \\\hline
30256573a343132354b122097b0ee1215dda1364Till MossakowskiOWL2CASL & inclusion \\\hline
30256573a343132354b122097b0ee1215dda1364Till MossakowskiPropositional2CASL & inclusion \\\hline
30256573a343132354b122097b0ee1215dda1364Till MossakowskiRelScheme2CASL & inclusion \\\hline
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\section{Getting started}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe latest \Hets version can be obtained from the
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\Hets tools home page
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Since \Hets is being
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\Hets currently is available (on Intel architectures only) for Linux, Solaris
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederThere are three possibilities to install \Hets:
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\begin{enumerate}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe Java-based \Hets installer. Download a \texttt{.jar} file and
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederjava -jar \texttt{file.jar}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederdouble-click on the \texttt{.jar} file.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederThe installer will lead you through the installation with
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maedera graphical interface. It will download and install further
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maedersoftware (if not already installed on your computer):
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\begin{tabular}{|l|l|p{5cm}|}\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederTcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederDarwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederIf you do not have Sun Java, you can just download the hets binary.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederYou have to unpack it with \texttt{bunzip2} and then put it at
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maedersome place coverd by your \texttt{PATH}. You also have to
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederinstall the above mentioned software and set
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederseveral environment variables, as explained on the installation page.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederYou may compile \Hets from the sources, please follow the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskilink ``Hets: source code and information for developers''
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederon the \Hets web page, download the sources (as tarball or from
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maedersvn), and follow the
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederinstructions in the \texttt{INSTALL} file, but be prepared to take some time.
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\end{enumerate}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiDepending on your application further tools are supported and may be
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiinstalled in addition:
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\begin{tabular}{|l|l|p{5cm}|}\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederzChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederminisat & SAT solver & \url{http://minisat.se/} \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiPellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiE-KRHyper & theorem prover
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederReduce & computer algebra system
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \url{http://www.reduce-algebra.com/} \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiVSE & theorem prover & (non-public) \\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichTwelf & & \url{http://twelf.plparty.org/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\ednote{TODO Mihai, Till, Luecke: check prover list}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\section{Analysis of Specifications}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiConsider the following \CASL
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maederspecification:
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\begin{BIGEXAMPLE}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\I\SPEC \NAME{Strict\_Partial\_Order} =
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\begin{ITEMS}[\PRED]
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\I\SORT \( Elem \)
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder% \COMMENTENDLINE{\PRED abbreviates predicate}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\(\[ \FORALL x,y,z : Elem \\
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\begin{COMMENT}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian MaederNote that there may exist \(x, y\) such that\\
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maederneither \(x < y\) nor \(y < x\).
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\end{BIGEXAMPLE}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\Hets can be used for parsing and
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maederchecking static well-formedness of specifications.
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder \index{parsing}%
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski \index{static!analysis}%
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski \index{analysis, static}%
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiLet us assume that the example is in a file named
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\texttt{Order.casl} (actually, this file is provided
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiwith the \Hets distribution as \texttt{Hets-lib/UserManual/Chapter3.casl}).
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThen you can check the well-formedness of the
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederspecification by typing (into some shell):
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\Hets checks both the correctness of this specification
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski with respect to the \CASL syntax, as
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiwell as its correctness with respect to the static semantics (e.g.\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiwhether all identifiers have been declared before they are used,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiwhether operators are applied to arguments of the correct sorts,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiwhether the use of overloaded symbols is unambiguous, and so on).
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThe following flags are available in this context:
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\begin{description}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski -- the static analysis is skipped and no development is created.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski static analysis of (heterogeneous) structured specifications, but
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski leave out the analysis of basic specifications. This can be used
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski for prototyping issues, namely to quickly produce a development graph
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski showing the dependencies among the specifications (cf.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder Sect.~\ref{sec:DevGraph}) even if the individual specifications are
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski not correct yet.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
30256573a343132354b122097b0ee1215dda1364Till MossakowskiUse \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maedercalling \Hets).
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\item[\texttt{-a ANALYSIS}, \texttt{--casl-amalg=ANALYSIS}]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski For the analysis of architectural specification (a quite advanced
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder amalgamability checking
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder algorithm for \CASL logic; it is a comma-separated list of zero or
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder more of the following options:
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \begin{description}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \item[\texttt{sharing}] perform sharing analysis for sorts,
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder operations and predicates.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \item[\texttt{cell}] perform cell condition check; implies
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \texttt{sharing}. With this option on, the subsort embeddings are
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \item[\texttt{colimit-thinness}] perform colimit thinness check;
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder implies \texttt{sharing}. The colimit thinness check is less
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder complete and usually takes longer than the full cell condition
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder check (\texttt{cell} option), but may prove more efficient in case
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder of certain specifications.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \end{description}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder If \texttt{ANALYSIS} is empty then amalgamability analysis for
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \CASL is skipped.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder The default value for \texttt{--casl-amalg} is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{cell}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets accepts plain text input files with the following endings:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{tabular}{|l|c|c|}\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederEnding & default logic & structuring language\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.hs} & Haskell & Haskell\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.elf} & LF & Twelf \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.maude} & Maude & Maude \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFurthermore, \texttt{.xml} files are accepted as Catia output if the default
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic is set to DMU before a library import or by the ``\texttt{-l DMU}''
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicommand line option of \Hets.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederinterchangeable, the former should be used for libraries of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof heterogeneous specifications (that use the \CASL structuring
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito \HasCASL in the following way:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe subsequent specifications are then parsed and analysed as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\HasCASL specifications. Within such specifications,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiit is possible to use references to named \CASL specifications;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithese are then automatically translated along the default
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(There are also heterogeneous constructs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor explicit translations between logics, see \cite{Mossakowski04}.)
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiA \CspCASL specification consists of a \CASL specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor the data part and a \Csp process built over this data part.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{data} as follows:
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{verbatim}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederlibrary Buffer
30256573a343132354b122097b0ee1215dda1364Till Mossakowski free type List[Elem] ::= nil | cons(Elem; List[Elem])
30256573a343132354b122097b0ee1215dda1364Till Mossakowski ops last: List -> ? Elem;
30256573a343132354b122097b0ee1215dda1364Till Mossakowski rest: List -> ? List
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder channel read, write : Elem
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski process Buf(List): read, write, List;
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski EmptyBuffer : read,write, List;
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski Buf(l)= read? x :: Elem -> Buf(cons(x,nil)) []
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski (if l=nil then STOP else
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski write!last(l) -> Buf(rest(l)))
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski EmptyBuffer = Buf(nil)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{verbatim}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiHere, the construct \texttt{data List} refers to the \CASL specification
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\texttt{List}, which is implicitly embedded into \CspCASL.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiThe ending \texttt{.hs} is available for directly reading in
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiHaskell programs % and HasSLe specifications,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederand hence supports the Haskell module system.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe logic Haskell has to be chosen explicitly, and the \CASL structuring
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisyntax needs to be used:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary Factorial
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispec Factorial =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifac :: Int -> Int
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifac n = foldl (*) 1 [1..n]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiNote that according to the Haskell syntax, Haskell function
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskideclarations and definitions need to start with the first column of
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\section{Development Graphs}\label{sec:DevGraph}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskistructured theorem proving and proof management.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederA development graph consists of a set of nodes (corresponding to whole
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskistructured specifications or parts thereof), and a set of arrows
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicalled \emph{definition links}, indicating the dependency of each
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinvolved structured specification on its subparts. Each node is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiassociated with a signature and some set of local axioms. The axioms
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof other nodes are inherited via definition links. Definition links
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare usually drawn as black solid arrows, denoting an import of another
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiComplementary to definition links, which \emph{define} the theories of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskirelated nodes, \emph{theorem links} serve for \emph{postulating}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederrelations between different theories. Theorem links are the central
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskidata structure to represent proof obligations arising in formal
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTheorem links can be \emph{global} (drawn as solid arrows) or
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\emph{local} (drawn as dashed arrows): a global theorem link
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskipostulates that all axioms of the source node (including the inherited
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiones) hold in the target node, while a local theorem link only postulates
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithat the local axioms of the source node hold in the target node.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBoth definition and theorem links can be \emph{homogeneous},
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskii.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe logic changes along the arrow. Technically, this is the case
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor Grothendieck signature morphisms $(\rho,\sigma)$ where
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski$\rho\not=id$. This case is indicated with double arrows.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiTheorem links are initially displayed in red.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe \emph{proof
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder calculus} for development graphs
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\cite{MossakowskiEtAl05,Habil} is given by rules
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithat allow for proving global theorem links by decomposing them
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinto simpler (local and global) ones. Theorem links that have been
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiproved with this calculus are drawn in green. Local theorem links can
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskibe proved by turning them into \emph{local proof goals}. The latter
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskican be discharged using a logic-specific calculus as given by an
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskientailment system for a specific institution. Open local
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiproof goals are indicated by marking the corresponding node in the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederdevelopment graph as red; if all local implications are proved, the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedernode is turned into green. This implementation ultimately is based
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederon a theorem \cite{Habil} stating soundness and relative completeness
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederof the proof calculus for heterogeneous development graphs.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe following options let \Hets show the development graph of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskia specification library:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-u}, \texttt{--uncolored}] no colors in shown graphs
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill MossakowskiThe following additional options also apply typical rules from the development
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskigraph calculus to the final graph and save applying these rule via the GUI.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-A}, \texttt{--apply-automatic-rule}] apply the automatic
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski strategy to the development graph. This is what you usual want in order to
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski get goals within nodes for proving.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-N}, \texttt{--normal-form}] compute all normal forms for nodes
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski with incoming hiding links. (This may take long and may not be implemented
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski for all logics.)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiLet us extend the above library \texttt{Order.casl}. One use of the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary might be to express the fact that the natural numbers form a
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederstrict partial order as a view, as follows:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{EXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{Natural}} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\(\[ \FORALL x,y:Nat \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \. 0 < suc(x) \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \. \neg x < 0 \\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \. suc(x) < suc(y) \IFF x < y
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\NAMEREF{Natural\_Order\_2} =
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\I{} \( Elem \MAPSTO Nat\)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederAgain, these specifications can be checked with \Hets. However, this
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskionly checks syntactic and static semantic well-formedness -- it is
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiby a strict partial ordering relation. Checking this requires theorem
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiproving, which will be discussed below.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederHowever, before coming to theorem proving, let us first inspect the
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiproof obligations arising from a specification. This can be done with:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{hets -g Order.casl}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski(assuming that the above two specifications and the view
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskihave been added to the file
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\Hets now displays a so-called development graph
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski(which is just an overview graph showing the overall structure
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiof the specifications in the library), see Fig.~\ref{fig:dg0}.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{figure}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{center}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\includegraphics[scale=0.7]{dg-order-0}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\caption{Sample development graph.\label{fig:dg0}}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiNodes in a development graph correspond to \CASL specifications.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiArrows show how specifications are related by the structuring
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe black arrow denotes an ordinary import of
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskispecifications (generated by the extension), while the red arrow
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidenotes a proof obligation (corresponding to the view).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThis proof obligation needs to be discharged in order to
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedershow that the view is well-formed (then its color turns into green).
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiAs a more complex example, consider the following loose specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof a sorting function, taken from the \CASL User Manual
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\cite{CASL-UM}, Chap.~6:
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{BIGEXAMPLE}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\I\SPEC \NAMEREF{List\_Order\_Sorted}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{ITEMS}[\WITHIN]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{ITEMS}[\PRED]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\I\PRED \( \_\_is\_sorted : List \)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\(\[ \FORALL e,e': Elem; L : List \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. empty~is\_sorted \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. cons(e,empty)~is\_sorted \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. cons(e,cons(e',L))~is\_sorted \IFF
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following specification of sorting by insertion also is taken from
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe \CASL User Manual \cite{CASL-UM}, Chap.~6:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\phantomsection
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( insert : Elem \* List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e,e':Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ELSE cons(e, cons(e',L)) \] \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e:Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(empty) = empty \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(cons(e,L)) = insert(e, order(L)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederBoth specifications are related. To see this, we first inspect
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedertheir signatures. This is possible with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Sorting.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiassuming that \texttt{Sorting.casl} contains the above specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-1}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIn the above-mentioned development graph, we have two types of nodes.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe named ones correspond to named specifications, but there
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiare also unnamed nodes corresponding to anonymous basic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications like the declaration of the $insert$ operation in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} above. Basically, there is an
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiunnamed node for each structured specification that is not named.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAgain, the black arrows denote an ordinary import of specifications
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(corresponding to the extensions and unions in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications), while the blue arrows denote hiding (corresponding to
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowskithe local specification).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBy clicking on the nodes, one can inspect their signatures.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} have the same signature. Hence, it
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis legal to add a view:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe have already added this view to \texttt{Sorting.casl}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe corresponding
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligation between \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski as a red arrow.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHere is a summary of the types of nodes and links occurring in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidevelopment graphs:\ednote{TODO Christian: update list}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Named nodes] correspond to a named specification.
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\item[Unnamed nodes] correspond to an anonymous specification.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Elliptic nodes] correspond to a specification in the current library.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Rectangular nodes] are external nodes corresponding
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski to a specification downloaded from
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskianother library.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Red nodes] have open proof obligations.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Green nodes] have all proof obligations resolved.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Black links] correspond to reference to other specifications
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(definition links in the sense of \cite[IV:4]{CASL/RefManual}).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Blue links] correspond to hiding (hiding definition links).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Red links] correspond to open proof obligations (theorem links).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Green links] correspond to proved proof obligations (theorem links).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Yellow links] correspond to open proof obligations involving hiding (hiding theorem links).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Solid links] correspond to global (definition or theorem)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilinks in the sense of \cite[IV:4]{CASL/RefManual}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Dashed links] correspond to local (definition or theorem) links in the sense of \cite[IV:4]{CASL/RefManual}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Single links] have homogeneous signature morphisms (staying within
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskione and the same logic).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Double links] have heterogeneous signature morphisms (moving between
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe now explain the menus of the development graph window.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMost of the pull-down menus of the window are uDraw(Graph)-specific
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheir function can be looked up in the uDraw(Graph) documentation\footnote{see
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe exception is the Edit menu. Moreover, the nodes and links
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the graph have attached pop-up menus, which appear when
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiclicking with the right mouse button.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\ednote{TODO Mihai: update}\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Edit] This menu has the following submenus:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[undo] Undo the last development graph proof step (see under Proofs)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[redo] Restore the last undone development graph proof step (see
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski under Proofs)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[reload] Reload the specification library (Attention! all proofs are lost. A change management keep proofs is in preparation.)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Unnamed nodes]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe ``Hide/show names'' menu is a toggle:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiyou can switch on or off the display of names for nodes that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare initially unnamed. The newly named nodes get names that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare derived from named neighbour nodes.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWith the ``Hide nodes'' submenu, it is possible
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito reduce the complexity of the graph by hiding all unnamed nodes;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskionly nodes corresponding to named specifications remain displayed.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiPaths between named nodes going through unnamed nodes
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederare displayed as links. With the ``Show nodes'' submenu, the unnamed
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinodes re-appear.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Proofs] This menu allows to apply some of the deduction rules
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for development graphs, see Sect. IV:4.4 of the \CASL Reference
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Manual \cite{CASL/RefManual} or one of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}. While support for
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder local and global (definition or theorem) links is stable, support
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for hiding links and checking conservativity is still experimental.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski In most cases, it is advisable to use ``Automatic'', which
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski automatically applies the rules in the correct order. As a result,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski the the open theorem links (marked in red) will be reduced to local
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski proof goals, that is, they become green, and instead, some of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski node will get red, indicating open local proof goals.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Besides the deduction rules, the menu contains entries for computing
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski a colimit approximation for the development graph and for
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder computing normal forms of all nodes (needed when dealing with hiding).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Translate Graph] translates the whole development graph
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskialong a logic comorphism.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Show Logic Graph] shows the graph of logics and logic comorphisms
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedercurrently supported by \Hets.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Show Library Graph] shows the graph of libraries that have
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibeen loaded into \Hets, and their dependencies. For library,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe corresponding development graphs can be shown using its node menu.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAlso, a list of specifications and views can be shown.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{description}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Pop-up menu for nodes]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere, the number of submenus depends on the type of the node:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show signature] Shows the signature of the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show local axioms] Shows the local axioms of the node.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Show theory] Shows the theory of the node (including axioms
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederimported from other nodes). Warning: axioms imported via hiding links
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiare not part of the theory; they can be made visible only by re-adding
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederthe hidden symbols, using the proof rule \emph{Theorem-Hide-Shift}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Translate theory] Translates the theory of a node to another logic.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederA menu with the possible translation paths will be displayed.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph of the signature of the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show sublogic] Shows the logic and, within that logic, the minimal sublogic
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederfor the signature and the axioms of the node.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Show origin] Shows the kind of \CASL structuring construct that
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederled to the node.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Show proof status] Show open and proven local proof goals.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Check consistency] Check the consistency of the theory of the node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show just subtree] (Only for named nodes) Reduce the complexity
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederof the graph by just showing the subtree below the current node.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Undo show just subtree] (Only for named nodes) Undo the reduction.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Show referenced library] (Only for external nodes) Open a new window
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedershowing the development graph for the library the external node refers to.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder%\item[Show spec] Show the structured specification of the node.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder% (not fully implemented yet)
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Show number of node] Show the internal number of the node.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Pop-up menu for links]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAgain, the number of submenus depends on the type of the link:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Show morphism] Shows the signature morphism of the link. It consists
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof two components: a logic translation and a signature morphism in the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitarget logic of the logic translation.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIn the (most frequent) case
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof an intra-logic signature morphism, the logic translation component is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskijust the identity.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show origin] Shows the kind of \CASL structuring construct that
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederled to the link.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Show proof status] (Only for theorem links) Show the proof status.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Check conservativity] (Experimental) Check whether the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitheory of the target node of the link
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuis a conservative extension of the theory of the source node.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Show ID of this edge] Shows the internal number of the edge.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThese numbers are also used in the proof status information for
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\end{description}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\end{description}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\section{Reading, Writing and Formatting}
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\Hets provides several options controlling the types of files
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithat are read and written.
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\begin{description}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify \texttt{ITYPE}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu as explicit type of the input file. By default \texttt{env}, \texttt{casl},
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu or \texttt{het} extensions are tried in this order. An \texttt{env} file
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski contains a shared ATerm of a development graph, whereas \texttt{casl} or
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder \texttt{het} files contain plain \HetCASL text. An \texttt{env} file will
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu always be read if it exists and is consistent (aka newer) than the
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu corresponding \HetCASL file.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder \texttt{exp} files contain a development graph in a new experimental omdoc
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu format. \texttt{prf} files contain additional development steps (as shared
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu ATerms) to be applied on top of an underlying development graph created from
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu a corresponding \texttt{env}, \texttt{casl}, or \texttt{het}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu file. \texttt{hpf} files are plain text files representing heterogeneous
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu proof scripts. The contents of a \texttt{hpf} file must be valid input for
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder \Hets in interactive mode. (\texttt{gen\_trm} formats are currently not
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe possible input types are:
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\begin{verbatim}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu casl|het|owl|hs|exp|maude|elf|prf
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu |omdoc|hpf|[tree.]gen_trm[.baf]
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\end{verbatim}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuSpecify \texttt{DIR} as destination directory for output files.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\texttt{OTYPES} is a comma separated list of output types:
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\begin{verbatim}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | (sig|th)[.delta]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | pp.(het|tex|xml)
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\end{verbatim}
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai CodescuThe \texttt{env} and \texttt{prf} formats are for subsequent reading,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederavoiding the need to re-analyse downloaded libraries. \texttt{prf} files
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescucan also be stored or loaded via the GUI's File menu.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe \texttt{owl} option \cite{books/sp/Kohlhase06} will produce OWL files in
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuManchester Syntax for each specification of a structured OWL library.
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederThe \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maedermarkup format and data model for Open Mathematical Documents. It
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuserves as semantics-oriented representation format and ontology
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codesculanguage for mathematical knowledge. Currently, \CASL specifications
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedercan be output in this format; support for further logics is planned.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe \texttt{xml} option will produce an XML-version of the development graph
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescufor our change management broker.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe \texttt{exp} format is the new experimental omdoc format.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe \texttt{hs} format is used for Haskell modules. Executable \CASL or
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\HasCASL specifications can be translated to Haskell.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWhen the \texttt{thy} format is selected, \Hets will try to translate
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedereach specification in the library to \Isabelle, and write one \Isabelle
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{.thy} file per specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWhen the \texttt{comptable.xml} format is selected, \Hets will extract
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuthe composition and inverse table of a Tarskian relation algebra from
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuspecification(s) (selected with the \texttt{-n} or \texttt{--spec}
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maederoption). It is assumed that the relation algebra is
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maedergenerated by basic relations, and that the specification is written
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maederin the \CASL logic. A sample specification of a relation
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescualgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiavailable from \texttt{www.cofi.info/Libraries}.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe output format is XML, the URL of the DTD is included in the
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe \texttt{sig} or \texttt{th} option will create \HetCASL signature or
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescutheory files for each development graph node. (The \texttt{.delta} extension
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiis not supported, yet.)
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe \texttt{pp} format is for pretty printing, either as plain text
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu(\texttt{het}), \LaTeX input (\texttt{tex}) or XML (\texttt{xml}).
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuFor example, it is possible to generate a pretty
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuprinted \LaTeX\ version of \texttt{Order.casl} by typing:
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederThis will generate a file \texttt{Order.pp.tex}. It can be included
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maedercoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe format \texttt{pp.xml} represents a library in XML for our change
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu management broker.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuFormats with \texttt{graph} are for future usage.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe \texttt{dfg} format is used by the \SPASS theorem prover
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\cite{WeidenbachEtAl02}.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuformat for first-order theorem provers.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAppending \texttt{.c} to \texttt{dfg} or \texttt{tptp} will create files for
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettichconsistency checks by SPASS or Darwin respectively.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuFor all output formats it is recommended to increase the verbosity to at least
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederlevel 2 (by using the option \texttt{-v2}) to get feedback which files are
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuactually written. (\texttt{-v2} also shows which files are read.)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskichooses a translation option. \texttt{TRANS} is a colon-separated list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiwithout blanks of one or more comorphism names (see Sect.~\ref{comorphisms}).
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskichooses a list of named specifications for processing
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[\texttt{-R}, \texttt{--recursive}] output also imported libraries.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-I}, \texttt{--interactive}] run \Hets in interactive mode
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-x}, \texttt{--xml}] use xml-pgip packets to communicate with
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \Hets in interactive mode
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[\texttt{-S PORT}, \texttt{--listen=PORT}] communicate
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder with \Hets in interactive mode vy listining to the port \texttt{PORT}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[\texttt{-c HOSTNAME:PORT}, \texttt{--connect=HOSTNAME:PORT}] communicate
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder with \Hets in interactive mode via connecting to the port on host
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \texttt{HOSTNAME}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[\texttt{-d STRING}, \texttt{--dump=STRING}] produces implementation
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder dependent output for debugging purposes only
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\end{description}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\section{Miscellaneous Options}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\begin{description}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederSet the verbosity level according to \texttt{Int}. Default is 1.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[\texttt{-q}, \texttt{--quiet}]
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederBe quiet -- no diagnostic output at all. Overrides -v.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederPrint usage information and exit.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \texttt{Int} megabytes (needed in case of a stack overflow).
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederThis must be the first option.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskideclaration. The default is \CASL.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\section{Proofs with \Hets}\label{sec:Proofs}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe proof calculus for development graphs (Sect.~\ref{sec:DevGraph})
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederreduces global theorem links to local proof goals. Local proof goals
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder(indicated by red nodes in the development graph) can be eventually
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederdischarged using a theorem prover, using the ``Prove'' menu of a red node.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe graphical user interface (GUI) for calling a prover is shown in
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederFig. \ref{fig:proof_window} --- we call it ``Proof Management GUI''.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe list on the left shows all goal names prefixed with the proof
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederstatus in square brackets. A proved goal is indicated by a `+', a `-'
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederindicates a disproved goal, a space denotes an open goal, and a
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder`$\times$' denotes an inconsistent specification (aka a fallen `+';
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedersee below for details).
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{figure}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\includegraphics[width=\textwidth]{proofmanagement1}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\caption{Hets Goal and Prover Interface\label{fig:proof_window}}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIf you open this GUI when processing the goals of one node for the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifirst time, it will show all goals as open. Within this list you can
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederselect those goals that should be inspected or proved. The button
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder`Display' shows the selected goals in the ASCII syntax of this
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitheory's logic in a separate window. With the `Prove' button the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederactual prover is launched. This is described in more detail in the
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiparagraphs below. By pressing the `Show Proof Details' button a window
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiis opened where for each proved goal the used axioms, its proof
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederscript, and its proof are shown --- the level of detail depends on the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederused theorem prover. The `Status:' shows either `No prover running' or
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder`Waiting for prover' in black or blue. If you press the `Close' button
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederthe window is closed and the status of the goals' list is integrated
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederinto the development graph. If all goals have been proved, the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederselected node turns from red into green.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\ednote{TODO Christian: describe disprove button}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\ednote{TODO Christian: describe consistency checker interface}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe list `Pick Theorem Prover:' lets you choose one of the connected
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederprovers (among them \Isabelle, MathServe Broker, \SPASS,
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederVampire, and zChaff, described below). By pressing `Prove' the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiselected prover is launched and the theory along with the selected
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedergoals is translated via the shortest possible path of comorphisms into
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederthe provers logic. The button `More fine grained selection...' lets
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederyou pick a (composed) comorphism in a separate window from where the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiprover is launched then.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederSince the amount and kind of sentences sent to an ATP system is a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskimajor factor for the performance of the ATP system, it is possible to
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiselect the axioms and proven theorems that will comprise the theory
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof the next proof attempt. Based on this selection the sublogic may
30256573a343132354b122097b0ee1215dda1364Till Mossakowskivary and also the available provers and comorphisms to provers. Former
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitheorems that are imported from other specifications are marked with
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe prefix `(Th)'. Since former theorems do not add additional logical
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicontent, they may be safely removed from the theory.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\subsection[Automated Theorem Proving Systems]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder{Automated Theorem Proving Systems\\(Logic SoftFOL)}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\label{sec:ATP}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{figure}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\includegraphics[width=\textwidth]{spassGUI1}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiAll ATPs integrated into \Hets share the same GUI, with only a slight
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskimodification for the MathServe Broker: it does not have input
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifields for extra options. Figure~\ref{fig:SPASS_GUI} shows the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiinstantiation for \SPASS, where in the lower part of the window the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskibatch mode can be controlled. The upper part shows on the left the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskilist of goals (with the same status indicators as in the Proof
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiManagement GUI), and on the right a proof attempt of the selected goal
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiis controlled and the result of the last proof attempt is displayed.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe status line indicates `Open', `Running', `Proved', `Disproved',
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski`Open (Time is up!)', and `Proved (Theory inconsistent!)'. The list of
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiused axioms is actually only filled by \SPASS. The help button displays
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiinformation about the extra options accepted by the ATP system. The
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederbutton `Show Details' shows the whole output of the ATP system. `Save
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederProver Configuration' allows you to save the configuration and status
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederof each proof for documentation. By pressing the button `Exit Prover'
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederthe status of these proofs and goals is transferred back to the
30256573a343132354b122097b0ee1215dda1364Till MossakowskiProof Management GUI.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
30256573a343132354b122097b0ee1215dda1364Till MossakowskiZimmer provides a unified interface to a range of different ATP
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisystems; the most important systems are listed in
30256573a343132354b122097b0ee1215dda1364Till MossakowskiTable~\ref{tab:MathServe}, along with their capabilities. These
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedercapabilities are derived from the \emph{Specialist Problem Classes}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(SPCs) defined upon the basis of logical, language and syntactical
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiproperties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiOnly two of the Web services provided by the MathServe system are used
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiby \Hets currently: Vampire and the brokering system. The ATP systems
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiare offered as Web Services using standardized protocols and formats
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisuch as SOAP, HTTP and XML. Currently, the ATP system Vampire may be
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederaccessed from \Hets via MathServe; the other systems are only reached
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederafter brokering.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{table}[t]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \begin{threeparttable}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \begin{tabular}{|l|c|p{7cm}|}\firsthline
30256573a343132354b122097b0ee1215dda1364Till Mossakowski ATP System & Version & Suitable Problem Classes\tnote{a}\\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \hhline{|=|=|=|}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder DCTP & 10.21p & effectively propositional \\\hline
30256573a343132354b122097b0ee1215dda1364Till Mossakowski EP & 0.91 & effectively propositional; real first-order, no
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder equality; real first-order, equality\\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder Otter & 3.3 & real first-order, no equality\\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \SPASS & 2.2 & effectively propositional; real first-order, no
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder equality; real first-order, equality\\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder Vampire & 8.0 & effectively propositional; pure equality, equality
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder clauses contain non-unit equality clauses; real first-order, no
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder equality, non-Horn\\\hline
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski Waldmeister & 704 & pure equality, equality clauses are unit
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder equality clauses\\\lasthline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \end{tabular}
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski %\renewcommand{\thempfootnote}{\arabic{mpfootnote}}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder %\footnotetext%[\value{footnote}\stepcounter{footnote}]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \begin{tablenotes}\footnotesize
30256573a343132354b122097b0ee1215dda1364Till Mossakowski {The list of problem classes for each ATP system is not
30256573a343132354b122097b0ee1215dda1364Till Mossakowski exhaustive, but only the most appropriate problem classes are
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder named according to benchmark tests made with MathServe by
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder J\"urgen Zimmer.}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \end{tablenotes}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \end{threeparttable}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \caption{ATP systems provided as Web services by MathServe}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\vspace*{-4mm}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \label{tab:MathServe}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\subsubsection*{\SPASS}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe ATP system \SPASS \cite{WeidenbachEtAl02} is a resolution-based
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederprover for first-order logic with equality. Furthermore, it provides a soft
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedertyping mechanism with subsorting that treats sorts as unary
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipredicates. The ATP \SPASS should be installed locally and available
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithrough your \verb,$PATH, environment variable.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\subsubsection*{Vampire}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski% http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe ATP system Vampire is the winner of the last 5 CADE ATP System
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCompetitions (CASC) (2002--2006) in the devisions \verb,FOF, and
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\verb,CNF,. It is a resolution based ATP system supporting the calculi
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof ordered binary resolution and superposition for handling equality.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\url{http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifor detailed information. The connection to Vampire is achieved by
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederusing an Web service of the MathServe system.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\subsubsection*{MathServe Broker}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski% The classes ``effectively propositional'' and ``real first-order''
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% apply to first-order problems that are distinguished by the finiteness
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski% of the Herbrand universe; an effectively propositional problem has
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% only constants (generated by finitely many terms) whereas a real
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich% first-order problem contains true functions with an infinite Herbrand
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe brokering service chooses the most appropriate ATP system
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederupon a classification based on the SPCs, and on a training with the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederlibrary Thousands of Problems for Theorem Provers (TPTP)
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\cite{ZimmerAutexier06}. The TPTP format
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskihas been introduced by Sutcliffe and Suttner for the annual
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcompetition CASC \cite{Sutcliffe:2006:CASC} and provides a unified
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsyntax for untyped FOL with equality, but without any symbol
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\subsection{Isabelle}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\Isabelle \cite{NipPauWen02} is an interactive theorem prover, which is
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichmore powerful than ATP systems, but also requires more user interaction.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskihas a very small core guaranteeing correctness, and its provers,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskilike the simplifier or the tableaux prover, are built on top of this
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskicore. Furthermore, there is over fifteen years of experience with it,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiand several mathematical textbooks have been partially
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \index{formal!verification}%
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\Isabelle is a tactic based theorem prover implemented in standard ML.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe main \Isabelle logic (called Pure) is some weak intuitionistic type
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedertheory with polymorphism. The logic Pure is used to represent a
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedervariety of logics within \Isabelle; one of them being \HOL (higher-order
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederlogic). For example, logical implication in Pure (written
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\texttt{==>}, also called meta-implication), is different from logical
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederimplication in \HOL (written \texttt{-->}, also called object
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederIt is essential to be aware of the fact that the \Isabelle/\HOL logic
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederis different from the logics that are encoded into it via comorphisms.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederTherefore, the formulas appearing in subgoals of proofs with \Isabelle
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederwill not conform to the syntax of the original input logic. They may
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedereven use features of \Isabelle/\HOL such as higher-order functions
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthat are not present in an input logic like \CASL.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\Isabelle is started with ProofGeneral
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\cite{url:Emacs,url:XEmacs}.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe \Isabelle theory file conforms to the Isabelle/Isar syntax
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\cite{NipPauWen02}. It starts with the theory (encoded along the selected
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder comorphism), followed by a list of theorems. Initially, all the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder theorems have trivial proofs, using the `oops` command. However, if
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder you have saved earlier proof attempts, \Hets will patch these into
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder the generated \Isabelle theory file, ensuring that your previous work
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder is not lost. (But note that this patching can only be successful
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder if you do not rename specifications, or change their structure.) You
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder now can replace the 'oops' commands with real \Isabelle proofs, and
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder use Proof General to step through the proofs. You finish your session
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder by saving your file (using the Emacs file menu, or the Ctrl-x Ctrl-s
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder key sequence), and by exiting Emacs (Ctrl-x Ctrl-c).
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\subsection{VSE}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder The specification environment Verification Support Environment
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder(VSE) \cite{VSE00}, developed at
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederDFKI Saarbr\"ucken, provides an industrial-strength methodology
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederfor specification and verification of imperative programs.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederVSE provides an interactive prover, which supports a Gentzen style
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedernatural deduction calculus for dynamic logic.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThis logic is an extension of first-order logic with two additional
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederkinds of formulas
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthat allow for reasoning about programs. One of them is the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederbox formula $[\alpha]\varphi$, where $\alpha$ is a program written in an imperative
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederlanguage, and $\varphi$ is a dynamic logic formula.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe meaning of $[\alpha]\varphi$ can be roughly put as
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder``After every terminating execution of $\alpha$, $\varphi$ holds.''.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe other new kind
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederof formulas is the diamond formula $\langle\alpha\rangle\varphi$, which is the dual counter part
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederof a box formula. The meaning of $\langle\alpha\rangle\varphi$
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedercan be described as ``After some terminating execution of $\alpha$,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder$\varphi$ holds''.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\ednote{TODO Christian: describe interaction with \Hets}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\subsection{zChaff}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederzChaff is a solver for satisfiabily problems of boolean formulas
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder(\normalTEXTSC{S}{AT})
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederin CNF. It is connected as a prover for propositional logic to \Hets. The prover
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\SPASS is used to transform arbitrary boolean formulas to CNF. zChaff
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederimplements the \normalTEXTSC{C}{HAFF}\xspace algorithm. We are
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederusing the property, that a conjecture under the assumption of a set of axioms is
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedertrue, if the variables of axioms together with the negation of the conjecture
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederhave no satisfying assignment, to prove theorems with zChaff. That is why you see
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthe result \normalTEXTSC{U}{NSAT}\xspace in the proof details, if a theorem has been proved
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederto be true. zChaff uses the same ATP GUI as the provers for SoftFOL (ref. to section
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\ref{sec:ATP}). zChaff does not accept any options apart from the time-limit. The
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcurrent integration of zChaff into \Hets has been tested with zChaff 2004.11.15.
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke\subsection{Reduce}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\ednote{TODO : Dominik D.}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\subsection{Pellet}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiPellet is a popular open-source \DL-reasoner for \SROIQ, which is the logic
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiunderlying OWL 2.0, written in Java. A Java Runtime Environment (in version > 1.5)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichis needed to run Pellet. For the integration into \Hets the environment variable
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\verb+PELLET_PATH+ has to be set to the root-directory of the Pellet installation.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiPellet uses the same ATP GUI as the provers for SoftFOL (ref. to section
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\ref{sec:ATP}).
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\subsection{Fact++}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederFact++ is a \DL-reasoner for \SROIQ, which is the logic underlying OWL 2.0, written in
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederC++. Fact++ is integrated into \Hets via the OWL-API, which is written in Java.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederA Java Runtime Environment (in version >= 1.5) has to be installed. To use Fact++,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthe environment variable \verb+HETS_OWL_TOOLS+ has to be set to the directory
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedercontaining the files
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\begin{verbatim}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\end{verbatim}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\begin{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichon a 32bits-Linux-system or
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichin a 64bits-Linux-system. Fact++ does not support options.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichFact++ uses the same ATP GUI as the provers for SoftFOL (ref. to section
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\ref{sec:ATP}).
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsection{QuickCheck}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\ednote{TODO Till}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsection{minisat}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\ednote{TODO Till}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsection{Truth tables}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\ednote{TODO Till}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsection{E-KRHyper}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichE-KRHyper\footnote{\url{http://www.uni-koblenz.de/~bpelzer/ekrhyper/}}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichis an extension of
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichKRHyper\footnote{\url{http://www.uni-koblenz.de/~wernhard/krhyper/}} by
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichhandling of equality. E-KRHyper is an automatic first order theorem
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichprover and model finder based on the Hyper Tableaux Calculus\cite{Baumgartner:1996}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichE-KRHyper is optimized for being integrated into other systems. In the current
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichimplementation we use a default tactics script, that can be influenced by the user.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe options of E-KRHyper are written in a Prolog-like syntax as in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich#(set_parameter(timeout_termination_method,0)).
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichthe ``.'' at the end of each option is mandatory. To get an overview of
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichE-KRHyper's options, run the command
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichin a terminal. Then enter the command
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichat the prompt of E-KRHyper, to display its help information, which is basically
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luetticha long list of all available parameters. You can exit E-KRHyper by the command
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichE-KRHyper uses the same ATP GUI as the other provers for SoftFOL (ref. to section
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\ref{sec:ATP}).
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsection{Darwin}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichDarwin is an automatic first order prover and model finder implementing the Model
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichCalculus\cite{Baumgartner:2003}. The integration of Darwin as a consistency checker
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsupports the display of models (if they can be constructed) in \CASL-syntax.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichEprover is needed to be in the system-path, if Darwin is used with \Hets, since
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiDarwin uses Eprover for clausification of first-order formulae.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichDarwin supports a wide range of options, to get an overview of them run the command
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichin a terminal.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichDarwin uses the same ATP GUI as the other provers for SoftFOL (ref. to section
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\ref{sec:ATP}).
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsection{CspCASLProver}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\ednote{TODO Markus}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\section{Limits of Hets}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\Hets is still intensively under development. In particular, the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichfollowing points are still missing:
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{itemize}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item There is no proof support for architectural specifications.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item Distributed libraries are always downloaded from the local disk,
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichnot from the Internet.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item Version numbers of libraries are not considered properly.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item The proof engine for development graphs provides only experimental
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsupport for hiding links and for conservativity.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\section{Architecture of Hets}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe architecture of \Hets is shown in Fig.~\ref{fig:hets}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichHow is a single logic implemented in the Heterogeneous Tool Set?
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThis is depicted in the left column of Fig.~\ref{fig:hets}.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\Hets provides an abstract interface for
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \index{institution!independence}%
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \index{independence, institution}%
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederinstitutions, so
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithat new logics can be integrated smoothly.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiIn order to do so, a parser,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskia static checker and a prover for basic specifications in the logic have
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederto be provided.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{center}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{verbatim}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiclass Logic lid sign morphism sentence basic_spec symbol_map
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski | lid -> sign morphism sentence basic_spec symbol_map where
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski identity :: lid -> sign -> morphism
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski compose :: lid -> morphism -> morphism -> morphism
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski dom, codom :: lid -> morphism -> sign
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski parse_basic_spec :: lid -> String -> basic_spec
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski parse_symbol_map :: lid -> String -> symbol_map
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski parse_sentence :: lid -> String -> sentence
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski empty_signature :: lid -> sign
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski basic_analysis :: lid -> sign -> basic_spec -> (sign, [sentence])
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski stat_symbol_map :: lid -> sign -> symbol_map -> morphism
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski map_sentence :: lid -> morphism -> sentence -> sentence
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski lid -> [(sign, [sentence]) -> [sentence] -> Proof_status]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski cons_checkers :: lid -> [(sign, [sentence]) -> Proof_status]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiclass Comorphism cid
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski lid1 sign1 morphism1 sentence1 basic_spec1 symbol_map1
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski lid2 sign2 morphism2 sentence2 basic_spec2 symbol_map2
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski | cid -> lid1 lid2 where
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski sourceLogic :: cid -> lid1 targetLogic :: cid -> lid2
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski map_theory :: cid -> (sign1, [sentence1]) -> (sign2, [sentence2])
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski map_morphism :: cid -> morphism1 -> morphism2
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\end{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\caption{The basic ingredients of logics and logic comorphisms}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{fig:logic:all}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiEach logic is realized in the programming language Haskell
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\cite{PeytonJones03} by a set of types and functions, see
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederFig.~\ref{fig:logic:all}, where we present a simplified, stripped down
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederversion, where e.g.\ error handling is ignored. For technical reasons
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskia logic is \emph{tagged} with a unique identifier type (\texttt{lid}),
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiwhich is a singleton type the only purpose of which is to determine
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiall other type components of the given logic. In Haskell jargon, the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiinterface is called a multiparameter type class with functional
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskidependencies \cite{TypeClasses}. The Haskell interface for logic
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskitranslations is realised similarly.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe logic-independent modules in \Hets can be found in the right half
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiof Fig.~\ref{fig:hets}. These modules comprise roughly one third of
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\Hets' 100.000 lines of Haskell code.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe heterogeneous parser transforms a string
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiconforming to the syntax in Fig.~\ref{fig:lang}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskito an abstract syntax tree, using the \texttt{Parsec} combinator parser
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder\cite{Parsec}. Logic and translation names are looked up in the logic
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedergraph --- this is necessary to be able to choose the correct parser
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederfor basic specifications. Indeed, the parser has a state that carries
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederthe current logic, and which is updated if an explicit specification
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederof the logic is given, or if a logic translation is encountered (in
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederthe latter case, the state is set to the target logic of the
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedertranslation). With this, it is possible to parse basic specifications
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederby just using the logic-specific parser of the current logic as
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederobtained from the state.
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederThe static analysis is based on the static analysis of basic
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederspecifications, and transforms an abstract syntax tree to a
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederdevelopment graph (cf.\ Sect.~\ref{sec:DevGraph} above). Starting with a
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedernode corresponding to the empty theory, it successively extends (using
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederthe static analysis of basic specifications) and/or translates (along
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederthe intra- and inter-logic translations) the theory, while
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedersimultaneously adding nodes and links to the development graph.
f8a33e72909e67885a9ecbae881fc75134c362cbDominik LueckeHeterogeneous proof management is done using heterogeneous
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederdevelopment graphs, as described in Sect.~\ref{sec:DevGraph}.
f8a33e72909e67885a9ecbae881fc75134c362cbDominik LueckeFor local proof goals, logic-specific provers are invoked,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedersee Sect.~\ref{sec:Proofs}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\Hets can store development graphs, including their proofs.
f8a33e72909e67885a9ecbae881fc75134c362cbDominik LueckeTherefore, \Hets uses the so-called
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \index{ATerms}%
f8a33e72909e67885a9ecbae881fc75134c362cbDominik LueckeATerm format \cite{BJKO00}, which is used as interchange format
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckefor interfacing with other tools.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederMore details can be found in \cite{Habil,MossakowskiEtAl07b}
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckeand in the overview of modules provided in the developers section
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckeof the \Hets home page at \url{http://www.dfki.de/sks/hets}.
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\begin{figure}
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\begin{center}
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\includegraphics[scale=0.4]{hets2007}
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\caption{Architecture of the heterogeneous tool set.
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\label{fig:hets}}
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\Hets is mainly maintained by
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiChristian Maeder (Christian.Maeder@dfki.de) and Till Mossakowski
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder(Till.Mossakowski@dfki.de). The mailing list is
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \url{hets-users@informatik.uni-bremen.de}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckethe homepage is
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\url{http://www.informatik.uni-bremen.de/mailman/listinfo/hets-users}.
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederYou need to subscribe to the list before you can send a mail.
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian MaederBut note that subscription is very easy!
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeIf your favourite logic is missing in \Hets, please tell us
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke(hets-users@informatik.uni-bremen.de). We will take account your
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckefeedback when deciding which logics and proof tools to integrate next
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeinto \Hets. Help with integration of more logics and proof tools into
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\Hets is also welcome.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\paragraph{Acknowledgement}
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederThe heterogeneous tool set \Hets would not have possible
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckewithout cooperation with many people.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke%Christian Maeder and Klaus L\"uttich.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeBesides the authors, the following people have been involved
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckein the implementation of \Hets:
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeKatja Abu-Dib,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeMihai Codescu,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeCarsten Fischer,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeJorina Freya Gerken,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeRainer Grabbe,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeSonja Gr\"{o}ning,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeDaniel Hausmann,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeWiebke Herding,
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederCui ``Ken'' Jian,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeAnton Kirilov,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeTina Krausser,
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederMartin K\"{u}hl,
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederDominik L\"{u}cke,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke%Klaus L\"{u}ttich,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke%Christian Maeder,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeMaciek Makowski,
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederImmanuel Normann,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeRazvan Pascanu,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeDaniel Pratsch,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeFelix Reckers,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeMarkus Roggenbach,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckePascal Schmidt,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckePaolo Torrini,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeRen\'{e} Wagner,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeJian Chun Wang and
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeThiemo Wiedemeyer.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\Hets has been built based on experiences with its
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \index{Cats@\Cats}%
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \index{Maya@\MAYA}%
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe \CASL Tool Set (\Cats)
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\cite{Mossakowski:2000:CST,Mossakowski:1998:SSA}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeprovides parsing and static analysis for \CASL.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeIt has been developed by the first author with help
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederof Mark van den Brand, Kolyang, Bartek Klin, Pascal Schmidt and
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederFrederic Voisin.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\MAYA \cite{Autexier:2002:IHD,AutexierEtal02} is a proof management
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecketool based on development graphs. \MAYA only supports development
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckegraphs without hiding and without logic translations. \MAYA has been
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckedeveloped by Serge Autexier and Dieter Hutter.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeWe also want to thank Agn\`es Arnould, Thibaud Brunet, Pascale LeGall,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeKathrin Hoffmann, Katiane Lopes,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke%Klaus L\"uttich, Christian Maeder,
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeStefan Merz, Maria Martins Moreira, Christophe
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiRingeissen, Markus Roggenbach, Dmitri Schamschurko, Lutz Schr\"oder,
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederKonstantin Tchekine and Stefan W\"olfl
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederfor giving feedback about \Cats, HOL-CASL and \Hets. Finally,
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederspecial thanks to Christoph L\"uth and George Russell
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederfor help with connecting \Hets to their UniForM workbench.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\bibliographystyle{plain}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\bibliography{cofibib,cofi-ann,UM,hets,kl}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\end{document}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski%%% Local Variables:
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski%%% mode: latex
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%%% TeX-master: "UserGuide"