UserGuide.tex revision a17349d0247036407c22e632ece0e8f2b736253c
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage[hide]{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 --}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\author{Till Mossakowski, Christian Maeder,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder Mihai Codescu\\[1em]
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiDFKI GmbH, Bremen, Germany.\\[1em]
464c78620a182d2e8fbd125098045eae8788e2bdTill MossakowskiComments to: hets-users@informatik.uni-bremen.de \\
12a1614014912501fbfc30a74242d6f3a5c97e80Till 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 an open source general framework for formal methods
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiintegration and proof management. One can think of \Hets acting like a
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskimotherboard where different expansion cards can be plugged in, the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiexpansion cards here being individual logics (with their analysis and
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiproof tools) as well as logic translations. Individual logics and
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskitheir analysis and proof tools can be plugged into the \Hets
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskimotherboard using an object-oriented interface based on institutions
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\cite{GoguenBurstall92}. The \Hets motherboard already has plugged in
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskia number of expansion cards (e.g., the theorem provers Isabelle, SPASS
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiand more, as well as model finders). Hence, a variety of tools is
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiavailable, without the need to hard-wire each tool to the logic at
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{figure}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{center}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \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
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskidegree of support by \Hets in Fig.~\ref{fig:Languages}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{figure}[ht]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederSPEC ::= BASIC-SPEC
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | SPEC then SPEC
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | SPEC then %implies SPEC
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | 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}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiprescribe the structure of implementations. \emph{Specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski libraries} are collections of named structured and architectural
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederspecifications.
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
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till 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
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\cite{MossakowskiEA06,MossakowskiEtAl07b}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Logics supported by Hets}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe following list of logics (formalized as so-called institutions
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\cite{GoguenBurstall92}) is currently supported by \Hets:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \includegraphics[scale=0.4]{LogicGraph}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\caption{Graph of logics currently supported by \Hets. The more an
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\label{fig:LogicGraph}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{center}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{tabular}{|l|c|c|c|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CoCASL & x & x & - \\\hline
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\ModalCASL & x & x & - \\\hline
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maeder\HasCASL & x & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederHaskell & (x) & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederCspCASL & x & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederCspCASL\_Trace & - & - & x \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederCspCASL\_Failure & - & - & - \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCommonLogic & x & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederConstraint\CASL & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederTemporal & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederRelScheme & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederDFOL & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederExtModal & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLF & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Structured specifications & x & x & (x) \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Architectural specifications & x & x & -\\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\CASLDL & x & - & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederDMU & x & - & - \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiFreeCAD & - & - & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederOWL DL & x & x & x \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederPropositional & x & x & x \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederQBF & x & x & x \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederSoftFOL & x & - & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMaude & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiVSE & x & x & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Isabelle & (x) & - & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHolLight & (x) & - & - \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAdl & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFpl & x & x & - \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederEnCL & x & x & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\caption{Current degree of \Hets support for the different languages. Languages without prover can still ``borrow'' provers
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskivia logic translations.\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
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederthe zChaff SAT solver \cite{Herbstritt03} connected to it.
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\item[QBF] are quantified boolean formulas, with
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederDepQBF \url{http://fmv.jku.at/depqbf/} connected to it.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[RelScheme] is a logic for relational databases \cite{DBLP:journals/ao/SchorlemmerK08}.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item[SoftFOL] \cite{LuettichEA06a} offers several automated theorem
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski proving (ATP) systems for first-order logic with equality: \begin{inparaenum}[(1)]\item \SPASS
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \cite{WeidenbachEtAl02}, see \url{http://www.spass-prover.org};
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item Vampire \cite{RiazanovV02} see \url{http://www.vprover.org};
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item Eprover \cite{Schulz:AICOM-2002}, see {http://www.eprover.org};
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item E-KRHyper \cite{DBLP:conf/cade/PelzerW07}, see {http://www.uni-koblenz.de/~bpelzer/ekrhyper}, and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski MathServe Broker\footnote{which chooses an appropriate ATP upon a
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski classification of the FOL problem} \cite{ZimmerAutexier06}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{inparaenum}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski These together comprise some of the most advanced theorem provers
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski for first-order logic. SoftFOL is essentially the first-order
30256573a343132354b122097b0ee1215dda1364Till Mossakowski interchange language TPTP \cite{DBLP:conf/lpar/Sutcliffe10},
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski for higher-order logic.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[HolLight] \url{http://www.cl.cam.ac.uk/~jrh13/hol-light/}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski is John Harrison's interactive theorem prover
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski for higher-order logic.
30256573a343132354b122097b0ee1215dda1364Till 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.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Moreover, LF can be used as a logical framework to add new logics in Hets \cite{CHK+2011a}.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder Logic definitions in LF are based in the logic atlas of the Latin project \cite{project:latin}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder and therefore the environment variable \verb+LATIN_LIB+ must be set to the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski repository with the Latin logic definitions.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian 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
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder designed for requirements engineering of business rules
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder \url{https://lab.cs.ru.nl/BusinessRules/Requirements_engineering}.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\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
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder algebra systems Mathematica, Maple and Reduce.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[THF] is an interchange language for higher-order logic
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \cite{DBLP:conf/cade/BenzmullerRS08}, similar to what TPTP
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder is for first-order logic. \Hets connects THF to the automated
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder higher-order prover Leo-II.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\end{description}
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederVarious logics are supported with proof tools. Proof support for the
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian 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
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiexplain 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
17787092f1a5f5d16445e8293fd4bcde69e3fc81Mihai Codescuis the \HetCASL language summary \cite{Mossakowski04}; a formal
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskisemantics as well as a user manual with more examples are in preparation.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiSome of \HetCASL's heterogeneous constructs will be illustrated
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederin Sect.~\ref{sec:HetSpec} below.
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder\section{Logic translations supported
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\label{comorphisms}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederLogic translations (formalized as institution comorphisms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{GoguenRosu02}) translate from a given source logic to a given
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitarget logic. More precisely, one and the same logic translation
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskimay have several source and target \emph{sub}logics: for
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luetticheach source sublogic, the corresponding sublogic of the target
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskilogic is indicated.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiA graph of the most important logics and sublogics, together with their
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\begin{figure}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder \begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \includegraphics[scale=0.4]{SublogicGraph}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\caption{Graph of most important sublogics currently supported by \Hets,
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskitogether with their comorphisms.}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\label{fig:SublogicGraph}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiIn more detail, the following list of logic translations is currently
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskisupported 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
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL2HasCASL & inclusion \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL2Isabelle & inclusion on sublogic CFOL=
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(translation $(7)$ of \cite{Mossakowski02}) \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL2Modal & inclusion \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederCASL2PCFOL & coding of subsorting (SubPCFOL=) by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual} \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederCASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
c5e63ec138b908ac9d15e6843120033bf36a1862Till Mossakowskipredicates for the subsorts \\\hline
c488ac18796ad6383b1edf7fa2820edc8296c89eChristian MaederCASL2Propositional & translation of propositional FOL \\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichCASL2SoftFOL & coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maedermapping 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
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL2SubCFOL & coding of partial functions by error elements
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting, i.e. sublogic SubPCFOL=) \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL2VSE & inclusion on sublogic CFOL= \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2VSEImport & inclusion on sublogic CFOL= \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2VSERefine & refining translation of CASL.CFOL= to VSE \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL\_DL2CASL & inclusion \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCoCASL2Isabelle & extended translation similar to CASL2Isabelle \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCommonLogic2CASL & Coding Common Logic to \CASL.Module elimination
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski is applied before translating to \CASL. \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederCommonLogic2CASLCompact & Coding compact Common Logic to \CASL.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Compact Common Logic is a sublogic of Common Logic
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski where no sequence markers occur. Module elimination
30256573a343132354b122097b0ee1215dda1364Till Mossakowski is applied before translating to \CASL. We recommend
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder using this comorphism whenever possible because it
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski results in simpler specifications.\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCommonLogicModuleElimination & Eliminating modules from a Common Logic theory
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder resulting in an equivalent specification without
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder modules. \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederCspCASL2CspCASL\_Failure & inclusion \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederCspCASL2CspCASL\_Trace & inclusion \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederCspCASL2Modal & translating the CASL data part to ModalCASL \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederDFOL2CASL & translating dependent types \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederDMU2OWL & interpreting Catia output as OWL \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\begin{tabular}{|l|p{7cm}|}\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederHasCASL2HasCASLNoSubtypes & coding out subtypes \\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederHasCASL2HasCASLPrograms & coding of \HasCASL axiomatic recursive definitions
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederas \HasCASL recursive program definitions \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederHasCASL2IsabelleOption & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederHaskell2Isabelle & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07} \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederHolLight2Isabelle & coding of HolLight to Isabelle/HOL \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederMaude2CASL & encoding of rewrites as predicates \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiModal2CASL & the standard translation of modal logic
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskito first-order logic \cite{blackburn_p-etal:2001a} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiOWL2CASL & inclusion \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiOWL2CommonLogic & inclusion \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPropositional2CASL & inclusion \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiPropositional2QBF & inclusion \\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichQBF2Propositional & inclusion \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiRelScheme2CASL & inclusion \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Getting started}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe latest \Hets version can be obtained from the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets tools home page
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Since \Hets is being
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets is currently available (on Intel architectures only) for Linux
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThere are several possibilities to install \Hets.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{enumerate}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe best support is currently given via Ubuntu packages.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-add-repository ppa:hets/hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-add-repository \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski "deb http://archive.canonical.com/ubuntu lucid partner"
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-get update
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-get install hets
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{verbatim}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThis 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote 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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{libglade2} package (and all its dependencies) yourself. In order to
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederspeed this up we provide a meta package \texttt{libglade2.mpkg}, too.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe installer will lead you through the installation with
30256573a343132354b122097b0ee1215dda1364Till Mossakowskia graphical interface. It will download and install further
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisoftware (if not already installed on your computer):
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{tabular}{|l|l|p{5cm}|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiTcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiDarwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiIf you do not have Sun Java, you can just download the hets binary.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiYou have to unpack it with \texttt{bunzip2} and then put it at
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedersome place coverd by your \texttt{PATH}. You also have to
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiinstall the above mentioned software and set
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiseveral environment variables, as explained on the installation page.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederYou may compile \Hets from the sources (they are licensed under GPL),
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiplease follow the
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskilink ``Hets: source code and information for developers''
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederon the \Hets web page, download the sources (as tarball or from
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskisvn), and follow the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederinstructions in the \texttt{INSTALL} file, but be prepared to take some time.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{enumerate}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDepending on your application further tools are supported and may be
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinstalled in addition:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{tabular}{|l|l|p{5cm}|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskizChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiminisat & SAT solver & \url{http://minisat.se/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiPellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
30256573a343132354b122097b0ee1215dda1364Till MossakowskiE-KRHyper & theorem prover
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederReduce & computer algebra system
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder & \url{http://www.reduce-algebra.com/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiVSE & theorem prover & (non-public) \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiTwelf & & \url{http://twelf.plparty.org/} \\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\section{Analysis of Specifications}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederConsider the following \CASL
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{BIGEXAMPLE}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\I\SPEC \NAME{Strict\_Partial\_Order} =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\PRED]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\SORT \( Elem \)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\(\[ \FORALL x,y,z : Elem \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\begin{COMMENT}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiNote that there may exist \(x, y\) such that\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskineither \(x < y\) nor \(y < x\).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{BIGEXAMPLE}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets can be used for parsing and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskichecking static well-formedness of specifications.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{parsing}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{static!analysis}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederwith the \Hets distribution as \texttt{Hets-lib/UserManual/Chapter3.casl}).
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThen you can check the well-formedness of the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification by typing (into some shell):
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets checks both the correctness of this specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski with respect to the \CASL syntax, as
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederwell as its correctness with respect to the static semantics (e.g.\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederwhether all identifiers have been declared before they are used,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederwhether operators are applied to arguments of the correct sorts,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederwhether the use of overloaded symbols is unambiguous, and so on).
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe following flags are available in this context:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski for prototyping issues, namely to quickly produce a development graph
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski showing the dependencies among the specifications (cf.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Sect.~\ref{sec:DevGraph}) even if the individual specifications are
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder not correct yet.
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill 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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski algorithm for \CASL logic; it is a comma-separated list of zero or
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski more of the following options:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \item[\texttt{sharing}] perform sharing analysis for sorts,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder operations and predicates.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski check (\texttt{cell} option), but may prove more efficient in case
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski of certain specifications.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski If \texttt{ANALYSIS} is empty then amalgamability analysis for
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \CASL is skipped.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski The default value for \texttt{--casl-amalg} is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{cell}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\Hets accepts plain text input files with the following endings:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{tabular}{|l|c|c|}\hline
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiEnding & default logic & structuring language\\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{.hol} & HolLight & HolLight \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{.hs} & Haskell & Haskell \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{.owl} & OWL DL, OWL Lite & OWL \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{.elf} & LF & Twelf \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{.clf} or \texttt{.clif} & CommonLogic & \CASL \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{.maude} & Maude & Maude \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiFurthermore, \texttt{.xml} files are accepted as Catia output if the default
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskilogic is set to DMU before a library import or by the ``\texttt{-l DMU}''
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskicommand line option of \Hets. In all other cases \texttt{.xml} files are
3532dcfda4dd76997072fcda24e75c305d105233Till 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;
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskithese 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
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskifor the data part and a \Csp process built over this data part.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{data} as follows:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary Buffer
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder free type List[Elem] ::= nil | cons(Elem; List[Elem])
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder ops last: List -> ? Elem;
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder rest: List -> ? List
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder channel read, write : Elem
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder process Buf(List): read, write, List;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski EmptyBuffer : read,write, List;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Buf(l)= read? x :: Elem -> Buf(cons(x,nil)) []
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if l=nil then STOP else
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski write!last(l) -> Buf(rest(l)))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski EmptyBuffer = Buf(nil)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHere, the construct \texttt{data List} refers to the \CASL specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{List}, which is implicitly embedded into \CspCASL.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe ending \texttt{.hs} is available for directly reading in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell programs % and HasSLe specifications,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand hence supports the Haskell module system.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe logic Haskell has to be chosen explicitly, and the \CASL structuring
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisyntax needs to be used:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary Factorial
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispec Factorial =
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfac :: Int -> Int
5277e290ad70afdf97f359019afd8fb5816f4102Till 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.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederA development graph consists of a set of nodes (corresponding to whole
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederstructured 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiassociated 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
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\emph{local} (drawn as dashed arrows): a global theorem link
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipostulates that all axioms of the source node (including the inherited
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBoth definition and theorem links can be \emph{homogeneous},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskii.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe logic changes along the arrow. Technically, this is the case
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifor Grothendieck signature morphisms $(\rho,\sigma)$ where
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$\rho\not=id$. This case is indicated with double arrows.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiTheorem links are initially displayed in red.
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinode is turned into green. This implementation ultimately is based
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskion a theorem \cite{Habil} stating soundness and relative completeness
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the proof calculus for heterogeneous development graphs.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following options let \Hets show the development graph of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia specification library:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-u}, \texttt{--uncolored}] no colors in shown graphs
5277e290ad70afdf97f359019afd8fb5816f4102Till 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.
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill 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 usually 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder 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} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{Natural}} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y:Nat \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederproof obligations arising from a specification. This can be done with:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{hets -g Order.casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidenotes a proof obligation (corresponding to the view).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis proof obligation needs to be discharged in order to
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedershow that the view is well-formed (then its color turns into green).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAs a more complex example, consider the following loose specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof a sorting function, taken from the \CASL User Manual
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\cite{CASL-UM}, Chap.~6:
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\begin{BIGEXAMPLE}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\I\SPEC \NAMEREF{List\_Order\_Sorted}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\begin{ITEMS}[\WITHIN]
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\begin{ITEMS}[\PRED]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\PRED \( \_\_is\_sorted : List \)
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\(\[ \FORALL e,e': Elem; L : List \\
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \. empty~is\_sorted \\
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \. cons(e,empty)~is\_sorted \\
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \. cons(e,cons(e',L))~is\_sorted \IFF
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\OP]
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\I\OP \( order : List \TOTAL List \)
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\end{BIGEXAMPLE}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederThe following specification of sorting by insertion also is taken from
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe \CASL User Manual \cite{CASL-UM}, Chap.~6:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{BIGEXAMPLE}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\I\SPEC \NAMEREF{List\_Order}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\phantomsection
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\WITHIN]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{ITEMS}[\OP]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\I\OP \( insert : Elem \* List \TOTAL List \)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\(\[ \FORALL e,e':Elem; L:List \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu \ELSE cons(e, cons(e',L)) \] \\
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\begin{ITEMS}[\OP]
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\I\OP \( order : List \TOTAL List \)
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\(\[ \FORALL e:Elem; L:List \\
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu \. order(empty) = empty \\
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder \. order(cons(e,L)) = insert(e, order(L)) \]\)
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\end{BIGEXAMPLE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBoth specifications are related. To see this, we first inspect
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedertheir signatures. This is possible with:
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\texttt{hets -g Sorting.casl}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederassuming that \texttt{Sorting.casl} contains the above specifications.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\begin{figure}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\begin{center}
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\includegraphics[scale=0.7]{dg-order-1}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuIn the above-mentioned development graph, we have two types of nodes.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe named ones correspond to named specifications, but there
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuare also unnamed nodes corresponding to anonymous basic
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederspecifications like the declaration of the $insert$ operation in
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\NAMEREF{List\_Order} above. Basically, there is an
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederunnamed node for each structured specification that is not named.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederAgain, the black arrows denote an ordinary import of specifications
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu(corresponding to the extensions and unions in the
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuspecifications), while the blue arrows denote hiding (corresponding to
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuthe local specification).
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuBy clicking on the nodes, one can inspect their signatures.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\NAMEREF{List\_Order} have the same signature. Hence, it
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis legal to add a view:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederWe have already added this view to \texttt{Sorting.casl}.
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai CodescuThe corresponding
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederproof obligation between \NAMEREF{List\_Order\_Sorted} and
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescu\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu as a red arrow.
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederHere is a summary of the types of nodes and links occurring in
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederdevelopment graphs:
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\begin{description}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Named nodes] correspond to a named specification.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Unnamed nodes] correspond to an anonymous specification.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item[Elliptic nodes] correspond to a specification in the current library.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Rectangular nodes] are external nodes corresponding to a specification
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu downloaded from another library.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Red nodes] have open proof obligations.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Yellow nodes] have an open conservativity proof obligations.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Green nodes] have all proof obligations resolved.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Black links] correspond to reference to other specifications (definition
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder links in the sense of \cite[IV:4]{CASL/RefManual}).
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Red links] correspond to open proof obligations (theorem links).
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Green links] correspond to proven theorem links.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Yellow links] correspond to proven theorem links with open
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder conservativity or to open hiding theorem links.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Blue links] correspond to hiding, free, or cofree definition links.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Violett links] correspond to a mixture of links becoming visible after
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ``expand'' or ``Show unnamed nodes with open proofs''.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Solid links] correspond to global (definition or theorem)
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codesculinks in the sense of \cite[IV:4]{CASL/RefManual}.
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\item[Dashed links] correspond to local (theorem) links in the sense of
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder \cite[IV:4]{CASL/RefManual}. These are usually created after
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder ``Global-Decomposition'' or only be visible after ``Show newly added proven
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Single line links] have homogeneous signature morphisms (staying within
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu one and the same logic).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Double line links] have heterogeneous signature morphisms (moving
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder between logics).
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\end{description}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiWe now explain the menus of the development graph window.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiMost of the pull-down menus of the window are uDraw(Graph)-specific
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescutheir function can be looked up in the uDraw(Graph) documentation\footnote{see
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe exception is the Edit menu. Moreover, the nodes and links
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiof the graph have attached pop-up menus, which appear when
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederclicking with the right mouse button.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\begin{description}
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\item[Edit] This menu has the following submenus:
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\begin{description}
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\item[Undo] Undo the last development graph proof step (see under Proofs)
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\item[Redo] Restore the last undone development graph proof step (see
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder under Proofs)
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe ``Hide/show names/nodes/edges'' menu is a toggle:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiyou can switch on or off the display of node names, unnamed nodes or
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuproven theorem links.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuWith the ``Hide/show internal node names'' option, the nodes that
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuare initially unnamed get derived names.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuWith the ``Hide/show unnamed nodes without open proofs'' option, it is possible
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuto reveal the unnamed nodes which do not have open proof goals.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuInitially, the complexity of the graph is reduced by hiding all these nodes;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskionly nodes corresponding to named specifications are displayed.
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus LuettichPaths between named nodes going through unnamed nodes
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiare displayed as edges; these paths are then expanded when showing the
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuunnamed nodes.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuWhen applying the development graph calculus rules, theorem links that have
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskibeen proven are removed from the graph. With the ``Hide/Show newly added
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproven edges'' option, it is possible to re-display these links; they are marked
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskias proven in the link info (see \emph{Pop-up menu for links}, below).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Focus node]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThis menu is particularly useful when navigating in a large development graph,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiwhich does not fit on a single screen. The list of all nodes is displayed:
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuthe nodes are identified by the internal node number and the internal node name.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuOnce a node is selected, the view centers on it.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Select Linktypes]
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederThis menu allows to select the type of links that are displayed in the
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederdevelopment graph. A selection window appears, where links are grouped into
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederthree categories: definition links, proven theorem links and unproven
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedertheorem links. It is possible to select/deselect all links or to invert the
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maedercurrent selection.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Consistency checker]
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder Checks whether the theories of the nodes of the graph are consistent
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder i.e. have a model. The model finders currently interfaced are
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder Isabelle-refute, darwin and E-KRHyper, with best support for darwin.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Proofs] This menu allows to apply some of the deduction rules
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder for development graphs, see Sect. IV:4.4 of the \CASL Reference
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder Manual \cite{CASL/RefManual} or one of
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}. While support for
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder local and global (definition or theorem) links is stable, support
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder for hiding links and checking conservativity is still experimental.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder In most cases, it is advisable to use ``Auto-DG-Prover'', which
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder automatically applies the rules in the correct order. As a result,
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder the open theorem links (marked in red) will be reduced to local
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder proof goals, that is, they become green, and instead, some target nodes
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder may get red, indicating open local proof goals.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder Besides the deduction rules, the menu contains entries for computing
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder a colimit approximation for the development graph and for
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder computing normal forms of all nodes (needed when dealing with hiding).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Also, a \CASL-specific normalisation of free links has been
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Dump Development Graph] This option is available only for
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski 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}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Pop-up menu for nodes]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederHere, the number of submenus depends on the type of the node:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Show node info] Shows the local informations of the node: the internal
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder node name and node number, the xpath that denotes the location of the node
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski within an XML representation, information about consistency of the node,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski 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
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiimported from other nodes). Notice that axioms imported via hiding links
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederare not part of the theory; they can be made visible only by re-adding
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskithe hidden symbols, using the normal form of the node, by calling
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\emph{Proofs/Compute Normal Form}. For such nodes, a warning is displayed.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Translate theory] Translates the theory of a node to another logic.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederA menu with the possible translation paths will be displayed.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder of the signature of the node.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Show proof status] Show open and proven local proof goals.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Prove VSE structured] Allows to send a development graph below the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder current node to the interactive \texttt{hetsvse} prover if that binary is
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder available, see \ref{subsec:VSE}.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\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
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski goal is disproven.)
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Add sentence] This menu allows to add a sentence on the fly. The
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (possibly named) sentence will be parsed and analysed using the underlying logic.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Check consistency] Simply calls the global ``Consistency checker'' menu
30256573a343132354b122097b0ee1215dda1364Till Mossakowski for the current node, see \ref{sec:CC}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Check conservativity] Checks conservativity of the inclusion
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski morphism from the empty theory to the theory of the node (see
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder {\bf Check conervativity} for edges).
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\end{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederFor the nodes which are references to specifications from an external library,
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederthe pop-up menu options are reduced to {\bf Show node info, Show theory,
30256573a343132354b122097b0ee1215dda1364Till MossakowskiShow proof status} and {\bf Prove} and moroever, the option {\bf Show
30256573a343132354b122097b0ee1215dda1364Till Mossakowskireferenced library} is added: on selection, it displays in a new window
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe development graph of the external library from which the specification has
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskibeen downloaded.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Pop-up menu for links]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiAgain, the number of submenus depends on the type of the link:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{description}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Show info] Shows informations about the edge: internal number and
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiinternal nodes it links, the link type and origin and the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskisignature morphism of the link. The latter consists
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiof two components: a logic translation and a signature morphism in the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskitarget logic of the logic translation.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIn the (most frequent) case
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiof an intra-logic signature morphism, the logic translation component is
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskijust the identity.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Check conservativity] (Experimental) Check whether the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskitheory of the target node of the link
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederis a conservative extension of the theory of the source node.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Expand]This menu is available only for paths going through unnamed
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedernodes which are not displayed and it expands the path to the links forming it.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\end{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederBesides development graphs there are library graph windows displaying the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilibrary hierarchy. The Edit menu has the following submenus:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Edit] This menu for library graphs has the following submenus:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Reload Library] Reloads all \HetCASL sources in order to avoid closing
30256573a343132354b122097b0ee1215dda1364Till Mossakowski and restarting the application after sources have changed. However, all
30256573a343132354b122097b0ee1215dda1364Till Mossakowski previous proof steps will be lost, therefore you have to confirm this
30256573a343132354b122097b0ee1215dda1364Till Mossakowski action. (A change management tool to keep proofs is in preparation.)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\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
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich original state and proof steps will be lost, therefore you have to confirm
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Show Logic Graph] Shows the graph of logics and logic comorphisms
30256573a343132354b122097b0ee1215dda1364Till Mossakowski currently supported by \Hets. The Edit menu of a logic graph window has the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder following submenu:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[Show detailed logic graph] Shows the important sublogics and comorphims
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder between them, i.e. translation (blue links) and inclusion (black links).
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\end{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\end{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\end{description}
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski\section{Reading, Writing and Formatting}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\Hets provides several options controlling the types of files
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowskithat are read and written.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify \texttt{ITYPE}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder as explicit type of the input file. By default \texttt{env}, \texttt{casl},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski or \texttt{het} extensions are tried in this order. An \texttt{env} file
30256573a343132354b122097b0ee1215dda1364Till Mossakowski contains a shared ATerm of a development graph, whereas \texttt{casl} or
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \texttt{het} files contain plain \HetCASL text. An \texttt{env} file will
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder always be read if it exists and is consistent (aka newer) than the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder corresponding \HetCASL file.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \texttt{exp} files contain a development graph in a new experimental omdoc
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder format. \texttt{prf} files contain additional development steps (as shared
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder ATerms) to be applied on top of an underlying development graph created from
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder a corresponding \texttt{env}, \texttt{casl}, or \texttt{het}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder file. \texttt{hpf} files are plain text files representing heterogeneous
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder proof scripts. The contents of a \texttt{hpf} file must be valid input for
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \Hets in interactive mode. (\texttt{gen\_trm} formats are currently not
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe possible input types are:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski | [tree.]gen_trm[.baf]
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{verbatim}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSpecify \texttt{DIR} as destination directory for output files.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\texttt{OTYPES} is a comma separated list of output types:
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\begin{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich | (sig|th)[.delta]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich | pp.(het|tex|xml|html)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\end{verbatim}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe \texttt{env} and \texttt{prf} formats are for subsequent reading,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiavoiding the need to re-analyse downloaded libraries. \texttt{prf} files
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskican 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.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedermarkup format and data model for Open Mathematical Documents. It
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederserves as semantics-oriented representation format and ontology
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederlanguage for mathematical knowledge. Currently, \CASL specifications
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedercan be output in this format; support for further logics is planned.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe \texttt{xml} option will produce an XML-version of the development graph
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederfor our change management broker.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe \texttt{exp} format is the new experimental omdoc format.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe \texttt{hs} format is used for Haskell modules. Executable \CASL or
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\HasCASL specifications can be translated to Haskell.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederWhen the \texttt{thy} format is selected, \Hets will try to translate
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedereach specification in the library to \Isabelle, and write one \Isabelle
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\texttt{.thy} file per specification.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederWhen the \texttt{comptable.xml} format is selected, \Hets will extract
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthe composition and inverse table of a Tarskian relation algebra from
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederspecification(s) (selected with the \texttt{-n} or \texttt{--spec}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederoption). It is assumed that the relation algebra is
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedergenerated by basic relations, and that the specification is written
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederin the \CASL logic. A sample specification of a relation
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederalgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederavailable from \texttt{www.cofi.info/Libraries}.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe output format is XML, the URL of the DTD is included in the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe \texttt{sig} or \texttt{th} option will create \HetCASL signature or
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedertheory files for each development graph node. (The \texttt{.delta} extension
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederis not supported, yet.)
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe \texttt{pp} format is for pretty printing, either as plain text
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder(\texttt{het}), \LaTeX input (\texttt{tex}), HTML (\texttt{html}) or XML
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder(\texttt{xml}). For example, it is possible to generate a pretty printed
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\LaTeX\ version of \texttt{Order.casl} by typing:
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThis will generate a file \texttt{Order.pp.tex}. It can be included
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedercoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe format \texttt{pp.xml} represents just a parsed library in XML.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederFormats with \texttt{graph} are for future usage.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe \texttt{dfg} format is used by the \SPASS theorem prover
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\cite{WeidenbachEtAl02}.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederformat for first-order theorem provers.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederAppending \texttt{.c} to \texttt{dfg} or \texttt{tptp} will create files for
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederconsistency checks by SPASS or Darwin respectively.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederFor all output formats it is recommended to increase the verbosity to at least
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederlevel 2 (by using the option \texttt{-v2}) to get feedback which files are
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederactually written. (\texttt{-v2} also shows which files are read.)
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederchooses a translation option. \texttt{TRANS} is a colon-separated list
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederwithout 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
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-w NVIEWS}, \texttt{--view=NVIEWS}]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskichooses a list of named views for processing
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-R}, \texttt{--recursive}] output also imported libraries
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-I}, \texttt{--interactive}] run \Hets in interactive mode
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[\texttt{-X}, \texttt{--server}] run \Hets as web server (see
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder \ref{sec:Server})
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item[\texttt{-x}, \texttt{--xml}] use xml-pgip packets to communicate with
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder \Hets in interactive mode
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item[\texttt{-S PORT}, \texttt{--listen=PORT}] communicate
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder with \Hets in interactive mode vy listining to the port \texttt{PORT}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item[\texttt{-c HOSTNAME:PORT}, \texttt{--connect=HOSTNAME:PORT}] communicate
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder with \Hets in interactive mode via connecting to the port on host
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder \texttt{HOSTNAME}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item[\texttt{-d STRING}, \texttt{--dump=STRING}] produces implementation
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder dependent output for debugging purposes only
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder (i.e.\ \texttt{-d LogicGraph} lists the logics and comorphisms)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{description}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\section{Hets as a web server}\label{sec:Server}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichLarge parts of \Hets are now also available via a web interface. A running
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichserver should be accessible on
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\url{http://pollux.informatik.uni-bremen.de:8000/}. It allows to browse the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\Hets library, upload a file or just a \HetCASL specification. Development
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichgraphs for well-formed specifications can be displayed in various formats
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichwhere the \texttt{svg} format is supposed to look like the graphs displayed by
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichuDrawGraph. Besides browsing, the web server is supposed to be accessed by
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichother programs using queries. The possible queries are described on
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\url{http://trac.informatik.uni-bremen.de:8080/hets/wiki/RESTfulInterface}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichA development graph is addressed by the \emph{path} following the port number
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichand the slash of the URL, i.e.\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\url{http://localhost:8000/Basic/Numbers.casl}. Once a development has been
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcreated it can be accessed via a (fairly unique) session id (consisting of
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichnine digits) that can be used as \emph{path}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichA \emph{path} may be followed by a query string that begins with a question
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichmark and consists of \emph{entries} (usually field-value pairs) separated by
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichampersands. The queries control the information to be extracted from the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichdevelopment graph given by the \emph{path} or they allow to perform commands
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichUsually, query string are made up of \texttt{field=value} pairs, but in some
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcases the field name or the value may be omitted and in that case the equal
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsign must be omitted, too.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichFor instance strings denoting formats, like \texttt{xml}, \texttt{svg},
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\texttt{pdf}, etc., do not need to be preceded by \texttt{format=}. Some
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichformats, like \texttt{pdf}, only pretty print specification and
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichbasically ignore the underlying development graph.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichA special \emph{entry} is just \texttt{session} which only returns a fresh
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsession id for a development graph that is given by a file name, i.e.\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\url{http://localhost:8000/Basic/Numbers.casl?session}. These session ids must
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichbe used to perform commands (of the development graph calculus) that
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\emph{change} the underlying graph.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichGiven a graph, nodes and edges can be addressed by numbers via entries like
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\texttt{node=0} or \texttt{edge=0}. (Nodes can also be given by name.) For
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichnodes, prover actions are possible by further
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichentries. \url{http://localhost:8000/123456789?prove=Nat\_\_E1\&prover=SPASS\&timeout=5}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichwould try to prove the goals of the node \texttt{Nat\_\_E1} using the prover
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\texttt{SPASS} with a timeout of 5 seconds for the development graph that
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichhappened to have the (unlikely) session id \texttt{123456789}. Individual
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichgoals can be given via a \texttt{theorems} field and special translations by a
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\texttt{translation} field. The available provers and translations can be
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichqueried by \texttt{?node=0\&translations} and \texttt{?node=0\&provers} or
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskishorter by \texttt{?translations=0} and \texttt{?provers=0}, where instead of
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskithe node number (here \texttt{0}) also a node name can be used.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\section{Miscellaneous Options}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{description}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichSet 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).
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThis 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.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-e ENCODING}, \texttt{--encoding=ENCODING}] Read input files using latin1 or utf8 encoding. The default is still latin1.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\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.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-U FILE}, \texttt{--xupdate=FILE}] update a development graph according to special xml update information (still experimental).
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{description}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\section{Proofs with \Hets}\label{sec:Proofs}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe proof calculus for development graphs (Sect.~\ref{sec:DevGraph}) reduces
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichglobal theorem links to local proof goals. Local proof goals (indicated by red
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichnodes in the development graph) can be eventually discharged using a theorem
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichprover, i.e. by using the ``Prove'' menu of a red node.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe graphical user interface (GUI) for calling a prover is shown in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichFig. \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 `-'
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichindicates a disproved goal, a space denotes an open goal, and a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski`$\times$' denotes an inconsistent specification (aka a fallen `+';
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedersee below for details).
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski launched and the theory along with the selected goals is translated via the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski shortest possible path of comorphisms into the provers logic.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item The pop-up choice box below `Selected comorphism path:' lets you pick a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (composed) comorphism to be used for the chosen prover.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item Since the amount and kind of sentences sent to an ATP system is a major
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski factor for the performance of the ATP system, it is possible to select in
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski the bottom lists the axioms and proven theorems that will comprise the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski theory of the next proof attempt. Based on this selection the sublogic may
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski vary and also the available provers and comorphisms to provers. Former
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski theorems that are imported from other specifications are marked with the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski prefix `(Th)'. Since former theorems do not add additional logical content,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski they may be safely removed from the theory.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item If you press the bottom-right `Close' button the window is closed and
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski the status of the goals' list is integrated into the development graph. If
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski all goals have been proved, the selected node turns from red into green.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item All other buttons control selecting list entries
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\subsection{Consistency Checker}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\label{sec:CC}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederSince 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
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederthe `Edit' menu as it operates on all nodes.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe list on the left shows all node names prefixed with a consistency status
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiin square brackets that is initially empty. A consistent node is indicated by
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskia `+', a `-' indicates an inconsistent node, a `t' denotes a timeout of the last
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskichecking attempt.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{figure}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\includegraphics[width=\textwidth]{ConsistencyChecker}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\caption{Hets Consistency Checker Interface\label{fig:cons_window}}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiFor some selection of nodes (of a common logic) a model finder should be
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiselectable from the `Pick Model finder:' list. Currently only for ``darwin''
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskisome \CASL models can be re-constructed. When pressing `Check', possibly after
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski`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'
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder(Fig. \ref{fig:cons_res}) will pop up and allow you to inspect the models for
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedernodes, if they could be constructed.
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder\begin{figure}
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder\includegraphics[width=\textwidth]{ConsCheckResults}
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder\caption{Consistency Checker Results\label{fig:cons_res}}
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder\subsection[Automated Theorem Proving Systems]
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder{Automated Theorem Proving Systems\\(Logic SoftFOL)}
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder\label{sec:ATP}
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder\begin{figure}
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke\includegraphics[width=\textwidth]{spassGUI1}
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke\caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederAll ATPs integrated into \Hets share the same GUI, with only a slight
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedermodification for the MathServe Broker: the input field for extra options is
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederinactive. Figure~\ref{fig:SPASS_GUI} shows the instantiation for \SPASS, where
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckein the top right part of the window the batch mode can be controlled. The
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederleft side shows the list of goals (with status indicators). If goals are
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecketimed out (indicated by `t') it may help to activate the check box `Include
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckepreceeding proven theorems in next proof attempt' and pressing `Prove all'
f8a33e72909e67885a9ecbae881fc75134c362cbDominik LueckeOn the bottom right the result of the last proof
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckeattempt is displayed. The `Status:' indicates `Open', `Proved', `Disproved',
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski`Open (Time is up!)', or `Proved (Theory inconsistent!)'. The list of `Used
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian MaederAxioms:' is filled by \SPASS. The button `Show Details' shows the whole output
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maederof the ATP system. The `Save' buttons allow you to save the input and
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maederconfiguration of each proof for documentation. By `Close' the results for all
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maedergoals are transferred back to the Proof Management GUI.
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian MaederThe MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian MaederZimmer provides a unified interface to a range of different ATP
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maedersystems; the most important systems are listed in
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian MaederTable~\ref{tab:MathServe}, along with their capabilities. These
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maedercapabilities are derived from the \emph{Specialist Problem Classes}
a05d3f31f5b28c68df892a785c1adb870ae430d7Christian Maeder(SPCs) defined upon the basis of logical, language and syntactical
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maederproperties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian MaederOnly two of the Web services provided by the MathServe system are used
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiby \Hets currently: Vampire and the brokering system. The ATP systems
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederare offered as Web Services using standardized protocols and formats
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maedersuch 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.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\begin{table}[t]
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \begin{threeparttable}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \begin{tabular}{|l|c|p{7cm}|}\firsthline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder ATP System & Version & Suitable Problem Classes\tnote{a}\\
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder \hhline{|=|=|=|}
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder DCTP & 10.21p & effectively propositional \\\hline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke EP & 0.91 & effectively propositional; real first-order, no
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke 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
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke 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}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke %\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}
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder \end{threeparttable}
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder \caption{ATP systems provided as Web services by MathServe}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\vspace*{-4mm}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \label{tab:MathServe}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\subsubsection*{\SPASS}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeThe ATP system \SPASS \cite{WeidenbachEtAl02} is a resolution-based
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeprover for first-order logic with equality. Furthermore, it provides a soft
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecketyping mechanism with subsorting that treats sorts as unary
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederpredicates. The ATP \SPASS should be installed locally and available
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckethrough 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.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\subsubsection*{MathServe Broker}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke% The classes ``effectively propositional'' and ``real first-order''
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski% apply to first-order problems that are distinguished by the finiteness
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder% of the Herbrand universe; an effectively propositional problem has
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke% only constants (generated by finitely many terms) whereas a real
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke% first-order problem contains true functions with an infinite Herbrand
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederThe brokering service chooses the most appropriate ATP system
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeupon a classification based on the SPCs, and on a training with the
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckelibrary Thousands of Problems for Theorem Provers (TPTP)
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\cite{ZimmerAutexier06}. The TPTP format
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckehas been introduced by Sutcliffe and Suttner for the annual
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckecompetition CASC \cite{Sutcliffe:2006:CASC} and provides a unified
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckesyntax for untyped FOL with equality, but without any symbol
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\subsection{Isabelle}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\Isabelle \cite{NipPauWen02} is an interactive theorem prover, which is
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maedermore powerful than ATP systems, but also requires more user interaction.
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederhas a very small core guaranteeing correctness, and its provers,
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskilike the simplifier or the tableaux prover, are built on top of this
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicore. Furthermore, there is over fifteen years of experience with it,
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskiand several mathematical textbooks have been partially
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski \index{formal!verification}%
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\Isabelle is a tactic based theorem prover implemented in standard ML.
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiThe main \Isabelle logic (called Pure) is some weak intuitionistic type
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskitheory with polymorphism. The logic Pure is used to represent a
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskivariety of logics within \Isabelle; one of them being \HOL (higher-order
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskilogic). For example, logical implication in Pure (written
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\texttt{==>}, also called meta-implication), is different from logical
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskiimplication in \HOL (written \texttt{-->}, also called object
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiIt is essential to be aware of the fact that the \Isabelle/\HOL logic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis different from the logics that are encoded into it via comorphisms.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederTherefore, 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat are not present in an input logic like \CASL.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Isabelle is started with ProofGeneral
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{url:Emacs,url:XEmacs}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe \Isabelle theory file conforms to the Isabelle/Isar syntax
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{NipPauWen02}. It starts with the theory (encoded along the selected
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski comorphism), followed by a list of theorems. Initially, all the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski theorems have trivial proofs, using the `oops` command. However, if
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski you have saved earlier proof attempts, \Hets will patch these into
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski the generated \Isabelle theory file, ensuring that your previous work
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski 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
30256573a343132354b122097b0ee1215dda1364Till Mossakowski 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthat 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder``After every terminating execution of $\alpha$, $\varphi$ holds.''.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe other new kind
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederof 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
30256573a343132354b122097b0ee1215dda1364Till 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
30256573a343132354b122097b0ee1215dda1364Till Mossakowskito be true. zChaff uses the same ATP GUI as the provers for SoftFOL (ref. to section
30256573a343132354b122097b0ee1215dda1364Till 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
30256573a343132354b122097b0ee1215dda1364Till Mossakowski./configure --with-csl
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{verbatim}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe binary \texttt{redcsl} will be searched in the \texttt{PATH} or is taken
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifrom the \texttt{HETS\_REDUCE} environment variable.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{Pellet}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiPellet is a popular open-source \DL-reasoner for \SROIQ, which is the logic
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiunderlying OWL 2.0, written in Java. A Java Runtime Environment (in version $> 1.5$)
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis needed to run Pellet. For the integration into \Hets the environment variable
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\verb+PELLET_PATH+ has to be set to the root-directory of the Pellet installation.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiPellet uses the same ATP GUI as the provers for SoftFOL (ref. to section
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\ref{sec:ATP}).
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{Fact++}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFact++ is a \DL-reasoner for \SROIQ, which is the logic underlying OWL 2.0, written in
30256573a343132354b122097b0ee1215dda1364Till MossakowskiC++. Fact++ is integrated into \Hets via the OWL-API, which is written in Java.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiA Java Runtime Environment (in version $>= 1.5$) has to be installed. To use Fact++,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe environment variable \verb+HETS_OWL_TOOLS+ has to be set to the directory
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicontaining the files
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskion a 32bits-Linux-system or
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\end{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiin a 64bits-Linux-system. Fact++ does not support options.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiFact++ uses the same ATP GUI as the provers for SoftFOL (ref. to section
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\ref{sec:ATP}).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\subsection{E-KRHyper}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiE-KRHyper\footnote{\url{http://www.uni-koblenz.de/~bpelzer/ekrhyper/}}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiis an extension of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiKRHyper\footnote{\url{http://www.uni-koblenz.de/~wernhard/krhyper/}} by
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihandling of equality. E-KRHyper is an automatic first order theorem
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowskiprover and model finder based on the Hyper Tableaux Calculus\cite{Baumgartner:1996}.
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiE-KRHyper is optimized for being integrated into other systems. In the current
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowskiimplementation we use a default tactics script, that can be influenced by the user.
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiThe options of E-KRHyper are written in a Prolog-like syntax as in
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski\begin{verbatim}
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski#(set_parameter(timeout_termination_method,0)).
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski\end{verbatim}
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowskithe ``.'' at the end of each option is mandatory. To get an overview of
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiE-KRHyper's options, run the command
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiin a terminal. Then enter the command
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederat the prompt of E-KRHyper, to display its help information, which is basically
3cca22bf00dd189214595454eb696fdf954f366fMihai Codescua long list of all available parameters. You can exit E-KRHyper by the command
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederE-KRHyper uses the same ATP GUI as the other provers for SoftFOL (ref. to section
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\ref{sec:ATP}).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\subsection{Darwin}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederDarwin is an automatic first order prover and model finder implementing the Model
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCalculus\cite{Baumgartner:2003}. The integration of Darwin as a consistency checker
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisupports the display of models (if they can be constructed) in \CASL-syntax.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiEprover is needed to be in the system-path, if Darwin is used with \Hets, since
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiDarwin uses Eprover for clausification of first-order formulae.
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till MossakowskiDarwin supports a wide range of options, to get an overview of them run the command
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{verbatim}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederin a terminal.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiDarwin uses the same ATP GUI as the other provers for SoftFOL (ref. to section
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\ref{sec:ATP}).
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\subsection{QuickCheck}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\subsection{minisat}
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till Mossakowski\subsection{Truth tables}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\subsection{CspCASLProver}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\section{Limits of Hets}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\Hets is still intensively under development. In particular, the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederfollowing points are still missing:
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\begin{itemize}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item There is no proof support for architectural specifications.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item Distributed libraries are always downloaded from the local disk,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedernot from the Internet.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item Version numbers of libraries are not considered properly.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item The proof engine for development graphs provides only experimental
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedersupport for hiding links and for conservativity.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\section{Architecture of Hets}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe architecture of \Hets is shown in Fig.~\ref{fig:hets}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiHow is a single logic implemented in the Heterogeneous Tool Set?
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThis is depicted in the left column of Fig.~\ref{fig:hets}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\Hets provides an abstract interface for
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \index{institution!independence}%
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \index{independence, institution}%
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederinstitutions, so
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskithat new logics can be integrated smoothly.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIn order to do so, a parser,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskia static checker and a prover for basic specifications in the logic have
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskito be provided.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{figure}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{center}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederclass Logic lid sign morphism sentence basic_spec symbol_map
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski | lid -> sign morphism sentence basic_spec symbol_map where
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski identity :: lid -> sign -> morphism
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski compose :: lid -> morphism -> morphism -> morphism
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski dom, codom :: lid -> morphism -> sign
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski parse_basic_spec :: lid -> String -> basic_spec
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski parse_symbol_map :: lid -> String -> symbol_map
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski parse_sentence :: lid -> String -> sentence
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski empty_signature :: lid -> sign
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski basic_analysis :: lid -> sign -> basic_spec -> (sign, [sentence])
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski stat_symbol_map :: lid -> sign -> symbol_map -> morphism
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski map_sentence :: lid -> morphism -> sentence -> sentence
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski lid -> [(sign, [sentence]) -> [sentence] -> Proof_status]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski cons_checkers :: lid -> [(sign, [sentence]) -> Proof_status]
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}