UserGuide.tex revision 38914aa544a92aa72e537446cfff297dc6109e04
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}\\
c488ac18796ad6383b1edf7fa2820edc8296c89eChristian Maeder-- Version 0.98 --}
e91e02579a34e005734059ad09e0d1d1304a03e0Till Mossakowski\author{Till Mossakowski, Christian Maeder,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Mihai Codescu\\[1em]
464c78620a182d2e8fbd125098045eae8788e2bdTill MossakowskiDFKI GmbH, Bremen, Germany.\\[1em]
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiComments to: hets-users@informatik.uni-bremen.de \\
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\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 the language heterogeneous \CASL.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiHeterogeneous \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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidegree of support by \Hets in Fig.~\ref{fig:Languages}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{figure}[ht]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederSPEC ::= BASIC-SPEC
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | SPEC then SPEC
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | SPEC then %implies SPEC
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | SPEC with SYMBOL-MAP
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | 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
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispecification 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWith \emph{heterogeneous structured specifications}, it is possible to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicombine and rename specifications, hide parts thereof, and also
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprescribe the structure of implementations. \emph{Specification
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder libraries} are collections of named structured and architectural
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\Hets is based on the theory of institutions \cite{GoguenBurstall92},
3532dcfda4dd76997072fcda24e75c305d105233Till 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
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\cite{MossakowskiEA06,MossakowskiEtAl07b}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Logics supported by Hets}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe following list of logics (formalized as so-called institutions
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{GoguenBurstall92}) is currently supported by \Hets:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \includegraphics[scale=0.4]{LogicGraph}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\caption{Graph of logics currently supported by \Hets. The more an
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{fig:LogicGraph}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{figure}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{center}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|c|c|c|}\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL & x & x & - \\\hline
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\CoCASL & x & x & - \\\hline
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maeder\ModalCASL & x & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\HasCASL & x & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederHaskell & (x) & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederCspCASL & x & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederCspCASL\_Trace & - & - & x \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCspCASL\_Failure & - & - & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederCommonLogic & x & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederConstraint\CASL & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederTemporal & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederRelScheme & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederDFOL & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiExtModal & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLF & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Structured specifications & x & x & (x) \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder%Architectural specifications & x & x & -\\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\CASLDL & x & - & - \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiDMU & x & - & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederFreeCAD & - & - & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederOWL DL & x & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederPropositional & x & x & x \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederQBF & x & x & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSoftFOL & x & - & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiMaude & x & x & - \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiVSE & x & x & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Isabelle & (x) & - & x \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHolLight & (x) & - & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiAdl & x & x & - \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederFpl & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiEnCL & x & x & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[CASL] extends many sorted first-order logic with partial
30256573a343132354b122097b0ee1215dda1364Till Mossakowski functions and subsorting. It also provides induction sentences,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski expressing the (free) generation of datatypes.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%It is mainly designed and used for the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%specification of requirements for software systems. But it is also
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%used for the specification of \Dolce (Descriptive Ontology for
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%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}.
7a8592051724fa46499bde120f44cdc8db270876Till 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
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskitypes for signatures, morphisms, abstract syntax etc. This eases
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiintegration of \CASL extensions and keeps the effort of integrating
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\CASL extensions quite moderate.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder is an extension of \CASL with multi-modalities and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiterm modalities. It allows the specification of modal systems with
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiKripke's possible worlds semantics. It is also possible to express
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskicertain forms of dynamic logic.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[ExtModal] is an extended modal logic, currently in an experimental state.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[HasCASL] is a higher order extension of \CASL allowing
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski polymorphic datatypes and functions. It is closely related to the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski programming language Haskell and allows program constructs being
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder embedded in the specification.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe language is summarized in \cite{HasCASL/Summary}, the semantics
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiin \cite{Schroder05b,Schroder-habil}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[Haskell] is a modern, pure and strongly typed functional
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski programming language. It simultaneously is the implementation
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski language of \Hets, such that in the future, \Hets might be applied
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe definitive reference for Haskell is \cite{PeytonJones03},
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski with the process algebra \Csp.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CommonLogic] \url{http://en.wikipedia.org/wiki/Common_logic}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder World Wide Web Consortium (W3C, \url{http://www.w3c.org}). It is
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski used for knowledge representation and the Semantic Web
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \cite{berners:2001:SWeb}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHets calls an external OWL DL parser
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski written in JAVA to obtain the abstract syntax for an OWL file and its
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski imports. The JAVA parser is also doing a first analysis classifying
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Hets only supports the last two, more restricted variants.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski structuring of the OWL imports is displayed as Development Graph.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[CASL-DL] \cite{OWL-CASL-WADT2004}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiis an extension of a restriction of \CASL, realizing
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskia strongly typed variant of OWL DL in \CASL syntax.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \CASL with cardinality restrictions for the description of sorts and
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich unary predicates. The restrictions are based on the equivalence
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski and binary predicates, predefined datatypes and concepts (subsorts
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski of the topsort Thing) are allowed. It is used to bring OWL DL and
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \CASL closer together.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[Propositional] is classical propositional logic, with
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe zChaff SAT solver \cite{Herbstritt03} connected to it.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item[QBF] are quantified boolean formulas, with
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiDepQBF \url{http://fmv.jku.at/depqbf/} connected to it.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item[RelScheme] is a logic for relational databases \cite{DBLP:journals/ao/SchorlemmerK08}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski proving (ATP) systems for first-order logic with equality: (1) \SPASS
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski MathServe Broker\footnote{which chooses an appropriate ATP upon a
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski classification of the FOL problem} \cite{ZimmerAutexier06}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski These together comprise some of the most advanced theorem provers
30256573a343132354b122097b0ee1215dda1364Till Mossakowski for first-order logic.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder for higher-order logic.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[HolLight] \url{http://www.cl.cam.ac.uk/~jrh13/hol-light/}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski is John Harrison's interactive theorem prover
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski for higher-order logic.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[VSE] is an interactive theorem prover, see \ref{subsec:VSE}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[DMU] is a dummy logic to read output of ``Computer Aided
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Three-dimensional Interactive Application'' (Catia).
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[FreeCAD] is a logic to read design files of the CAD system
30256573a343132354b122097b0ee1215dda1364Till Mossakowski FreeCAD\\\url{http://sourceforge.net/projects/free-cad}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Maude] is a rewrite system \url{http://maude.cs.uiuc.edu/} for
30256573a343132354b122097b0ee1215dda1364Till Mossakowski first-order logic. In order to use this logic the environment variable
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \verb+HETS_MAUDE_LIB+ must be set to a directory containing the files
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \verb+full-maude.maude+, \verb+hets.prj+, \verb+maude2haskell.maude+ and
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[DFOL] is an extension of first-order logic with dependent types \cite{rabe:dfol:06}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item [LF] is the dependent type theory of Twelf \url{http://twelf.plparty.org/}. Hets
30256573a343132354b122097b0ee1215dda1364Till Mossakowski calls Twelf on \verb+.elf+ files (for this, the environment variable
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \verb+TWELF_LIB+ must be set) and reads in the OMDoc generated by Twelf.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Moreover, LF can be used as a logical framework to add new logics in Hets \cite{CHK+2011a}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Logic definitions in LF are based in the logic atlas of the Latin project \cite{project:latin}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski and therefore the environment variable \verb+LATIN_LIB+ must be set to the
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder repository with the Latin logic definitions.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\item[Framework] is a dummy logic added for declarative logic definitions \cite{CHK+2011a}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[Adl] is ``A Description Language'' based on relational algebra originally
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski designed for requirements engineering of business rules
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \url{https://lab.cs.ru.nl/BusinessRules/Requirements_engineering}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[Fpl] is a ``logic for functional programs'' as an extension of a
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder restriction of \CASL. (\CASL predicates are disabled.)
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder A detailed description of FPL will appear elsewhere.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\item[EnCL] is an ``engineering calculation language'' based on first
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder order theory of real numbers with some predefined binders
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \cite{logic:EnCL}. It allows the formulation of executable
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder specifications of engineering calculation methods. For the execution
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder of these specifications Hets provides connections to the computer
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder algebra systems Mathematica, Maple and Reduce.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\end{description}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederVarious logics are supported with proof tools. Proof support for the
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederother logics can be obtained by using logic translations to a
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederprover-supported logic.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederAn introduction to \CASL can be found in the \CASL User Manual
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\cite{CASL-UM}; the detailed language reference is given in
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederthe \CASL Reference Manual \cite{CASL/RefManual}. These documents
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederexplain both the \CASL logic and language of basic specifications as
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederwell as the logic-independent constructs for structured and
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederarchitectural specifications. The corresponding document explaining the
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\HetCASL language constructs for \emph{heterogeneous} structured specifications
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederis the \HetCASL language summary \cite{Mossakowski04}; a formal
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maedersemantics as well as a user manual with more examples are in preparation.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederSome of \HetCASL's heterogeneous constructs will be illustrated
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederin Sect.~\ref{sec:HetSpec} below.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Logic translations supported
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\label{comorphisms}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederLogic translations (formalized as institution comorphisms
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\cite{GoguenRosu02}) translate from a given source logic to a given
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitarget logic. More precisely, one and the same logic translation
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maedermay have several source and target \emph{sub}logics: for
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maedereach source sublogic, the corresponding sublogic of the target
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederlogic is indicated.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiA graph of the most important logics and sublogics, together with their
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \includegraphics[scale=0.4]{SublogicGraph}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\caption{Graph of most important sublogics currently supported by \Hets,
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskitogether with their comorphisms.}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\label{fig:SublogicGraph}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederIn more detail, the following list of logic translations is currently
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maedersupported by \Hets:
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\begin{tabular}{|l|p{8cm}|}\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiAdl2CASL & inclusion taking relations to CASL predicates \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2CoCASL & inclusion \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2CspCASL & inclusion \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2HasCASL & inclusion \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2Isabelle & inclusion on sublogic CFOL=
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski(translation $(7)$ of \cite{Mossakowski02}) \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2Modal & inclusion \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2PCFOL & coding of subsorting (SubPCFOL=) by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual} \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskipredicates for the subsorts \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2Propositional & translation of propositional FOL \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2SoftFOL & coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskimapping types to soft types \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL2SoftFOLInduction & same as CASL2SoftFOL but with instances of induction
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiaxioms for all proof goals \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL2SoftFOLInduction2 & similar to CASL2SoftFOLInduction but replaces goals with induction premises \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederCASL2SubCFOL & coding of partial functions by error elements
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting, i.e. sublogic SubPCFOL=) \\\hline
c5e63ec138b908ac9d15e6843120033bf36a1862Till MossakowskiCASL2VSE & inclusion on sublogic CFOL= \\\hline
c488ac18796ad6383b1edf7fa2820edc8296c89eChristian MaederCASL2VSEImport & inclusion on sublogic CFOL= \\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichCASL2VSERefine & refining translation of CASL.CFOL= to VSE \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederCASL\_DL2CASL & inclusion \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCoCASL2Isabelle & extended translation similar to CASL2Isabelle \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCommonLogic2CASL & coding Common Logic to CASL \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCspCASL2CspCASL\_Failure & inclusion \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCspCASL2CspCASL\_Trace & inclusion \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCspCASL2Modal & translating the CASL data part to ModalCASL \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiDFOL2CASL & translating dependent types \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiDMU2OWL & interpreting Catia output as OWL \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\begin{tabular}{|l|p{7cm}|}\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHasCASL2HasCASLNoSubtypes & coding out subtypes \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiHasCASL2HasCASLPrograms & coding of \HasCASL axiomatic recursive definitions
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederas \HasCASL recursive program definitions \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHasCASL2IsabelleOption & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHaskell2Isabelle & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07} \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiHolLight2Isabelle & coding of HolLight to Isabelle/HOL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMaude2CASL & encoding of rewrites as predicates \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederModal2CASL & the standard translation of modal logic
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederto first-order logic \cite{blackburn_p-etal:2001a} \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederOWL2CASL & inclusion \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederOWL2CommonLogic & inclusion \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederPropositional2CASL & inclusion \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederPropositional2QBF & inclusion \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederQBF2Propositional & inclusion \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederRelScheme2CASL & inclusion \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\section{Getting started}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederThe latest \Hets version can be obtained from the
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\Hets tools home page
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder Since \Hets is being
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederimproved constantly, it is recommended always to use the latest version.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\Hets is currently available (on Intel architectures only) for Linux, Solaris
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThere are several possibilities to install \Hets.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{enumerate}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe best support is currently given via Ubuntu packages.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-add-repository ppa:hets/hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-add-repository \
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder "deb http://archive.canonical.com/ubuntu lucid partner"
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-get update
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-get install hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis will also install quite a couple of tools for proving requiring about
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski800 MB of disk space. For a minimal installation \texttt{apt-get install
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski hets-core} instead of \texttt{hets}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item For Mac OSX 10.6 (Snow Leopard) we provide a meta package
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{Hets.mpkg} based on MacPorts that will be extended by further tools
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for proving in the future.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThen we have Java based \Hets installer that we may drop in the future.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDownload a \texttt{.jar} file and start it with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskijava -jar \texttt{file.jar}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidouble-click on the \texttt{.jar} file, but you have to install the MacPorts
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{libglade2} package (and all its dependencies) yourself. In order to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispeed this up we provide a meta package \texttt{libglade2.mpkg}, too.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe installer will lead you through the installation with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia graphical interface. It will download and install further
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisoftware (if not already installed on your computer):
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{tabular}{|l|l|p{5cm}|}\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDarwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederIf you do not have Sun Java, you can just download the hets binary.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederYou have to unpack it with \texttt{bunzip2} and then put it at
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisome place coverd by your \texttt{PATH}. You also have to
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinstall the above mentioned software and set
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiseveral environment variables, as explained on the installation page.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiYou may compile \Hets from the sources, please follow the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilink ``Hets: source code and information for developers''
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskion the \Hets web page, download the sources (as tarball or from
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedersvn), and follow the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinstructions in the \texttt{INSTALL} file, but be prepared to take some time.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\end{enumerate}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiDepending on your application further tools are supported and may be
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederinstalled in addition:
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\begin{tabular}{|l|l|p{5cm}|}\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskizChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiminisat & SAT solver & \url{http://minisat.se/} \\\hline
30256573a343132354b122097b0ee1215dda1364Till MossakowskiPellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederE-KRHyper & theorem prover
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiReduce & computer algebra system
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski & \url{http://www.reduce-algebra.com/} \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederVSE & theorem prover & (non-public) \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiTwelf & & \url{http://twelf.plparty.org/} \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\section{Analysis of Specifications}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiConsider the following \CASL
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification:
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{BIGEXAMPLE}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\I\SPEC \NAME{Strict\_Partial\_Order} =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\PRED]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\SORT \( Elem \)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\(\[ \FORALL x,y,z : Elem \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{COMMENT}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederNote that there may exist \(x, y\) such that\\
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederneither \(x < y\) nor \(y < x\).
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\end{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets can be used for parsing and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskichecking static well-formedness of specifications.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \index{parsing}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{static!analysis}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{analysis, static}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiLet us assume that the example is in a file named
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{Order.casl} (actually, this file is provided
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwith the \Hets distribution as \texttt{Hets-lib/UserManual/Chapter3.casl}).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThen you can check the well-formedness of the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification by typing (into some shell):
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\Hets checks both the correctness of this specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with respect to the \CASL syntax, as
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiwell as its correctness with respect to the static semantics (e.g.\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwhether all identifiers have been declared before they are used,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwhether operators are applied to arguments of the correct sorts,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwhether the use of overloaded symbols is unambiguous, and so on).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe following flags are available in this context:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski -- the static analysis is skipped and no development is created.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski static analysis of (heterogeneous) structured specifications, but
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski leave out the analysis of basic specifications. This can be used
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski for prototyping issues, namely to quickly produce a development graph
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski showing the dependencies among the specifications (cf.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder Sect.~\ref{sec:DevGraph}) even if the individual specifications are
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder not correct yet.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiUse \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicalling \Hets).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-a ANALYSIS}, \texttt{--casl-amalg=ANALYSIS}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski For the analysis of architectural specification (a quite advanced
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski amalgamability checking
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder algorithm for \CASL logic; it is a comma-separated list of zero or
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder more of the following options:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \begin{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \item[\texttt{sharing}] perform sharing analysis for sorts,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder operations and predicates.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \item[\texttt{cell}] perform cell condition check; implies
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \texttt{sharing}. With this option on, the subsort embeddings are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \item[\texttt{colimit-thinness}] perform colimit thinness check;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski implies \texttt{sharing}. The colimit thinness check is less
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski complete and usually takes longer than the full cell condition
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski check (\texttt{cell} option), but may prove more efficient in case
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski of certain specifications.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \end{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder If \texttt{ANALYSIS} is empty then amalgamability analysis for
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowski \CASL is skipped.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski The default value for \texttt{--casl-amalg} is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \texttt{cell}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets accepts plain text input files with the following endings:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|c|c|}\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederEnding & default logic & structuring language\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\texttt{.hol} & HolLight & HolLight \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.hs} & Haskell & Haskell \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.owl} & OWL DL, OWL Lite & OWL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.elf} & LF & Twelf \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.clf} or \texttt{.clif} & CommonLogic & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.maude} & Maude & Maude \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFurthermore, \texttt{.xml} files are accepted as Catia output if the default
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilogic is set to DMU before a library import or by the ``\texttt{-l DMU}''
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicommand line option of \Hets. In all other cases \texttt{.xml} files are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiassumed to be development graph files as produced by ``\texttt{-o xml}''.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiinterchangeable, the former should be used for libraries of
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiof heterogeneous specifications (that use the \CASL structuring
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskito \HasCASL in the following way:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{verbatim}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{verbatim}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe subsequent specifications are then parsed and analysed as
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\HasCASL specifications. Within such specifications,
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiit is possible to use references to named \CASL specifications;
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthese are then automatically translated along the default
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski(There are also heterogeneous constructs
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskifor explicit translations between logics, see \cite{Mossakowski04}.)
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiA \CspCASL specification consists of a \CASL specification
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfor the data part and a \Csp process built over this data part.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{data} as follows:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{verbatim}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskilibrary Buffer
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski free type List[Elem] ::= nil | cons(Elem; List[Elem])
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski ops last: List -> ? Elem;
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski rest: List -> ? List
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski channel read, write : Elem
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski process Buf(List): read, write, List;
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski EmptyBuffer : read,write, List;
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Buf(l)= read? x :: Elem -> Buf(cons(x,nil)) []
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (if l=nil then STOP else
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski write!last(l) -> Buf(rest(l)))
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski EmptyBuffer = Buf(nil)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiHere, the construct \texttt{data List} refers to the \CASL specification
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\texttt{List}, which is implicitly embedded into \CspCASL.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe ending \texttt{.hs} is available for directly reading in
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederHaskell programs % and HasSLe specifications,
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederand hence supports the Haskell module system.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederthe logic Haskell has to be chosen explicitly, and the \CASL structuring
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedersyntax needs to be used:
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{verbatim}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederlibrary Factorial
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispec Factorial =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifac :: Int -> Int
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifac n = foldl (*) 1 [1..n]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote that according to the Haskell syntax, Haskell function
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskideclarations and definitions need to start with the first column of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Development Graphs}\label{sec:DevGraph}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructured theorem proving and proof management.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiA development graph consists of a set of nodes (corresponding to whole
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructured specifications or parts thereof), and a set of arrows
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicalled \emph{definition links}, indicating the dependency of each
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinvolved structured specification on its subparts. Each node is
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederassociated with a signature and some set of local axioms. The axioms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof other nodes are inherited via definition links. Definition links
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare usually drawn as black solid arrows, denoting an import of another
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecification.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiComplementary to definition links, which \emph{define} the theories of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirelated nodes, \emph{theorem links} serve for \emph{postulating}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirelations between different theories. Theorem links are the central
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidata structure to represent proof obligations arising in formal
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTheorem links can be \emph{global} (drawn as solid arrows) or
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{local} (drawn as dashed arrows): a global theorem link
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipostulates that all axioms of the source node (including the inherited
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiones) hold in the target node, while a local theorem link only postulates
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat the local axioms of the source node hold in the target node.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBoth definition and theorem links can be \emph{homogeneous},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskii.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe logic changes along the arrow. Technically, this is the case
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfor Grothendieck signature morphisms $(\rho,\sigma)$ where
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$\rho\not=id$. This case is indicated with double arrows.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTheorem links are initially displayed in red.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe \emph{proof calculus} for development graphs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{MossakowskiEtAl05,Habil} is given by rules
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat allow for proving global theorem links by decomposing them
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinto simpler (local and global) ones. Theorem links that have been
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproved with this calculus are drawn in green. Local theorem links can
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibe proved by turning them into \emph{local proof goals}. The latter
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskican be discharged using a logic-specific calculus as given by an
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskientailment system for a specific institution. Open local
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof goals are indicated by marking the corresponding node in the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidevelopment graph as red; if all local implications are proved, the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskinode is turned into green. This implementation ultimately is based
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskion a theorem \cite{Habil} stating soundness and relative completeness
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the proof calculus for heterogeneous development graphs.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following options let \Hets show the development graph of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskia specification library:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-u}, \texttt{--uncolored}] no colors in shown graphs
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following additional options also apply typical rules from the development
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigraph calculus to the final graph and save applying these rule via the GUI.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-A}, \texttt{--apply-automatic-rule}] apply the automatic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski strategy to the development graph. This is what you usual want in order to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski get goals within nodes for proving.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-N}, \texttt{--normal-form}] compute all normal forms for nodes
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with incoming hiding links. (This may take long and may not be implemented
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for all logics.)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLet us extend the above library \texttt{Order.casl}. One use of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary might be to express the fact that the natural numbers form a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistrict partial order as a view, as follows:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\IEXT{\NAMEREF{Natural}} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y:Nat \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \. 0 < suc(x) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. \neg x < 0 \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. suc(x) < suc(y) \IFF x < y
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I{} \( Elem \MAPSTO Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAgain, these specifications can be checked with \Hets. However, this
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskionly checks syntactic and static semantic well-formedness -- it is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiby a strict partial ordering relation. Checking this requires theorem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproving, which will be discussed below.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHowever, before coming to theorem proving, let us first inspect the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligations arising from a specification. This can be done with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Order.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(assuming that the above two specifications and the view
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihave been added to the file
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a so-called development graph
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(which is just an overview graph showing the overall structure
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the specifications in the library), see Fig.~\ref{fig:dg0}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-0}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Sample development graph.\label{fig:dg0}}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNodes in a development graph correspond to \CASL specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiArrows show how specifications are related by the structuring
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe black arrow denotes an ordinary import of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications (generated by the extension), while the red arrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidenotes a proof obligation (corresponding to the view).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis proof obligation needs to be discharged in order to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskishow that the view is well-formed (then its color turns into green).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAs a more complex example, consider the following loose specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof a sorting function, taken from the \CASL User Manual
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{CASL-UM}, Chap.~6:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order\_Sorted}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\PRED]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_is\_sorted : List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e,e': Elem; L : List \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \. empty~is\_sorted \\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \. cons(e,empty)~is\_sorted \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. cons(e,cons(e',L))~is\_sorted \IFF
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\OP]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\I\OP \( order : List \TOTAL List \)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{BIGEXAMPLE}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederThe following specification of sorting by insertion also is taken from
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskithe \CASL User Manual \cite{CASL-UM}, Chap.~6:
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\begin{BIGEXAMPLE}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\I\SPEC \NAMEREF{List\_Order}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\phantomsection
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\begin{ITEMS}[\WITHIN]
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\begin{ITEMS}[\OP]
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\I\OP \( insert : Elem \* List \TOTAL List \)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\(\[ \FORALL e,e':Elem; L:List \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \ELSE cons(e, cons(e',L)) \] \\
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\begin{ITEMS}[\OP]
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\I\OP \( order : List \TOTAL List \)
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\(\[ \FORALL e:Elem; L:List \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. order(empty) = empty \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. order(cons(e,L)) = insert(e, order(L)) \]\)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{BIGEXAMPLE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBoth specifications are related. To see this, we first inspect
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitheir signatures. This is possible with:
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\texttt{hets -g Sorting.casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiassuming that \texttt{Sorting.casl} contains the above specifications.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{figure}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{center}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\includegraphics[scale=0.7]{dg-order-1}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiIn the above-mentioned development graph, we have two types of nodes.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\NAMEREF{List\_Order} above. Basically, there is an
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiunnamed node for each structured specification that is not named.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiAgain, the black arrows denote an ordinary import of specifications
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(corresponding to the extensions and unions in the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispecifications), while the blue arrows denote hiding (corresponding to
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe local specification).
30256573a343132354b122097b0ee1215dda1364Till MossakowskiBy clicking on the nodes, one can inspect their signatures.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\NAMEREF{List\_Order} have the same signature. Hence, it
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis legal to add a view:
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescu\begin{EXAMPLE}%[\SLIDESMALL]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescu\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWe have already added this view to \texttt{Sorting.casl}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe corresponding
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproof obligation between \NAMEREF{List\_Order\_Sorted} and
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski as a red arrow.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiHere is a summary of the types of nodes and links occurring in
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskidevelopment graphs:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{description}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Named nodes] correspond to a named specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Unnamed nodes] correspond to an anonymous specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Elliptic nodes] correspond to a specification in the current library.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\item[Rectangular nodes] are external nodes corresponding to a specification
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski downloaded from another library.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Red nodes] have open proof obligations.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Yellow nodes] have an open conservativity proof obligations.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[Green nodes] have all proof obligations resolved.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Black links] correspond to reference to other specifications (definition
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski links in the sense of \cite[IV:4]{CASL/RefManual}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Red links] correspond to open proof obligations (theorem links).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Green links] correspond to proven theorem links.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Yellow links] correspond to proven theorem links with open
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski conservativity or to open hiding theorem links.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Blue links] correspond to hiding, free, or cofree definition links.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Violett links] correspond to a mixture of links becoming visible after
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski ``expand'' or ``Show unnamed nodes with open proofs''.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Solid links] correspond to global (definition or theorem)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilinks in the sense of \cite[IV:4]{CASL/RefManual}.
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich\item[Dashed links] correspond to local (theorem) links in the sense of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \cite[IV:4]{CASL/RefManual}. These are usually created after
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ``Global-Decomposition'' or only be visible after ``Show newly added proven
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Single line links] have homogeneous signature morphisms (staying within
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski one and the same logic).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Double line links] have heterogeneous signature morphisms (moving
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski between logics).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWe now explain the menus of the development graph window.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederMost of the pull-down menus of the window are uDraw(Graph)-specific
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskitheir function can be looked up in the uDraw(Graph) documentation\footnote{see
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThe exception is the Edit menu. Moreover, the nodes and links
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiof the graph have attached pop-up menus, which appear when
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiclicking with the right mouse button.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Edit] This menu has the following submenus:
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\begin{description}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Undo] Undo the last development graph proof step (see under Proofs)
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Redo] Restore the last undone development graph proof step (see
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder under Proofs)
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederThe ``Hide/show names/nodes/edges'' menu is a toggle:
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederyou can switch on or off the display of node names, unnamed nodes or
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederproven theorem links.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederWith the ``Hide/show internal node names'' option, the nodes that
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederare initially unnamed get derived names.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederWith the ``Hide/show unnamed nodes without open proofs'' option, it is possible
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederto reveal the unnamed nodes which do not have open proof goals.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederInitially, the complexity of the graph is reduced by hiding all these nodes;
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederonly nodes corresponding to named specifications are displayed.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederPaths between named nodes going through unnamed nodes
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederare displayed as edges; these paths are then expanded when showing the
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederunnamed nodes.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederWhen applying the development graph calculus rules, theorem links that have
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederbeen proven are removed from the graph. With the ``Hide/Show newly added
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederproven edges'' option, it is possible to re-display these links; they are marked
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederas proven in the link info (see \emph{Pop-up menu for links}, below).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Focus node]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis menu is particularly useful when navigating in a large development graph,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiwhich does not fit on a single screen. The list of all nodes is displayed:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe nodes are identified by the internal node number and the internal node name.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederOnce a node is selected, the view centers on it.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Select Linktypes]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThis menu allows to select the type of links that are displayed in the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederdevelopment graph. A selection window appears, where links are grouped into
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederthree categories: definition links, proven theorem links and unproven
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedertheorem links. It is possible to select/deselect all links or to invert the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedercurrent selection.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Consistency checker]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder Checks whether the theories of the nodes of the graph are consistent
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder i.e. have a model. The model finders currently interfaced are
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder Isabelle-refute, darwin and E-KRHyper, with best support for darwin.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Proofs] This menu allows to apply some of the deduction rules
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski for development graphs, see Sect. IV:4.4 of the \CASL Reference
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski Manual \cite{CASL/RefManual} or one of
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}. While support for
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder local and global (definition or theorem) links is stable, support
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski for hiding links and checking conservativity is still experimental.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski In most cases, it is advisable to use ``Auto-DG-Prover'', which
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder automatically applies the rules in the correct order. As a result,
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder the open theorem links (marked in red) will be reduced to local
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski proof goals, that is, they become green, and instead, some target nodes
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder may get red, indicating open local proof goals.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski Besides the deduction rules, the menu contains entries for computing
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski a colimit approximation for the development graph and for
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder computing normal forms of all nodes (needed when dealing with hiding).
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder Also, a \CASL-specific normalisation of free links has been
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Dump Development Graph] This option is available only for
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder debugging purposes; it outputs a textual representation
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder of the development graph.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Show Library Graph] This menu displays the library graph, in a separate
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder window, if the library graph window has been closed after \Hets has been
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Save Graph for uDrawGraph] Saves the development graph in a .udg file
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder which can be later read by uDrawGraph.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Save proof-script] This menu saves the proof rules that have been applied
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder to the current development graph in a .hpf file which can be later read by
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \Hets and thus the action performed on the graph are saved.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Pop-up menu for nodes]
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHere, the number of submenus depends on the type of the node:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Show node info] Shows the local informations of the node: the internal
30256573a343132354b122097b0ee1215dda1364Till Mossakowski node name and node number, the xpath that denotes the location of the node
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski within an XML representation, information about consistency of the node,
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder origin of the node and the local theory i.e. axioms declared locally.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Show theory] Shows the theory of the node (including axioms
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederimported from other nodes). Notice that axioms imported via hiding links
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederare not part of the theory; they can be made visible only by re-adding
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe hidden symbols, using the normal form of the node, by calling
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\emph{Proofs/Compute Normal Form}. For such nodes, a warning is displayed.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Translate theory] Translates the theory of a node to another logic.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiA menu with the possible translation paths will be displayed.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski of the signature of the node.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Show proof status] Show open and proven local proof goals.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Prove VSE structured] Allows to send a development graph below the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski current node to the interactive \texttt{hetsvse} prover if that binary is
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski available, see \ref{subsec:VSE}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Disprove] Negates selected goals and tries to disprove them using
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder consistency checkers. Other goals will be treated like axioms if ``Include
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder Theorems'' is selected. (If a theory is consistent with a negated goal, the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder goal is disproven.)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Add sentence] This menu allows to add a sentence on the fly. The
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder (possibly named) sentence will be parsed and analysed using the unlying logic.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Check consistency] Simply calls the global ``Consistency checker'' menu
30256573a343132354b122097b0ee1215dda1364Till Mossakowski for the current node, see \ref{sec:CC}.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Check conservativity] Checks conservativity of the inclusion
30256573a343132354b122097b0ee1215dda1364Till Mossakowski morphism from the empty theory to the theory of the node (see
30256573a343132354b122097b0ee1215dda1364Till Mossakowski {\bf Check conervativity} for edges).
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{description}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFor the nodes which are references to specifications from an external library,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe pop-up menu options are reduced to {\bf Show node info, Show theory,
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederShow proof status} and {\bf Prove} and moroever, the option {\bf Show
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederreferenced library} is added: on selection, it displays in a new window
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederthe development graph of the external library from which the specification has
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederbeen downloaded.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[Pop-up menu for links]
30256573a343132354b122097b0ee1215dda1364Till MossakowskiAgain, the number of submenus depends on the type of the link:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Show info] Shows informations about the edge: internal number and
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederinternal nodes it links, the link type and origin and the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisignature morphism of the link. The latter consists
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederof two components: a logic translation and a signature morphism in the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedertarget logic of the logic translation.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederIn the (most frequent) case
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederof an intra-logic signature morphism, the logic translation component is
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederjust the identity.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Check conservativity] (Experimental) Check whether the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedertheory of the target node of the link
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowskiis a conservative extension of the theory of the source node.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Expand]This menu is available only for paths going through unnamed
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskinodes which are not displayed and it expands the path to the links forming it.
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski\end{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\end{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederBesides development graphs there are library graph windows displaying the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilibrary hierarchy. The Edit menu has the following submenus:
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Edit] This menu for library graphs has the following submenus:
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Reload Library] Reloads all \HetCASL sources in order to avoid closing
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder and restarting the application after sources have changed. However, all
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder previous proof steps will be lost, therefore you have to confirm this
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder action. (A change management tool to keep proofs is in preparation.)
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Experimental reload changed Library] This button is supposed to
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder interface our change management tool (in order to preserve proof
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder information) but does not work yet.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Translate Library] Translates a library along a comorphism to be chosen.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder This only works for a homogeneous library hierarchy. A finer grained
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder alternative is to use ``Translate theory'' for individual nodes. The
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder original state and proof steps will be lost, therefore you have to confirm
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Show Logic Graph] Shows the graph of logics and logic comorphisms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski currently supported by \Hets. The Edit menu of a logic graph window has the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski following submenu:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Show detailed logic graph] Shows the important sublogics and comorphims
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski between them, i.e. translation (blue links) and inclusion (black links).
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\section{Reading, Writing and Formatting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets provides several options controlling the types of files
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskithat are read and written.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify \texttt{ITYPE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski as explicit type of the input file. By default \texttt{env}, \texttt{casl},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski or \texttt{het} extensions are tried in this order. An \texttt{env} file
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich contains a shared ATerm of a development graph, whereas \texttt{casl} or
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \texttt{het} files contain plain \HetCASL text. An \texttt{env} file will
30256573a343132354b122097b0ee1215dda1364Till Mossakowski always be read if it exists and is consistent (aka newer) than the
30256573a343132354b122097b0ee1215dda1364Till Mossakowski corresponding \HetCASL file.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \texttt{exp} files contain a development graph in a new experimental omdoc
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski format. \texttt{prf} files contain additional development steps (as shared
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich ATerms) to be applied on top of an underlying development graph created from
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich a corresponding \texttt{env}, \texttt{casl}, or \texttt{het}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich file. \texttt{hpf} files are plain text files representing heterogeneous
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich proof scripts. The contents of a \texttt{hpf} file must be valid input for
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \Hets in interactive mode. (\texttt{gen\_trm} formats are currently not
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe possible input types are:
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich | [tree.]gen_trm[.baf]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichSpecify \texttt{DIR} as destination directory for output files.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\texttt{OTYPES} is a comma separated list of output types:
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{verbatim}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski | (sig|th)[.delta]
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski | pp.(het|tex|xml|html)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{env} and \texttt{prf} formats are for subsequent reading,
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichavoiding the need to re-analyse downloaded libraries. \texttt{prf} files
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcan also be stored or loaded via the GUI's File menu.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{omn} option \cite{books/sp/Kohlhase06} will produce OWL files in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichManchester Syntax for each specification of a structured OWL library.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskimarkup format and data model for Open Mathematical Documents. It
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiserves as semantics-oriented representation format and ontology
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskilanguage for mathematical knowledge. Currently, \CASL specifications
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcan be output in this format; support for further logics is planned.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe \texttt{xml} option will produce an XML-version of the development graph
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskifor our change management broker.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{exp} format is the new experimental omdoc format.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{hs} format is used for Haskell modules. Executable \CASL or
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\HasCASL specifications can be translated to Haskell.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichWhen the \texttt{thy} format is selected, \Hets will try to translate
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luetticheach specification in the library to \Isabelle, and write one \Isabelle
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\texttt{.thy} file per specification.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichWhen the \texttt{comptable.xml} format is selected, \Hets will extract
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichthe composition and inverse table of a Tarskian relation algebra from
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichspecification(s) (selected with the \texttt{-n} or \texttt{--spec}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichoption). It is assumed that the relation algebra is
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichgenerated by basic relations, and that the specification is written
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichin the \CASL logic. A sample specification of a relation
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichalgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichavailable from \texttt{www.cofi.info/Libraries}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe output format is XML, the URL of the DTD is included in the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{sig} or \texttt{th} option will create \HetCASL signature or
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichtheory files for each development graph node. (The \texttt{.delta} extension
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichis not supported, yet.)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{pp} format is for pretty printing, either as plain text
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich(\texttt{het}), \LaTeX input (\texttt{tex}), HTML (\texttt{html}) or XML
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich(\texttt{xml}). For example, it is possible to generate a pretty printed
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\LaTeX\ version of \texttt{Order.casl} by typing:
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThis will generate a file \texttt{Order.pp.tex}. It can be included
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe format \texttt{pp.xml} represents just a parsed library in XML.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichFormats with \texttt{graph} are for future usage.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{dfg} format is used by the \SPASS theorem prover
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\cite{WeidenbachEtAl02}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichformat for first-order theorem provers.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichAppending \texttt{.c} to \texttt{dfg} or \texttt{tptp} will create files for
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichconsistency checks by SPASS or Darwin respectively.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichFor all output formats it is recommended to increase the verbosity to at least
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichlevel 2 (by using the option \texttt{-v2}) to get feedback which files are
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichactually written. (\texttt{-v2} also shows which files are read.)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichchooses a translation option. \texttt{TRANS} is a colon-separated list
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichwithout blanks of one or more comorphism names (see Sect.~\ref{comorphisms})
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichchooses a list of named specifications for processing
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-w NVIEWS}, \texttt{--view=NVIEWS}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichchooses a list of named views for processing
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-R}, \texttt{--recursive}] output also imported libraries
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[\texttt{-I}, \texttt{--interactive}] run \Hets in interactive mode
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-X}, \texttt{--server}] run \Hets as web server
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-x}, \texttt{--xml}] use xml-pgip packets to communicate with
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \Hets in interactive mode
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-S PORT}, \texttt{--listen=PORT}] communicate
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich with \Hets in interactive mode vy listining to the port \texttt{PORT}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-c HOSTNAME:PORT}, \texttt{--connect=HOSTNAME:PORT}] communicate
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich with \Hets in interactive mode via connecting to the port on host
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \texttt{HOSTNAME}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-d STRING}, \texttt{--dump=STRING}] produces implementation
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich dependent output for debugging purposes only
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (i.e.\ \texttt{-d LogicGraph} lists the logics and comorphisms)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{description}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\section{Miscellaneous Options}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{description}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederSet the verbosity level according to \texttt{Int}. Default is 1.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-q}, \texttt{--quiet}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichBe quiet -- no diagnostic output at all. Overrides -v.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichPrint usage information and exit.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \texttt{Int} megabytes (needed in case of a stack overflow).
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThis must be the first option.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichdeclaration. The default is \CASL.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-e ENCODING}, \texttt{--encoding=ENCODING}] Read input files using latin1 or utf8 encoding. The default is still latin1.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{--unlit}] Read literate input files.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{--relative-positions}] Just uses the relative library name in positions of warning or errors.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-U FILE}, \texttt{--xupdate=FILE}] update a development graph according to special xml update information (still experimental).
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\end{description}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\section{Proofs with \Hets}\label{sec:Proofs}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe proof calculus for development graphs (Sect.~\ref{sec:DevGraph}) reduces
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiglobal theorem links to local proof goals. Local proof goals (indicated by red
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedernodes in the development graph) can be eventually discharged using a theorem
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiprover, i.e. by using the ``Prove'' menu of a red node.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe graphical user interface (GUI) for calling a prover is shown in
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiFig. \ref{fig:proof_window} --- we call it ``Proof Management GUI''.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe top list on the left shows all goal names prefixed with the proof
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskistatus in square brackets. A proved goal is indicated by a `+', a `-'
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiindicates a disproved goal, a space denotes an open goal, and a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski`$\times$' denotes an inconsistent specification (aka a fallen `+';
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskisee below for details).
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\includegraphics[width=\textwidth]{proofmanagement1}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\caption{Hets Goal and Prover Interface\label{fig:proof_window}}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiIf you open this GUI when processing the goals of one node for the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskifirst time, it will show all goals as open. Within this list you can
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiselect those goals that should be inspected or proved. The GUI elements are the following:
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{itemize}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item The button `Display' shows the selected goals in the ASCII syntax of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski this theory's logic in a separate window.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item By pressing the `Proof details' button a window is opened where for each
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski proved goal the used axioms, its proof script, and its proof are shown ---
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski the level of detail depends on the used theorem prover.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item With the `Prove' button the actual prover is launched. This is described
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski in more detail in the paragraphs below.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item The list `Pick Theorem Prover:' lets you choose one of the connected
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski provers (among them \Isabelle, MathServe Broker, \SPASS, Vampire, and
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski zChaff, described below). By pressing `Prove' the selected prover is
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder launched and the theory along with the selected goals is translated via the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski shortest possible path of comorphisms into the provers logic.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item The pop-up choice box below `Selected comorphism path:' lets you pick a
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski (composed) comorphism to be used for the chosen prover.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item Since the amount and kind of sentences sent to an ATP system is a major
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski factor for the performance of the ATP system, it is possible to select in
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder the bottom lists the axioms and proven theorems that will comprise the
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder theory of the next proof attempt. Based on this selection the sublogic may
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski vary and also the available provers and comorphisms to provers. Former
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski theorems that are imported from other specifications are marked with the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski prefix `(Th)'. Since former theorems do not add additional logical content,
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski they may be safely removed from the theory.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item If you press the bottom-right `Close' button the window is closed and
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski the status of the goals' list is integrated into the development graph. If
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski all goals have been proved, the selected node turns from red into green.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item All other buttons control selecting list entries
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\subsection{Consistency Checker}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\label{sec:CC}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiSince proofs are void if specifications are inconsistent, the consistency
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskishould be checked (if possible for the given logic) by the ``Consistency
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskichecker'' shown in Fig. \ref{fig:cons_window}. This GUI is invoked from
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederthe `Edit' menu as it operates on all nodes.
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederThe list on the left shows all node names prefixed with a consistency status
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederin square brackets that is initially empty. A consistent node is indicated by
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedera `+', a `-' indicates an inconsistent node, a `t' denotes a timeout of the last
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederchecking attempt.
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder\begin{figure}
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder\includegraphics[width=\textwidth]{ConsistencyChecker}
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder\caption{Hets Consistency Checker Interface\label{fig:cons_window}}
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederFor some selection of nodes (of a common logic) a model finder should be
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederselectable from the `Pick Model finder:' list. Currently only for ``darwin''
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedersome \CASL models can be re-constructed. When pressing `Check', possibly after
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder`Select comorphism path:', all selected nodes will be checked, spending at
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedermost the number of seconds given under `Timeout:' on each node. Pressing
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder`Stop' allows to terminate this process if too many nodes have been chosen.
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederEither by `View results' or automatically the `Results of consistency check'
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski(Fig. \ref{fig:cons_res}) will pop up and allow you to inspect the models for
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckenodes, if they could be constructed.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{figure}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\includegraphics[width=\textwidth]{ConsCheckResults}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\caption{Consistency Checker Results\label{fig:cons_res}}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\subsection[Automated Theorem Proving Systems]
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke{Automated Theorem Proving Systems\\(Logic SoftFOL)}
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke\label{sec:ATP}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{figure}
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke\includegraphics[width=\textwidth]{spassGUI1}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederAll ATPs integrated into \Hets share the same GUI, with only a slight
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckemodification for the MathServe Broker: the input field for extra options is
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeinactive. Figure~\ref{fig:SPASS_GUI} shows the instantiation for \SPASS, where
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckein the top right part of the window the batch mode can be controlled. The
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeleft side shows the list of goals (with status indicators). If goals are
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecketimed out (indicated by `t') is may help to activate the check box `Include
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckepreceeding proven theorems in next proof attempt' and pressing `Prove all'
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederOn the bottom right the result of the last proof
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederattempt is displayed. The `Status:' indicates `Open', `Proved', `Disproved',
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder`Open (Time is up!)', or `Proved (Theory inconsistent!)'. The list of `Used
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeAxioms:' is filled by \SPASS. The button `Show Details' shows the whole output
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeof the ATP system. The `Save' buttons allow you to save the input and
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeconfiguration of each proof for documentation. By `Close' the results for all
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckegoals are transferred back to the Proof Management GUI.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeThe MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeZimmer provides a unified interface to a range of different ATP
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maedersystems; the most important systems are listed in
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeTable~\ref{tab:MathServe}, along with their capabilities. These
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckecapabilities are derived from the \emph{Specialist Problem Classes}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke(SPCs) defined upon the basis of logical, language and syntactical
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeproperties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeOnly two of the Web services provided by the MathServe system are used
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeby \Hets currently: Vampire and the brokering system. The ATP systems
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeare offered as Web Services using standardized protocols and formats
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckesuch as SOAP, HTTP and XML. Currently, the ATP system Vampire may be
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeaccessed from \Hets via MathServe; the other systems are only reached
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeafter brokering.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{table}[t]
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \begin{threeparttable}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \begin{tabular}{|l|c|p{7cm}|}\firsthline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski ATP System & Version & Suitable Problem Classes\tnote{a}\\
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \hhline{|=|=|=|}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke DCTP & 10.21p & effectively propositional \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder EP & 0.91 & effectively propositional; real first-order, no
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder equality; real first-order, equality\\\hline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke Otter & 3.3 & real first-order, no equality\\\hline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \SPASS & 2.2 & effectively propositional; real first-order, no
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke equality; real first-order, equality\\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder Vampire & 8.0 & effectively propositional; pure equality, equality
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke clauses contain non-unit equality clauses; real first-order, no
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder equality, non-Horn\\\hline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke Waldmeister & 704 & pure equality, equality clauses are unit
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke equality clauses\\\lasthline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \end{tabular}
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder %\renewcommand{\thempfootnote}{\arabic{mpfootnote}}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke %\footnotetext%[\value{footnote}\stepcounter{footnote}]
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \begin{tablenotes}\footnotesize
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke {The list of problem classes for each ATP system is not
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke exhaustive, but only the most appropriate problem classes are
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke named according to benchmark tests made with MathServe by
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke J\"urgen Zimmer.}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \end{tablenotes}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \end{threeparttable}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \caption{ATP systems provided as Web services by MathServe}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\vspace*{-4mm}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \label{tab:MathServe}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\subsubsection*{\SPASS}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe ATP system \SPASS \cite{WeidenbachEtAl02} is a resolution-based
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederprover for first-order logic with equality. Furthermore, it provides a soft
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecketyping mechanism with subsorting that treats sorts as unary
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckepredicates. The ATP \SPASS should be installed locally and available
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederthrough your \verb,$PATH, environment variable.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\subsubsection*{Vampire}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke% http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeThe ATP system Vampire is the winner of the last 5 CADE ATP System
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeCompetitions (CASC) (2002--2006) in the devisions \verb,FOF, and
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\verb,CNF,. It is a resolution based ATP system supporting the calculi
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeof ordered binary resolution and superposition for handling equality.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\url{http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckefor detailed information. The connection to Vampire is achieved by
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeusing an Web service of the MathServe system.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\subsubsection*{MathServe Broker}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski% The classes ``effectively propositional'' and ``real first-order''
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski% apply to first-order problems that are distinguished by the finiteness
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski% of the Herbrand universe; an effectively propositional problem has
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski% only constants (generated by finitely many terms) whereas a real
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski% first-order problem contains true functions with an infinite Herbrand
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiThe brokering service chooses the most appropriate ATP system
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiupon a classification based on the SPCs, and on a training with the
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskilibrary Thousands of Problems for Theorem Provers (TPTP)
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\cite{ZimmerAutexier06}. The TPTP format
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskihas been introduced by Sutcliffe and Suttner for the annual
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskicompetition CASC \cite{Sutcliffe:2006:CASC} and provides a unified
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskisyntax for untyped FOL with equality, but without any symbol
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\subsection{Isabelle}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Isabelle \cite{NipPauWen02} is an interactive theorem prover, which is
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedermore powerful than ATP systems, but also requires more user interaction.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihas a very small core guaranteeing correctness, and its provers,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederlike the simplifier or the tableaux prover, are built on top of this
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicore. Furthermore, there is over fifteen years of experience with it,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand several mathematical textbooks have been partially
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{formal!verification}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Isabelle is a tactic based theorem prover implemented in standard ML.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe main \Isabelle logic (called Pure) is some weak intuitionistic type
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheory with polymorphism. The logic Pure is used to represent a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskivariety of logics within \Isabelle; one of them being \HOL (higher-order
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilogic). For example, logical implication in Pure (written
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{==>}, also called meta-implication), is different from logical
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiimplication in \HOL (written \texttt{-->}, also called object
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederIt is essential to be aware of the fact that the \Isabelle/\HOL logic
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis different from the logics that are encoded into it via comorphisms.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiTherefore, the formulas appearing in subgoals of proofs with \Isabelle
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiwill not conform to the syntax of the original input logic. They may
30256573a343132354b122097b0ee1215dda1364Till Mossakowskieven use features of \Isabelle/\HOL such as higher-order functions
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithat are not present in an input logic like \CASL.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\Isabelle is started with ProofGeneral
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{url:Emacs,url:XEmacs}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \Isabelle theory file conforms to the Isabelle/Isar syntax
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{NipPauWen02}. It starts with the theory (encoded along the selected
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder comorphism), followed by a list of theorems. Initially, all the
30256573a343132354b122097b0ee1215dda1364Till Mossakowski theorems have trivial proofs, using the `oops` command. However, if
30256573a343132354b122097b0ee1215dda1364Till Mossakowski you have saved earlier proof attempts, \Hets will patch these into
30256573a343132354b122097b0ee1215dda1364Till Mossakowski the generated \Isabelle theory file, ensuring that your previous work
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder is not lost. (But note that this patching can only be successful
30256573a343132354b122097b0ee1215dda1364Till Mossakowski if you do not rename specifications, or change their structure.) You
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder now can replace the 'oops' commands with real \Isabelle proofs, and
30256573a343132354b122097b0ee1215dda1364Till Mossakowski use Proof General to step through the proofs. You finish your session
30256573a343132354b122097b0ee1215dda1364Till Mossakowski by saving your file (using the Emacs file menu, or the Ctrl-x Ctrl-s
30256573a343132354b122097b0ee1215dda1364Till Mossakowski key sequence), and by exiting Emacs (Ctrl-x Ctrl-c).
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{VSE}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\label{subsec:VSE}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski The specification environment Verification Support Environment
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(VSE) \cite{VSE00}, developed at
30256573a343132354b122097b0ee1215dda1364Till MossakowskiDFKI Saarbr\"ucken, provides an industrial-strength methodology
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor specification and verification of imperative programs.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiVSE provides an interactive prover, which supports a Gentzen style
30256573a343132354b122097b0ee1215dda1364Till Mossakowskinatural deduction calculus for dynamic logic.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThis logic is an extension of first-order logic with two additional
30256573a343132354b122097b0ee1215dda1364Till Mossakowskikinds of formulas
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithat allow for reasoning about programs. One of them is the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskibox formula $[\alpha]\varphi$, where $\alpha$ is a program written in an imperative
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilanguage, and $\varphi$ is a dynamic logic formula.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe meaning of $[\alpha]\varphi$ can be roughly put as
30256573a343132354b122097b0ee1215dda1364Till Mossakowski``After every terminating execution of $\alpha$, $\varphi$ holds.''.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe other new kind
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof formulas is the diamond formula $\langle\alpha\rangle\varphi$, which is the dual counter part
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof a box formula. The meaning of $\langle\alpha\rangle\varphi$
30256573a343132354b122097b0ee1215dda1364Till Mossakowskican be described as ``After some terminating execution of $\alpha$,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski$\varphi$ holds''.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiA VSE specification or something that can be translated to VSE (currently only
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\CASL) can be sent to the VSE prover via the node menu of development graph
30256573a343132354b122097b0ee1215dda1364Till Mossakowskinodes in two different ways. You can either select VSE from the theorem prover
30256573a343132354b122097b0ee1215dda1364Till Mossakowskichoice box shown after ``Prove'' or you can select ``Prove VSE Structured''.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe first choice will call VSE with a single flattened theory whereas a
30256573a343132354b122097b0ee1215dda1364Till Mossakowskistructured call will translate all nodes with ingoing links to the current one
30256573a343132354b122097b0ee1215dda1364Till MossakowskiVSE pops up with a ``project'' window. In this window you can choose ``Work
30256573a343132354b122097b0ee1215dda1364Till Mossakowskion'' and ``specification''. Besides the builtin specification ``boolean''
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithere is at least one specification from your development graph that you
30256573a343132354b122097b0ee1215dda1364Till Mossakowskican select for proving. For a structured choice you'll have specifications
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor all underlying nodes that you should work on in a bottom up fashion.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe state created by VSE will be stored in a \texttt{.tar} file (within the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicurrent directory) that preserves proofs for replay later on as long as you
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidon't change library or node names.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{zChaff}
30256573a343132354b122097b0ee1215dda1364Till MossakowskizChaff is a solver for satisfiabily problems of boolean formulas
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(\normalTEXTSC{S}{AT})
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiin CNF. It is connected as a prover for propositional logic to \Hets. The prover
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\SPASS is used to transform arbitrary boolean formulas to CNF. zChaff
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiimplements the \normalTEXTSC{C}{HAFF}\xspace algorithm. We are
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiusing the property, that a conjecture under the assumption of a set of axioms is
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitrue, if the variables of axioms together with the negation of the conjecture
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskihave no satisfying assignment, to prove theorems with zChaff. That is why you see
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe result \normalTEXTSC{U}{NSAT}\xspace in the proof details, if a theorem has been proved
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskito be true. zChaff uses the same ATP GUI as the provers for SoftFOL (ref. to section
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\ref{sec:ATP}). zChaff does not accept any options apart from the time-limit. The
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicurrent integration of zChaff into \Hets has been tested with zChaff 2004.11.15.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{Reduce}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThis is a connection to the computer algebra system from
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\url{http://www.reduce-algebra.com/}. Installation is possible as follows:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{verbatim}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisvn co https://reduce-algebra.svn.sourceforge.net/svnroot/reduce-algebra
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski./configure --with-csl --with-psl
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe binary \texttt{redcsl} will be searched in the \texttt{PATH} or is taken
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifrom the \texttt{HETS\_REDUCE} environment variable.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{Pellet}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiPellet is a popular open-source \DL-reasoner for \SROIQ, which is the logic
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiunderlying OWL 2.0, written in Java. A Java Runtime Environment (in version $> 1.5$)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis needed to run Pellet. For the integration into \Hets the environment variable
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\verb+PELLET_PATH+ has to be set to the root-directory of the Pellet installation.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiPellet uses the same ATP GUI as the provers for SoftFOL (ref. to section
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\ref{sec:ATP}).
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\subsection{Fact++}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiFact++ is a \DL-reasoner for \SROIQ, which is the logic underlying OWL 2.0, written in
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiC++. Fact++ is integrated into \Hets via the OWL-API, which is written in Java.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiA Java Runtime Environment (in version $>= 1.5$) has to be installed. To use Fact++,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe environment variable \verb+HETS_OWL_TOOLS+ has to be set to the directory
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicontaining the files
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski\end{verbatim}
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski\begin{verbatim}
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskion a 32bits-Linux-system or
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiin a 64bits-Linux-system. Fact++ does not support options.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiFact++ uses the same ATP GUI as the provers for SoftFOL (ref. to section
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\ref{sec:ATP}).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\subsection{E-KRHyper}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiE-KRHyper\footnote{\url{http://www.uni-koblenz.de/~bpelzer/ekrhyper/}}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiis an extension of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiKRHyper\footnote{\url{http://www.uni-koblenz.de/~wernhard/krhyper/}} by
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskihandling of equality. E-KRHyper is an automatic first order theorem
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprover and model finder based on the Hyper Tableaux Calculus\cite{Baumgartner:1996}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiE-KRHyper is optimized for being integrated into other systems. In the current
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiimplementation we use a default tactics script, that can be influenced by the user.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe options of E-KRHyper are written in a Prolog-like syntax as in
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till Mossakowski\begin{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski#(set_parameter(timeout_termination_method,0)).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskithe ``.'' at the end of each option is mandatory. To get an overview of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiE-KRHyper's options, run the command
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiin a terminal. Then enter the command
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederat the prompt of E-KRHyper, to display its help information, which is basically
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedera long list of all available parameters. You can exit E-KRHyper by the command
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiE-KRHyper uses the same ATP GUI as the other provers for SoftFOL (ref. to section
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\ref{sec:ATP}).
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\subsection{Darwin}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiDarwin is an automatic first order prover and model finder implementing the Model
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiCalculus\cite{Baumgartner:2003}. The integration of Darwin as a consistency checker
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskisupports the display of models (if they can be constructed) in \CASL-syntax.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederEprover is needed to be in the system-path, if Darwin is used with \Hets, since
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiDarwin uses Eprover for clausification of first-order formulae.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiDarwin supports a wide range of options, to get an overview of them run the command
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiin a terminal.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiDarwin uses the same ATP GUI as the other provers for SoftFOL (ref. to section
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\ref{sec:ATP}).
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\subsection{QuickCheck}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\subsection{minisat}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\subsection{Truth tables}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\subsection{CspCASLProver}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\section{Limits of Hets}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\Hets is still intensively under development. In particular, the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifollowing points are still missing:
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\begin{itemize}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item There is no proof support for architectural specifications.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item Distributed libraries are always downloaded from the local disk,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinot from the Internet.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item Version numbers of libraries are not considered properly.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item The proof engine for development graphs provides only experimental
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisupport for hiding links and for conservativity.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\section{Architecture of Hets}
version, where e.g.\ error handling is ignored. For technical reasons
the static analysis of basic specifications) and/or translates (along
of the \Hets home page at \url{http://www.dfki.de/sks/hets}.
%\input{hets.tex}