5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
a17349d0247036407c22e632ece0e8f2b736253cTill 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}
1d9290e729b7cd9a6f666432934fd890a9766fbdChristoph Lange\usepackage{paralist}
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}\\
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maeder-- Version 0.99 --}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\author{Till Mossakowski, Christian Maeder,
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder Mihai Codescu\\[1em]
d78a2b8c5a63f3e63393e5cc44a5e9b253ac459bChristian MaederDFKI 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
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskiprovide an open source general framework for formal methods
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskiintegration and proof management. One can think of \Hets acting like a
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskimotherboard where different expansion cards can be plugged in, the
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskiexpansion cards here being individual logics (with their analysis and
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskiproof tools) as well as logic translations. Individual logics and
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskitheir analysis and proof tools can be plugged into the \Hets
a17349d0247036407c22e632ece0e8f2b736253cTill 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,
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian MaederCommon Logic, OWL 2, LF, THF, HOL, Haskell, and Maude. For heterogeneous
533d6033bec94a46d13b73cafe40953f699757c7Christian Maederspecification, \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
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederCspCASL & x & x & - \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederCspCASL\_Trace & - & - & x \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederCspCASL\_Failure & - & - & - \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederCommonLogic & x & x & - \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiConstraint\CASL & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederTemporal & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederRelScheme & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederDFOL & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederExtModal & x & (x) & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederLF & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Structured specifications & x & x & (x) \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Architectural specifications & x & x & -\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASLDL & x & - & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederDMU & x & - & - \\\hline
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian MaederFreeCAD & - & x & - \\\hline
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian MaederOWL 2 & x & x & x \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiPropositional & x & x & x \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederQBF & x & x & x \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederSoftFOL & x & - & x \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederMaude & x & x & - \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederVSE & x & x & x \\\hline
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian MaederTHF & x & x & x \\\hline
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder\Isabelle & (x) & - & x \\\hline
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian MaederHolLight & x & x & - \\\hline
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian MaederAdl & x & x & - \\\hline
4317329b15d986d363c78acf8e4b330f33cccf9dChristian MaederFpl & x & x & - \\\hline
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst SchulzEnCL & x & x & x \\\hline
4edebbc87f6686cea89c00cefda6e16e049c6d8cJonathan von SchroederHybrid & x & x & - \\\hline
4edebbc87f6686cea89c00cefda6e16e049c6d8cJonathan von SchroederHybridize & x & - & -\\\hline
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski\caption{Current degree of \Hets support for the different languages. Languages without prover can still ``borrow'' provers
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskivia logic translations.\label{fig:Languages}}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{description}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CASL] extends many sorted first-order logic with partial
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%specify calculi for time and space.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiWe have implemented the \CASL logic in such a way that much of the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiimplementation can be re-used for \CASL extensions as well; this
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiis achieved via ``holes'' (realized via polymorphic variables) in the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitypes for signatures, morphisms, abstract syntax etc. This eases
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiintegration of \CASL extensions and keeps the effort of integrating
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL extensions quite moderate.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
7a8592051724fa46499bde120f44cdc8db270876Till Mossakowskisuited for the specification of process types and reactive systems.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe central proof method is coinduction.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[ModalCASL] \cite{ModalCASL}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski is an extension of \CASL with multi-modalities and
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederterm modalities. It allows the specification of modal systems with
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiKripke's possible worlds semantics. It is also possible to express
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedercertain forms of dynamic logic.
e25f8c6234c9184e49ee346abebb5f961851c4a5Christian Maeder\item[ExtModal] is an extended modal logic, subsuming and replacing ModalCASL.
e25f8c6234c9184e49ee346abebb5f961851c4a5Christian Maeder It features -- apart from multiple modalities and dynamic logic -- also time
e25f8c6234c9184e49ee346abebb5f961851c4a5Christian Maeder (and term) modalities, grading, hybrid modal logic, and the $\mu$-calculus
e25f8c6234c9184e49ee346abebb5f961851c4a5Christian Maeder \cite{Codruta10}. Comorphisms to CASL and THF have been implemented.
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.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskithe language is summarized in \cite{HasCASL/Summary}, the semantics
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiin \cite{Schroder05b,Schroder-habil}.
e25f8c6234c9184e49ee346abebb5f961851c4a5Christian Maeder\item[Haskell] is a modern, pure and strongly typed functional programming
e25f8c6234c9184e49ee346abebb5f961851c4a5Christian Maeder language. With various language extensions it simultaneously is the
e25f8c6234c9184e49ee346abebb5f961851c4a5Christian Maeder implementation language of \Hets. As a logic we only supports the older
e25f8c6234c9184e49ee346abebb5f961851c4a5Christian Maeder Haskell 98 standard. Yet, in principle, \Hets might be applied to itself --
e25f8c6234c9184e49ee346abebb5f961851c4a5Christian Maeder in some more distant future. The definitive reference for Haskell is
e25f8c6234c9184e49ee346abebb5f961851c4a5Christian Maeder \cite{PeytonJones03}, see also \url{www.haskell.org}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder with the process algebra \Csp.
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\item[CommonLogic] \url{http://en.wikipedia.org/wiki/Common_logic}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[ConstraintCASL] is an experimental logic for the specification
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiof qualitative constraint calculi.
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maeder\item[OWL 2] is the Web Ontology Language (OWL 2) recommended by the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich World Wide Web Consortium (W3C, \url{http://www.w3c.org}). It is
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski used for knowledge representation and the Semantic Web
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \cite{berners:2001:SWeb}.
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian MaederHets calls an external OWL 2 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder 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}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiis an extension of a restriction of \CASL, realizing
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maedera strongly typed variant of OWL in \CASL syntax.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \CASL with cardinality restrictions for the description of sorts and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski unary predicates. The restrictions are based on the equivalence
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maeder between \CASLDL, OWL and \SHOIN. Compared to \CASL only unary
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski and binary predicates, predefined datatypes and concepts (subsorts
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maeder of the topsort Thing) are allowed. It is used to bring OWL and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \CASL closer together.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Propositional] is classical propositional logic, with
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe zChaff SAT solver \cite{Herbstritt03} connected to it.
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\item[QBF] are quantified boolean formulas, with
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederDepQBF \url{http://fmv.jku.at/depqbf/} connected to it.
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu\item[RelScheme] is a logic for relational databases \cite{DBLP:journals/ao/SchorlemmerK08}.
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski\item[SoftFOL] \cite{LuettichEA06a} offers several automated theorem
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maeder proving (ATP) systems for first-order logic with equality:
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maeder\begin{itemize}
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian Maeder \cite{WeidenbachEtAl02}, see \url{http://www.spass-prover.org};
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski\item Vampire \cite{RiazanovV02} see \url{http://www.vprover.org};
ab5781bda9fa3062a3a92c4b57fa6bc7b70c745aTill Mossakowski\item Darwin \cite{Baumgartner:etal:Darwin:IJAIT:2005}, see \url{http://combination.cs.uiowa.edu/Darwin};
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maeder\item Eprover \cite{Schulz:AICOM-2002}, see \url{http://www.eprover.org};
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maeder\item E-KRHyper \cite{DBLP:conf/cade/PelzerW07}, see \url{http://www.uni-koblenz.de/~bpelzer/ekrhyper}, and
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich MathServe Broker\footnote{which chooses an appropriate ATP upon a
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski classification of the FOL problem} \cite{ZimmerAutexier06}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski These together comprise some of the most advanced theorem provers
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski for first-order logic. SoftFOL is essentially the first-order
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowski interchange language TPTP \cite{DBLP:conf/lpar/Sutcliffe10},
fae78303778c0b2fa0b28a371a625247e4255903Christian Maeder\item[THF] simply typed lambda calculus, is an interchange language for
fae78303778c0b2fa0b28a371a625247e4255903Christian Maeder (typed) higher-order logic \cite{DBLP:conf/cade/BenzmullerRS08}, similar to
fae78303778c0b2fa0b28a371a625247e4255903Christian Maeder what TPTP is for (untyped) first-order logic. \Hets connects THF to the
fae78303778c0b2fa0b28a371a625247e4255903Christian Maeder automated higher-order provers Leo-II, Satallax and Isabelle's nitpick,
fae78303778c0b2fa0b28a371a625247e4255903Christian Maeder refute and sledgehammer.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich for higher-order logic.
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder\item[HolLight] \url{http://www.cl.cam.ac.uk/~jrh13/hol-light/}
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder is John Harrison's interactive theorem prover
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder for higher-order logic.
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\item[VSE] is an interactive theorem prover, see \ref{subsec:VSE}.
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\item[DMU] is a dummy logic to read output of ``Computer Aided
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder Three-dimensional Interactive Application'' (Catia).
6eb84b5a2295c866c59905963b9342bc120b75ebEwaryst Schulz\item[FreeCAD] is a logic to read design files of the CAD system
9db773679fcc0a65c04b99f5699d3db382b6be7aEwaryst Schulz FreeCAD\\\url{http://sourceforge.net/projects/free-cad}.
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\item[Maude] is a rewrite system \url{http://maude.cs.uiuc.edu/} for
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder first-order logic. In order to use this logic the environment variable
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder \verb+HETS_MAUDE_LIB+ must be set to a directory containing the files
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder \verb+full-maude.maude+, \verb+hets.prj+, \verb+maude2haskell.maude+ and
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu\item[DFOL] is an extension of first-order logic with dependent types \cite{rabe:dfol:06}.
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu\item [LF] is the dependent type theory of Twelf \url{http://twelf.plparty.org/}. Hets
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder calls Twelf on \verb+.elf+ files (for this, the environment variable
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu \verb+TWELF_LIB+ must be set) and reads in the OMDoc generated by Twelf.
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu Moreover, LF can be used as a logical framework to add new logics in Hets \cite{CHK+2011a}.
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu Logic definitions in LF are based in the logic atlas of the Latin project \cite{project:latin}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder and therefore the environment variable \verb+LATIN_LIB+ must be set to the
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder repository with the Latin logic definitions.
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu\item[Framework] is a dummy logic added for declarative logic definitions \cite{CHK+2011a}.
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maeder\item[Adl] is ``A Description Language'' based on relational algebra originally
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maeder designed for requirements engineering of business rules
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maeder \url{https://lab.cs.ru.nl/BusinessRules/Requirements_engineering}.
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder\item[Fpl] is a ``logic for functional programs'' as an extension of a
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maeder restriction of \CASL (predicates are disabled) \cite{Sannella12}.
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz\item[EnCL] is an ``engineering calculation language'' based on first
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz order theory of real numbers with some predefined binders
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz \cite{logic:EnCL}. It allows the formulation of executable
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz specifications of engineering calculation methods. For the execution
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz of these specifications Hets provides connections to the computer
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz algebra systems Mathematica, Maple and Reduce.
4edebbc87f6686cea89c00cefda6e16e049c6d8cJonathan von Schroeder\item[Hybrid] HybridCASL \cite{DBLP:conf/calco/NevesMMB13} extends ModalCASL by implementing
ad5671edfa2ed767ec4fdc2f3099603d6fe8b97ecmaederthe characteristic features of hybrid logic, both at the level of syntax and semantics. A comorphism from HybridCASL
4edebbc87f6686cea89c00cefda6e16e049c6d8cJonathan von Schroederto CASL is provided.
ad5671edfa2ed767ec4fdc2f3099603d6fe8b97ecmaederThe method of hybridisation of arbitrary institutions documented in \cite{DBLP:conf/calco/MartinsMDB11}, providing a method to automatically
4edebbc87f6686cea89c00cefda6e16e049c6d8cJonathan von Schroedercombine the standard properties of hybrid logics with any logic already integrated in Hets.
4edebbc87f6686cea89c00cefda6e16e049c6d8cJonathan von SchroederSome manual intervention is still required: a parser and a semantics analyser for the sentences of the base
ad5671edfa2ed767ec4fdc2f3099603d6fe8b97ecmaederlogic need to be declared at source code level.
4edebbc87f6686cea89c00cefda6e16e049c6d8cJonathan von SchroederCurrently, the hybridised versions of the following logics may be used in a fully automatic way:
4edebbc87f6686cea89c00cefda6e16e049c6d8cJonathan von SchroederPropositional, CASL, CoCASL, and any other logic already hybridised.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{description}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiVarious logics are supported with proof tools. Proof support for the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiother logics can be obtained by using logic translations to a
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiprover-supported logic.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiAn introduction to \CASL can be found in the \CASL User Manual
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\cite{CASL-UM}; the detailed language reference is given in
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiexplain both the \CASL logic and language of basic specifications as
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwell as the logic-independent constructs for structured and
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiarchitectural specifications. The corresponding document explaining the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\HetCASL language constructs for \emph{heterogeneous} structured specifications
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis the \HetCASL language summary \cite{Mossakowski04}; a formal
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedersemantics as well as a user manual with more examples are in preparation.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederSome of \HetCASL's heterogeneous constructs will be illustrated
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiin Sect.~\ref{sec:HetSpec} below.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Logic translations supported
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\label{comorphisms}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiLogic translations (formalized as institution comorphisms
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{GoguenRosu02}) translate from a given source logic to a given
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitarget logic. More precisely, one and the same logic translation
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimay have several source and target \emph{sub}logics: for
30256573a343132354b122097b0ee1215dda1364Till Mossakowskieach source sublogic, the corresponding sublogic of the target
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilogic is indicated.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiA graph of the most important logics and sublogics, together with their
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{figure}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \begin{center}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \includegraphics[scale=0.4]{SublogicGraph}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\caption{Graph of most important sublogics currently supported by \Hets,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitogether with their comorphisms.}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\label{fig:SublogicGraph}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIn more detail, the following list of logic translations is currently
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisupported by \Hets:
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\begin{tabular}{|l|p{8cm}|}\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederAdl2CASL & inclusion taking relations to CASL predicates \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCASL2CoCASL & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2CspCASL & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2HasCASL & inclusion \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCASL2Isabelle & inclusion on sublogic CFOL=
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder(translation $(7)$ of \cite{Mossakowski02}) \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2Modal & inclusion \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCASL2PCFOL & coding of subsorting (SubPCFOL=) by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual} \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskipredicates for the subsorts \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCASL2Propositional & translation of propositional FOL \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCASL2SoftFOL & coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maedermapping types to soft types \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCASL2SoftFOLInduction & same as CASL2SoftFOL but with instances of induction
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederaxioms for all proof goals \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederCASL2SoftFOLInduction2 & similar to CASL2SoftFOLInduction but replaces goals with induction premises \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCASL2SubCFOL & coding of partial functions by error elements
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maeder(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting, i.e. sublogic SubPCFOL=) \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCASL2VSE & inclusion on sublogic CFOL= \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCASL2VSEImport & inclusion on sublogic CFOL= \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederCASL2VSERefine & refining translation of CASL.CFOL= to VSE \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCASL\_DL2CASL & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCoCASL2Isabelle & extended translation similar to CASL2Isabelle \\\hline
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen KuksaCommonLogic2CASL & Coding Common Logic to \CASL.Module elimination
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen Kuksa is applied before translating to \CASL. \\\hline
650631bddf665ec5ef991bf4ce2f569b7709d104Christian MaederCommonLogic2CASLCompact & Coding compact Common Logic to \CASL.
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen Kuksa Compact Common Logic is a sublogic of Common Logic
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen Kuksa where no sequence markers occur. Module elimination
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen Kuksa is applied before translating to \CASL. We recommend
650631bddf665ec5ef991bf4ce2f569b7709d104Christian Maeder using this comorphism whenever possible because it
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen Kuksa results in simpler specifications.\\\hline
650631bddf665ec5ef991bf4ce2f569b7709d104Christian MaederCommonLogicModuleElimination & Eliminating modules from a Common Logic theory
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen Kuksa resulting in an equivalent specification without
5c9181d2fd65687ced28a27cb8e161dee6d97f51Eugen Kuksa modules. \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCspCASL2CspCASL\_Failure & inclusion \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCspCASL2CspCASL\_Trace & inclusion \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederCspCASL2Modal & translating the CASL data part to ModalCASL \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederDFOL2CASL & translating dependent types \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederDMU2OWL & interpreting Catia output as OWL \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\begin{tabular}{|l|p{7cm}|}\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederHasCASL2HasCASLNoSubtypes & coding out subtypes \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederHasCASL2HasCASLPrograms & coding of \HasCASL axiomatic recursive definitions
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian Maederas \HasCASL recursive program definitions \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederHasCASL2IsabelleOption & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederHaskell2Isabelle & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07} \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederHolLight2Isabelle & coding of HolLight to Isabelle/HOL \\\hline
17787092f1a5f5d16445e8293fd4bcde69e3fc81Mihai CodescuMaude2CASL & encoding of rewrites as predicates \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiModal2CASL & the standard translation of modal logic
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskito first-order logic \cite{blackburn_p-etal:2001a} \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederOWL2CASL & inclusion \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederOWL2CommonLogic & inclusion \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederPropositional2CASL & inclusion \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederPropositional2QBF & inclusion \\\hline
533d6033bec94a46d13b73cafe40953f699757c7Christian MaederQBF2Propositional & inclusion \\\hline
7c3c3698b466d4c20e26b7bf4a16f3970303bcf7Christian MaederRelScheme2CASL & inclusion \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Getting started}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe latest \Hets version can be obtained from the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets tools home page
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski Since \Hets is being
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
e8f447e9e532f38658c7b3bbd0a5407aa42f66fbChristian Maeder\Hets is currently available (on Intel architectures only) for Linux
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian Maederand with limited functionality for Mac OSX.
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian MaederThere are several possibilities to install \Hets.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\begin{enumerate}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian MaederThe best support is currently given via Ubuntu packages.
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\begin{verbatim}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maedersudo apt-add-repository ppa:hets/hets
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maedersudo apt-get update
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maedersudo apt-get install hets
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder\end{verbatim}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian MaederThis will also install quite a couple of tools for proving requiring about
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder800 MB of disk space. For a minimal installation \texttt{apt-get install
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder hets-core} instead of \texttt{hets}.
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian MaederThe following software will be installed, too:
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\begin{tabular}{|l|l|p{5cm}|}\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
c5e63ec138b908ac9d15e6843120033bf36a1862Till MossakowskiuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian MaederTcl/Tk & graphics widget system & (version 8.4 or 8.5)\\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian MaederDarwin & theorem prover & \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian MaederA daily snapshot of \texttt{hets} can be installed by:
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian Maeder\begin{verbatim}
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian Maedersudo hets -update
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian Maeder\end{verbatim}
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian MaederIn case the binary (under \texttt{/usr/lib/hets/hets}) is broken it can be replaced manually or by reverting an update:
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian Maeder\begin{verbatim}
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian Maedersudo hets -revert
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian Maeder\end{verbatim}
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian Maeder\item For Mac OSX we provide disk images \texttt{Hets-<date>.dmg} without GTK support.
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian MaederYou may compile \Hets from the sources (they are licensed under GPL),
a17349d0247036407c22e632ece0e8f2b736253cTill Mossakowskiplease follow the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilink ``Hets: source code and information for developers''
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskion the \Hets web page, download the sources (as tarball or from
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisvn), and follow the
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederinstructions in the \texttt{INSTALL} file, but be prepared to take some time.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\end{enumerate}
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederDepending on your application further tools are supported and may be
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederinstalled in addition:
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder\begin{tabular}{|l|l|p{5cm}|}\hline
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian Maeder\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
34d880694ed872dd3e7f922bd9ca3b1aa917c822Christian Maeder(X)Emacs & editor (for Isabelle) & \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederzChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maederminisat & SAT solver & \url{http://minisat.se/} \\\hline
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian MaederPellet & OWL 2 reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederE-KRHyper & theorem prover
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederReduce & computer algebra system
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian Maeder & \url{http://www.reduce-algebra.com/} \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederVSE & theorem prover & (non-public) \\\hline
e0dcf58cb6eb2ba4cf2e14734d3af3c992cc1885Christian MaederTwelf & & \url{http://twelf.plparty.org/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Analysis of Specifications}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiConsider the following \CASL
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\I\SPEC \NAME{Strict\_Partial\_Order} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\PRED]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\I\SORT \( Elem \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y,z : Elem \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{COMMENT}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote that there may exist \(x, y\) such that\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskineither \(x < y\) nor \(y < x\).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\Hets can be used for parsing and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskichecking static well-formedness of specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{parsing}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{static!analysis}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{analysis, static}%
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLet us assume that the example is in a file named
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\texttt{Order.casl} (actually, this file is provided
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederwith the \Hets distribution as \texttt{Hets-lib/UserManual/Chapter3.casl}).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThen you can check the well-formedness of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecification by typing (into some shell):
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets checks both the correctness of this specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with respect to the \CASL syntax, as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwell as its correctness with respect to the static semantics (e.g.\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether all identifiers have been declared before they are used,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether operators are applied to arguments of the correct sorts,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhether the use of overloaded symbols is unambiguous, and so on).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe following flags are available in this context:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder -- the static analysis is skipped and no development is created.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
30256573a343132354b122097b0ee1215dda1364Till Mossakowski static analysis of (heterogeneous) structured specifications, but
30256573a343132354b122097b0ee1215dda1364Till Mossakowski leave out the analysis of basic specifications. This can be used
30256573a343132354b122097b0ee1215dda1364Till Mossakowski for prototyping issues, namely to quickly produce a development graph
30256573a343132354b122097b0ee1215dda1364Till Mossakowski showing the dependencies among the specifications (cf.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Sect.~\ref{sec:DevGraph}) even if the individual specifications are
30256573a343132354b122097b0ee1215dda1364Till Mossakowski not correct yet.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederUse \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).
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item[\texttt{-a ANALYSIS}, \texttt{--casl-amalg=ANALYSIS}]
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski For the analysis of architectural specification (a quite advanced
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder amalgamability checking
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski algorithm for \CASL logic; it is a comma-separated list of zero or
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski more of the following options:
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \begin{description}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \item[\texttt{sharing}] perform sharing analysis for sorts,
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski operations and predicates.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \item[\texttt{cell}] perform cell condition check; implies
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \texttt{sharing}. With this option on, the subsort embeddings are
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \item[\texttt{colimit-thinness}] perform colimit thinness check;
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski implies \texttt{sharing}. The colimit thinness check is less
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski complete and usually takes longer than the full cell condition
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski check (\texttt{cell} option), but may prove more efficient in case
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder of certain specifications.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \end{description}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski If \texttt{ANALYSIS} is empty then amalgamability analysis for
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \CASL is skipped.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski The default value for \texttt{--casl-amalg} is
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \texttt{cell}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\Hets accepts plain text input files with the following endings:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{tabular}{|l|c|c|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiEnding & default logic & structuring language\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder\texttt{.hol} & HolLight & HolLight \\\hline
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder\texttt{.hs} & Haskell & Haskell \\\hline
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maeder\texttt{.owl} & OWL 2 & OWL \\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\texttt{.elf} & LF & Twelf \\\hline
a748e6c1e72afbfa4f76e06632c05cb535bb54a0Christian Maeder\texttt{.clf} or \texttt{.clif} & CommonLogic & \CASL \\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\texttt{.maude} & Maude & Maude \\\hline
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederFurthermore, \texttt{.xml} files are accepted as Catia output if the default
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederlogic is set to DMU before a library import or by the ``\texttt{-l DMU}''
a748e6c1e72afbfa4f76e06632c05cb535bb54a0Christian Maedercommand line option of \Hets. In all other cases \texttt{.xml} files are
a748e6c1e72afbfa4f76e06632c05cb535bb54a0Christian Maederassumed to be development graph files as produced by ``\texttt{-o xml}''.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinterchangeable, the former should be used for libraries of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof heterogeneous specifications (that use the \CASL structuring
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskito \HasCASL in the following way:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe subsequent specifications are then parsed and analysed as
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\HasCASL specifications. Within such specifications,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiit is possible to use references to named \CASL specifications;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithese are then automatically translated along the default
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(There are also heterogeneous constructs
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor explicit translations between logics, see \cite{Mossakowski04}.)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiA \CspCASL specification consists of a \CASL specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifor the data part and a \Csp process built over this data part.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{data} as follows:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary Buffer
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski free type List[Elem] ::= nil | cons(Elem; List[Elem])
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder ops last: List -> ? Elem;
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder rest: List -> ? List
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski channel read, write : Elem
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder process Buf(List): read, write, List;
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder EmptyBuffer : read,write, List;
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder Buf(l)= read? x :: Elem -> Buf(cons(x,nil)) []
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (if l=nil then STOP else
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder write!last(l) -> Buf(rest(l)))
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder EmptyBuffer = Buf(nil)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHere, the construct \texttt{data List} refers to the \CASL specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{List}, which is implicitly embedded into \CspCASL.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe ending \texttt{.hs} is available for directly reading in
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederHaskell programs % and HasSLe specifications,
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowskiand hence supports the Haskell module system.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe logic Haskell has to be chosen explicitly, and the \CASL structuring
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisyntax needs to be used:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary Factorial
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispec Factorial =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifac :: Int -> Int
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifac n = foldl (*) 1 [1..n]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiNote that according to the Haskell syntax, Haskell function
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskideclarations and definitions need to start with the first column of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Development Graphs}\label{sec:DevGraph}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederstructured theorem proving and proof management.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiA development graph consists of a set of nodes (corresponding to whole
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskistructured specifications or parts thereof), and a set of arrows
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskicalled \emph{definition links}, indicating the dependency of each
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiinvolved structured specification on its subparts. Each node is
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiassociated with a signature and some set of local axioms. The axioms
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiof other nodes are inherited via definition links. Definition links
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiare usually drawn as black solid arrows, denoting an import of another
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskispecification.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiComplementary to definition links, which \emph{define} the theories of
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskirelated nodes, \emph{theorem links} serve for \emph{postulating}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskirelations between different theories. Theorem links are the central
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskidata structure to represent proof obligations arising in formal
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiTheorem links can be \emph{global} (drawn as solid arrows) or
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\emph{local} (drawn as dashed arrows): a global theorem link
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskipostulates that all axioms of the source node (including the inherited
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiones) hold in the target node, while a local theorem link only postulates
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskithat the local axioms of the source node hold in the target node.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederBoth definition and theorem links can be \emph{homogeneous},
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskii.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskithe logic changes along the arrow. Technically, this is the case
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskifor Grothendieck signature morphisms $(\rho,\sigma)$ where
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski$\rho\not=id$. This case is indicated with double arrows.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiTheorem links are initially displayed in red.
38914aa544a92aa72e537446cfff297dc6109e04Christian MaederThe \emph{proof calculus} for development graphs
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\cite{MossakowskiEtAl05,Habil} is given by rules
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskithat allow for proving global theorem links by decomposing them
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiinto simpler (local and global) ones. Theorem links that have been
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiproved with this calculus are drawn in green. Local theorem links can
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskibe proved by turning them into \emph{local proof goals}. The latter
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskican be discharged using a logic-specific calculus as given by an
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskientailment system for a specific institution. Open local
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiproof goals are indicated by marking the corresponding node in the
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskidevelopment graph as red; if all local implications are proved, the
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskinode is turned into green. This implementation ultimately is based
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskion a theorem \cite{Habil} stating soundness and relative completeness
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiof the proof calculus for heterogeneous development graphs.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe following options let \Hets show the development graph of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskia specification library:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item[\texttt{-u}, \texttt{--uncolored}] no colors in shown graphs
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\end{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe following additional options also apply typical rules from the development
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedergraph calculus to the final graph and save applying these rule via the GUI.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\begin{description}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-A}, \texttt{--apply-automatic-rule}] apply the automatic
d3e4f883d74b0cd6b1708141fddc20e895e82eb1Eugen Kuksa strategy to the development graph. This is what you usually want in order to
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder get goals within nodes for proving.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-N}, \texttt{--normal-form}] compute all normal forms for nodes
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder with incoming hiding links. (This may take long and may not be implemented
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder for all logics.)
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiLet us extend the above library \texttt{Order.casl}. One use of the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilibrary might be to express the fact that the natural numbers form a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiby a strict partial ordering relation. Checking this requires theorem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproving, which will be discussed below.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHowever, before coming to theorem proving, let us first inspect the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligations arising from a specification. This can be done with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Order.casl}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder(assuming that the above two specifications and the view
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederhave 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}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiNodes in a development graph correspond to \CASL specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiArrows show how specifications are related by the structuring
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe black arrow denotes an ordinary import of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecifications (generated by the extension), while the red arrow
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidenotes a proof obligation (corresponding to the view).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis proof obligation needs to be discharged in order to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskishow that the view is well-formed (then its color turns into green).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAs a more complex example, consider the following loose specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof a sorting function, taken from the \CASL User Manual
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\cite{CASL-UM}, Chap.~6:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order\_Sorted}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\PRED]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_is\_sorted : List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e,e': Elem; L : List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. empty~is\_sorted \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. cons(e,empty)~is\_sorted \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. cons(e,cons(e',L))~is\_sorted \IFF
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\\\M (cons(e',L)~is\_sorted \A \NOT(e'<e)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\( \FORALL L:List\. \[ order(L)~is\_sorted \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following specification of sorting by insertion also is taken from
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowskithe \CASL User Manual \cite{CASL-UM}, Chap.~6:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\phantomsection
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( insert : Elem \* List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e,e':Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, empty) = cons(e, empty) \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. insert(e, cons(e',L)) = \[ cons(e', insert(e,L)) \WHEN e' < e\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \ELSE cons(e, cons(e',L)) \] \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\OP \( order : List \TOTAL List \)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL e:Elem; L:List \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(empty) = empty \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. order(cons(e,L)) = insert(e, order(L)) \]\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBoth specifications are related. To see this, we first inspect
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheir signatures. This is possible with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Sorting.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiassuming that \texttt{Sorting.casl} contains the above specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-1}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn the above-mentioned development graph, we have two types of nodes.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe named ones correspond to named specifications, but there
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare also unnamed nodes corresponding to anonymous basic
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederspecifications like the declaration of the $insert$ operation in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} above. Basically, there is an
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiunnamed node for each structured specification that is not named.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAgain, the black arrows denote an ordinary import of specifications
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(corresponding to the extensions and unions in the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederspecifications), while the blue arrows denote hiding (corresponding to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe local specification).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBy clicking on the nodes, one can inspect their signatures.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} have the same signature. Hence, it
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis legal to add a view:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWe have already added this view to \texttt{Sorting.casl}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe corresponding
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederproof obligation between \NAMEREF{List\_Order\_Sorted} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski as a red arrow.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederHere is a summary of the types of nodes and links occurring in
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederdevelopment graphs:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Named nodes] correspond to a named specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Unnamed nodes] correspond to an anonymous specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Elliptic nodes] correspond to a specification in the current library.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Rectangular nodes] are external nodes corresponding to a specification
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder downloaded from another library.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Red nodes] have open proof obligations.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Yellow nodes] have an open conservativity proof obligations.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Green nodes] have all proof obligations resolved.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Black links] correspond to reference to other specifications (definition
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder links in the sense of \cite[IV:4]{CASL/RefManual}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Red links] correspond to open proof obligations (theorem links).
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Green links] correspond to proven theorem links.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Yellow links] correspond to proven theorem links with open
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder conservativity or to open hiding theorem links.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Blue links] correspond to hiding, free, or cofree definition links.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Violett links] correspond to a mixture of links becoming visible after
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder ``expand'' or ``Show unnamed nodes with open proofs''.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Solid links] correspond to global (definition or theorem)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilinks in the sense of \cite[IV:4]{CASL/RefManual}.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Dashed links] correspond to local (theorem) links in the sense of
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder \cite[IV:4]{CASL/RefManual}. These are usually created after
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder ``Global-Decomposition'' or only be visible after ``Show newly added proven
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Single line links] have homogeneous signature morphisms (staying within
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder one and the same logic).
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Double line links] have heterogeneous signature morphisms (moving
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder between logics).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWe now explain the menus of the development graph window.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiMost of the pull-down menus of the window are uDraw(Graph)-specific
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitheir function can be looked up in the uDraw(Graph) documentation\footnote{see
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe exception is the Edit menu. Moreover, the nodes and links
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the graph have attached pop-up menus, which appear when
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiclicking with the right mouse button.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Edit] This menu has the following submenus:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Undo] Undo the last development graph proof step (see under Proofs)
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Redo] Restore the last undone development graph proof step (see
30256573a343132354b122097b0ee1215dda1364Till Mossakowski under Proofs)
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuThe ``Hide/show names/nodes/edges'' menu is a toggle:
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederyou 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
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederare initially unnamed get derived names.
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederWith 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;
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuonly nodes corresponding to named specifications are displayed.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPaths between named nodes going through unnamed nodes
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederare 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
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederbeen proven are removed from the graph. With the ``Hide/Show newly added
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuproven edges'' option, it is possible to re-display these links; they are marked
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuas proven in the link info (see \emph{Pop-up menu for links}, below).
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Focus node]
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian MaederThis menu is particularly useful when navigating in a large development graph,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederwhich 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.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederOnce a node is selected, the view centers on it.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Select Linktypes]
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThis menu allows to select the type of links that are displayed in the
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescudevelopment graph. A selection window appears, where links are grouped into
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthree categories: definition links, proven theorem links and unproven
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescutheorem links. It is possible to select/deselect all links or to invert the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedercurrent selection.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item[Consistency checker]
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder Checks whether the theories of the nodes of the graph are consistent
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder i.e. have a model. The model finders currently interfaced are
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder Isabelle-refute, darwin and E-KRHyper, with best support for darwin.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Proofs] This menu allows to apply some of the deduction rules
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski for development graphs, see Sect. IV:4.4 of the \CASL Reference
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Manual \cite{CASL/RefManual} or one of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}. While support for
30256573a343132354b122097b0ee1215dda1364Till Mossakowski local and global (definition or theorem) links is stable, support
30256573a343132354b122097b0ee1215dda1364Till Mossakowski for hiding links and checking conservativity is still experimental.
af35cfab2b45879b385a8ec31558f7ebb1b3dc5fChristian Maeder In most cases, it is advisable to use ``Auto-DG-Prover'', which
30256573a343132354b122097b0ee1215dda1364Till Mossakowski automatically applies the rules in the correct order. As a result,
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder the open theorem links (marked in red) will be reduced to local
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder proof goals, that is, they become green, and instead, some target nodes
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder may get red, indicating open local proof goals.
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescu Besides the deduction rules, the menu contains entries for computing
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder a colimit approximation for the development graph and for
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescu computing normal forms of all nodes (needed when dealing with hiding).
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu Also, a \CASL-specific normalisation of free links has been
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\item[Dump Development Graph] This option is available only for
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder debugging purposes; it outputs a textual representation
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder of the development graph.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Show Library Graph] This menu displays the library graph, in a separate
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder window, if the library graph window has been closed after \Hets has been
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Save Graph for uDrawGraph] Saves the development graph in a .udg file
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu which can be later read by uDrawGraph.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Save proof-script] This menu saves the proof rules that have been applied
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder to the current development graph in a .hpf file which can be later read by
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu \Hets and thus the action performed on the graph are saved.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Pop-up menu for nodes]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHere, the number of submenus depends on the type of the node:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Show node info] Shows the local informations of the node: the internal
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder node name and node number, the xpath that denotes the location of the node
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder within an XML representation, information about consistency of the node,
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder origin of the node and the local theory i.e. axioms declared locally.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Show theory] Shows the theory of the node (including axioms
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuimported from other nodes). Notice that axioms imported via hiding links
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiare not part of the theory; they can be made visible only by re-adding
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederthe hidden symbols, using the normal form of the node, by calling
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\emph{Proofs/Compute Normal Form}. For such nodes, a warning is displayed.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Translate theory] Translates the theory of a node to another logic.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiA menu with the possible translation paths will be displayed.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu of the signature of the node.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Show proof status] Show open and proven local proof goals.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\item[Prove VSE structured] Allows to send a development graph below the
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder current node to the interactive \texttt{hetsvse} prover if that binary is
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder available, see \ref{subsec:VSE}.
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder\item[Disprove] Negates selected goals and tries to disprove them using
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder consistency checkers. Other goals will be treated like axioms if ``Include
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder Theorems'' is selected. (If a theory is consistent with a negated goal, the
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder goal is disproven.)
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder\item[Add sentence] This menu allows to add a sentence on the fly. The
d3e4f883d74b0cd6b1708141fddc20e895e82eb1Eugen Kuksa (possibly named) sentence will be parsed and analysed using the underlying logic.
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder\item[Check consistency] Simply calls the global ``Consistency checker'' menu
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder for the current node, see \ref{sec:CC}.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item[Check conservativity] Checks conservativity of the inclusion
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu morphism from the empty theory to the theory of the node (see
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu {\bf Check conervativity} for edges).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuFor the nodes which are references to specifications from an external library,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuthe pop-up menu options are reduced to {\bf Show node info, Show theory,
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai CodescuShow proof status} and {\bf Prove} and moroever, the option {\bf Show
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescureferenced library} is added: on selection, it displays in a new window
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescuthe development graph of the external library from which the specification has
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescubeen downloaded.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Pop-up menu for links]
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus LuettichAgain, the number of submenus depends on the type of the link:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Show info] Shows informations about the edge: internal number and
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederinternal nodes it links, the link type and origin and the
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescusignature morphism of the link. The latter consists
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof two components: a logic translation and a signature morphism in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitarget logic of the logic translation.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIn the (most frequent) case
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof an intra-logic signature morphism, the logic translation component is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskijust the identity.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Check conservativity] (Experimental) Check whether the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskitheory of the target node of the link
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiis a conservative extension of the theory of the source node.
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescu\item[Expand]This menu is available only for paths going through unnamed
ed4d9ed5597a2d5cc80793233a693ca24f60afa2Mihai Codescunodes which are not displayed and it expands the path to the links forming it.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian MaederBesides development graphs there are library graph windows displaying the
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maederlibrary hierarchy. The Edit menu has the following submenus:
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\begin{description}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Edit] This menu for library graphs has the following submenus:
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\begin{description}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Reload Library] Reloads all \HetCASL sources in order to avoid closing
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder and restarting the application after sources have changed. However, all
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder previous proof steps will be lost, therefore you have to confirm this
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder action. (A change management tool to keep proofs is in preparation.)
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder\item[Experimental reload changed Library] This button is supposed to
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder interface our change management tool (in order to preserve proof
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maeder information) but does not work yet.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Translate Library] Translates a library along a comorphism to be chosen.
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder This only works for a homogeneous library hierarchy. A finer grained
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder alternative is to use ``Translate theory'' for individual nodes. The
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder original state and proof steps will be lost, therefore you have to confirm
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Show Logic Graph] Shows the graph of logics and logic comorphisms
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder currently supported by \Hets. The Edit menu of a logic graph window has the
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder following submenu:
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\begin{description}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\item[Show detailed logic graph] Shows the important sublogics and comorphims
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder between them, i.e. translation (blue links) and inclusion (black links).
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\end{description}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\end{description}
c449906d0bfb0da56e503edfe7f5e998268e33b2Christian Maeder\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Reading, Writing and Formatting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets provides several options controlling the types of files
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithat are read and written.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\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},
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder or \texttt{het} extensions are tried in this order. An \texttt{env} file
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder 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
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe possible input types are:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{verbatim}
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder | [tree.]gen_trm[.baf]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederSpecify \texttt{DIR} as destination directory for output files.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\texttt{OTYPES} is a comma separated list of output types:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{verbatim}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder | (sig|th)[.delta]
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder | pp.(het|tex|xml|html)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{verbatim}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe \texttt{env} and \texttt{prf} formats are for subsequent reading,
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederavoiding the need to re-analyse downloaded libraries. \texttt{prf} files
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedercan also be stored or loaded via the GUI's File menu.
38914aa544a92aa72e537446cfff297dc6109e04Christian MaederThe \texttt{omn} option \cite{books/sp/Kohlhase06} will produce OWL files in
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederManchester Syntax for each specification of a structured OWL library.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimarkup format and data model for Open Mathematical Documents. It
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiserves as semantics-oriented representation format and ontology
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilanguage for mathematical knowledge. Currently, \CASL specifications
30256573a343132354b122097b0ee1215dda1364Till Mossakowskican be output in this format; support for further logics is planned.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe \texttt{xml} option will produce an XML-version of the development graph
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederfor our change management broker.
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaThe \texttt{db} option will save the development graph to a database.
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaThis can be either an SQLite database or a PostgreSQL database (only available
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksain the \texttt{hets-server} package). For an SQLite database, you need to pass
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksathe parameter \texttt{--database-file=FILEPATH} to specify the database file to
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksasave to. If the file does not yet exist, \Hets will create it.
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen KuksaFor a PostgreSQL database, you need to pass the
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa\texttt{--database-config=FILEPATH} and \texttt{--database-subconfig=KEY}
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaparameters that point to a Ruby-on-Rails-compatible \texttt{database.yml}
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaconfiguration file.\footnote{An example for a \texttt{database.yml} file can be
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksafound at \url{https://github.com/spechub/Hets/blob/master/Persistence/database_postgresql.yml}}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe \texttt{exp} format is the new experimental omdoc format.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{hs} format is used for Haskell modules. Executable \CASL or
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\HasCASL specifications can be translated to Haskell.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiWhen the \texttt{thy} format is selected, \Hets will try to translate
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskieach specification in the library to \Isabelle, and write one \Isabelle
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\texttt{.thy} file per specification.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiWhen the \texttt{comptable.xml} format is selected, \Hets will extract
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskithe composition and inverse table of a Tarskian relation algebra from
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskispecification(s) (selected with the \texttt{-n} or \texttt{--spec}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskioption). It is assumed that the relation algebra is
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskigenerated by basic relations, and that the specification is written
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiin the \CASL logic. A sample specification of a relation
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskialgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiavailable from \texttt{www.cofi.info/Libraries}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe output format is XML, the URL of the DTD is included in the
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederThe \texttt{sig} or \texttt{th} option will create \HetCASL signature or
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maedertheory files for each development graph node. (The \texttt{.delta} extension
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederis not supported, yet.)
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{pp} format is for pretty printing, either as plain text
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder(\texttt{het}), \LaTeX input (\texttt{tex}), HTML (\texttt{html}) or XML
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder(\texttt{xml}). For example, it is possible to generate a pretty printed
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder\LaTeX\ version of \texttt{Order.casl} by typing:
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThis will generate a file \texttt{Order.pp.tex}. It can be included
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
38914aa544a92aa72e537446cfff297dc6109e04Christian MaederThe format \texttt{pp.xml} represents just a parsed library in XML.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederFormats with \texttt{graph} are for future usage.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{dfg} format is used by the \SPASS theorem prover
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{WeidenbachEtAl02}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederformat for first-order theorem provers.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederAppending \texttt{.c} to \texttt{dfg} or \texttt{tptp} will create files for
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederconsistency checks by SPASS or Darwin respectively.
1e276df94eadfeab45099f4482f76a9958bedb9cChristian MaederFor all output formats it is recommended to increase the verbosity to at least
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederlevel 2 (by using the option \texttt{-v2}) to get feedback which files are
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederactually written. (\texttt{-v2} also shows which files are read.)
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederchooses a translation option. \texttt{TRANS} is a colon-separated list
38914aa544a92aa72e537446cfff297dc6109e04Christian Maederwithout blanks of one or more comorphism names (see Sect.~\ref{comorphisms})
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maederchooses a list of named specifications for processing
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder\item[\texttt{-w NVIEWS}, \texttt{--view=NVIEWS}]
38914aa544a92aa72e537446cfff297dc6109e04Christian Maederchooses a list of named views for processing
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder\item[\texttt{-R}, \texttt{--recursive}] output also imported libraries
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-I}, \texttt{--interactive}] run \Hets in interactive mode
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian Maeder\item[\texttt{-X}, \texttt{--server}] run \Hets as web server (see
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian Maeder \ref{sec:Server})
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-x}, \texttt{--xml}] use xml-pgip packets to communicate with
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \Hets in interactive mode
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-S PORT}, \texttt{--listen=PORT}] communicate
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder with \Hets in interactive mode vy listining to the port \texttt{PORT}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-c HOSTNAME:PORT}, \texttt{--connect=HOSTNAME:PORT}] communicate
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder with \Hets in interactive mode via connecting to the port on host
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder \texttt{HOSTNAME}
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder\item[\texttt{-d STRING}, \texttt{--dump=STRING}] produces implementation
1e276df94eadfeab45099f4482f76a9958bedb9cChristian Maeder dependent output for debugging purposes only
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder (i.e.\ \texttt{-d LogicGraph} lists the logics and comorphisms)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian Maeder\section{Hets as a web server}\label{sec:Server}
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian MaederLarge parts of \Hets are now also available via a web interface. A running
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian Maederserver should be accessible on
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian Maeder\url{http://pollux.informatik.uni-bremen.de:8000/}. It allows to browse the
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian Maeder\Hets library, upload a file or just a \HetCASL specification. Development
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian Maedergraphs for well-formed specifications can be displayed in various formats
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian Maederwhere the \texttt{svg} format is supposed to look like the graphs displayed by
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian MaederuDrawGraph. Besides browsing, the web server is supposed to be accessed by
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian Maederother programs using queries. The possible queries are described on
c4ef92d191720274e401498d3ba8dd97e1e76dc8Christian Maeder\url{http://trac.informatik.uni-bremen.de:8080/hets/wiki/RESTfulInterface}.
615303ffb83111f58cb5429d0d54d367de74f414Christian MaederA development graph is addressed by the \emph{path} following the port number
615303ffb83111f58cb5429d0d54d367de74f414Christian Maederand the slash of the URL, i.e.\
615303ffb83111f58cb5429d0d54d367de74f414Christian Maeder\url{http://localhost:8000/Basic/Numbers.casl}. Once a development has been
615303ffb83111f58cb5429d0d54d367de74f414Christian Maedercreated it can be accessed via a (fairly unique) session id (consisting of
615303ffb83111f58cb5429d0d54d367de74f414Christian Maedernine digits) that can be used as \emph{path}.
615303ffb83111f58cb5429d0d54d367de74f414Christian MaederA \emph{path} may be followed by a query string that begins with a question
615303ffb83111f58cb5429d0d54d367de74f414Christian Maedermark and consists of \emph{entries} (usually field-value pairs) separated by
615303ffb83111f58cb5429d0d54d367de74f414Christian Maederampersands. The queries control the information to be extracted from the
615303ffb83111f58cb5429d0d54d367de74f414Christian Maederdevelopment graph given by the \emph{path} or they allow to perform commands
615303ffb83111f58cb5429d0d54d367de74f414Christian MaederUsually, query string are made up of \texttt{field=value} pairs, but in some
615303ffb83111f58cb5429d0d54d367de74f414Christian Maedercases the field name or the value may be omitted and in that case the equal
615303ffb83111f58cb5429d0d54d367de74f414Christian Maedersign must be omitted, too.
615303ffb83111f58cb5429d0d54d367de74f414Christian MaederFor instance strings denoting formats, like \texttt{xml}, \texttt{svg},
615303ffb83111f58cb5429d0d54d367de74f414Christian Maeder\texttt{pdf}, etc., do not need to be preceded by \texttt{format=}. Some
615303ffb83111f58cb5429d0d54d367de74f414Christian Maederformats, like \texttt{pdf}, only pretty print specification and
615303ffb83111f58cb5429d0d54d367de74f414Christian Maederbasically ignore the underlying development graph.
615303ffb83111f58cb5429d0d54d367de74f414Christian MaederA special \emph{entry} is just \texttt{session} which only returns a fresh
615303ffb83111f58cb5429d0d54d367de74f414Christian Maedersession id for a development graph that is given by a file name, i.e.\
615303ffb83111f58cb5429d0d54d367de74f414Christian Maeder\url{http://localhost:8000/Basic/Numbers.casl?session}. These session ids must
615303ffb83111f58cb5429d0d54d367de74f414Christian Maederbe used to perform commands (of the development graph calculus) that
615303ffb83111f58cb5429d0d54d367de74f414Christian Maeder\emph{change} the underlying graph.
615303ffb83111f58cb5429d0d54d367de74f414Christian MaederGiven a graph, nodes and edges can be addressed by numbers via entries like
615303ffb83111f58cb5429d0d54d367de74f414Christian Maeder\texttt{node=0} or \texttt{edge=0}. (Nodes can also be given by name.) For
615303ffb83111f58cb5429d0d54d367de74f414Christian Maedernodes, prover actions are possible by further
615303ffb83111f58cb5429d0d54d367de74f414Christian Maederentries. \url{http://localhost:8000/123456789?prove=Nat\_\_E1\&prover=SPASS\&timeout=5}
615303ffb83111f58cb5429d0d54d367de74f414Christian Maederwould try to prove the goals of the node \texttt{Nat\_\_E1} using the prover
615303ffb83111f58cb5429d0d54d367de74f414Christian Maeder\texttt{SPASS} with a timeout of 5 seconds for the development graph that
615303ffb83111f58cb5429d0d54d367de74f414Christian Maederhappened to have the (unlikely) session id \texttt{123456789}. Individual
615303ffb83111f58cb5429d0d54d367de74f414Christian Maedergoals can be given via a \texttt{theorems} field and special translations by a
615303ffb83111f58cb5429d0d54d367de74f414Christian Maeder\texttt{translation} field. The available provers and translations can be
615303ffb83111f58cb5429d0d54d367de74f414Christian Maederqueried by \texttt{?node=0\&translations} and \texttt{?node=0\&provers} or
615303ffb83111f58cb5429d0d54d367de74f414Christian Maedershorter by \texttt{?translations=0} and \texttt{?provers=0}, where instead of
615303ffb83111f58cb5429d0d54d367de74f414Christian Maederthe node number (here \texttt{0}) also a node name can be used.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Miscellaneous Options}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiSet the verbosity level according to \texttt{Int}. Default is 1.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{-q}, \texttt{--quiet}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBe quiet -- no diagnostic output at all. Overrides -v.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPrint usage information and exit.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \texttt{Int} megabytes (needed in case of a stack overflow).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis must be the first option.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskideclaration. The default is \CASL.
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder\item[\texttt{-e ENCODING}, \texttt{--encoding=ENCODING}] Read input files using latin1 or utf8 encoding. The default is still latin1.
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder\item[\texttt{--unlit}] Read literate input files.
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder\item[\texttt{--relative-positions}] Just uses the relative library name in positions of warning or errors.
38914aa544a92aa72e537446cfff297dc6109e04Christian Maeder\item[\texttt{-U FILE}, \texttt{--xupdate=FILE}] update a development graph according to special xml update information (still experimental).
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\section{Proofs with \Hets}\label{sec:Proofs}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe proof calculus for development graphs (Sect.~\ref{sec:DevGraph}) reduces
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederglobal theorem links to local proof goals. Local proof goals (indicated by red
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedernodes in the development graph) can be eventually discharged using a theorem
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederprover, 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''.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe top list on the left shows all goal names prefixed with the proof
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichstatus in square brackets. A proved goal is indicated by a `+', a `-'
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichindicates a disproved goal, a space denotes an open goal, and a
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich`$\times$' denotes an inconsistent specification (aka a fallen `+';
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsee below for details).
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\includegraphics[width=\textwidth]{proofmanagement1}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\caption{Hets Goal and Prover Interface\label{fig:proof_window}}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIf you open this GUI when processing the goals of one node for the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichfirst time, it will show all goals as open. Within this list you can
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederselect those goals that should be inspected or proved. The GUI elements are the following:
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\begin{itemize}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item The button `Display' shows the selected goals in the ASCII syntax of
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder this theory's logic in a separate window.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item By pressing the `Proof details' button a window is opened where for each
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder proved goal the used axioms, its proof script, and its proof are shown ---
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder the level of detail depends on the used theorem prover.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item With the `Prove' button the actual prover is launched. This is described
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder in more detail in the paragraphs below.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item The list `Pick Theorem Prover:' lets you choose one of the connected
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder provers (among them \Isabelle, MathServe Broker, \SPASS, Vampire, and
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder zChaff, described below). By pressing `Prove' the selected prover is
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder launched and the theory along with the selected goals is translated via the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder shortest possible path of comorphisms into the provers logic.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item The pop-up choice box below `Selected comorphism path:' lets you pick a
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder (composed) comorphism to be used for the chosen prover.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item Since the amount and kind of sentences sent to an ATP system is a major
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder factor for the performance of the ATP system, it is possible to select in
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder the bottom lists the axioms and proven theorems that will comprise the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder theory of the next proof attempt. Based on this selection the sublogic may
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder vary and also the available provers and comorphisms to provers. Former
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder theorems that are imported from other specifications are marked with the
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder prefix `(Th)'. Since former theorems do not add additional logical content,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder they may be safely removed from the theory.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item If you press the bottom-right `Close' button the window is closed and
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder the status of the goals' list is integrated into the development graph. If
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder all goals have been proved, the selected node turns from red into green.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\item All other buttons control selecting list entries
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\subsection{Consistency Checker}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\label{sec:CC}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederSince proofs are void if specifications are inconsistent, the consistency
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedershould be checked (if possible for the given logic) by the ``Consistency
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederchecker'' shown in Fig. \ref{fig:cons_window}. This GUI is invoked from
6135dff41a8cf187b8821aab7def02f624f8e856Christian Maederthe `Edit' menu as it operates on all nodes.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederThe list on the left shows all node names prefixed with a consistency status
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederin square brackets that is initially empty. A consistent node is indicated by
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedera `+', a `-' indicates an inconsistent node, a `t' denotes a timeout of the last
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederchecking attempt.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\begin{figure}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\includegraphics[width=\textwidth]{ConsistencyChecker}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\caption{Hets Consistency Checker Interface\label{fig:cons_window}}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederFor some selection of nodes (of a common logic) a model finder should be
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederselectable from the `Pick Model finder:' list. Currently only for ``darwin''
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedersome \CASL models can be re-constructed. When pressing `Check', possibly after
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder`Select comorphism path:', all selected nodes will be checked, spending at
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedermost the number of seconds given under `Timeout:' on each node. Pressing
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder`Stop' allows to terminate this process if too many nodes have been chosen.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederEither by `View results' or automatically the `Results of consistency check'
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder(Fig. \ref{fig:cons_res}) will pop up and allow you to inspect the models for
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedernodes, if they could be constructed.
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\begin{figure}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\includegraphics[width=\textwidth]{ConsCheckResults}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\caption{Consistency Checker Results\label{fig:cons_res}}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsection[Automated Theorem Proving Systems]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich{Automated Theorem Proving Systems\\(Logic SoftFOL)}
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke\label{sec:ATP}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\includegraphics[width=\textwidth]{spassGUI1}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiAll ATPs integrated into \Hets share the same GUI, with only a slight
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedermodification for the MathServe Broker: the input field for extra options is
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederinactive. Figure~\ref{fig:SPASS_GUI} shows the instantiation for \SPASS, where
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederin the top right part of the window the batch mode can be controlled. The
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederleft side shows the list of goals (with status indicators). If goals are
d3e4f883d74b0cd6b1708141fddc20e895e82eb1Eugen Kuksatimed out (indicated by `t') it may help to activate the check box `Include
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederpreceeding proven theorems in next proof attempt' and pressing `Prove all'
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederOn the bottom right the result of the last proof
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederattempt is displayed. The `Status:' indicates `Open', `Proved', `Disproved',
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder`Open (Time is up!)', or `Proved (Theory inconsistent!)'. The list of `Used
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederAxioms:' is filled by \SPASS. The button `Show Details' shows the whole output
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederof the ATP system. The `Save' buttons allow you to save the input and
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maederconfiguration of each proof for documentation. By `Close' the results for all
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maedergoals are transferred back to the Proof Management GUI.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichZimmer provides a unified interface to a range of different ATP
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsystems; the most important systems are listed in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichTable~\ref{tab:MathServe}, along with their capabilities. These
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcapabilities are derived from the \emph{Specialist Problem Classes}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich(SPCs) defined upon the basis of logical, language and syntactical
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichproperties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichOnly two of the Web services provided by the MathServe system are used
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichby \Hets currently: Vampire and the brokering system. The ATP systems
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichare offered as Web Services using standardized protocols and formats
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsuch as SOAP, HTTP and XML. Currently, the ATP system Vampire may be
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichaccessed from \Hets via MathServe; the other systems are only reached
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichafter brokering.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{table}[t]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \begin{threeparttable}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \begin{tabular}{|l|c|p{7cm}|}\firsthline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich ATP System & Version & Suitable Problem Classes\tnote{a}\\
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \hhline{|=|=|=|}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich DCTP & 10.21p & effectively propositional \\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich EP & 0.91 & effectively propositional; real first-order, no
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich equality; real first-order, equality\\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich Otter & 3.3 & real first-order, no equality\\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \SPASS & 2.2 & effectively propositional; real first-order, no
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich equality; real first-order, equality\\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich Vampire & 8.0 & effectively propositional; pure equality, equality
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich clauses contain non-unit equality clauses; real first-order, no
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich equality, non-Horn\\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich Waldmeister & 704 & pure equality, equality clauses are unit
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich equality clauses\\\lasthline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \end{tabular}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich %\renewcommand{\thempfootnote}{\arabic{mpfootnote}}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich %\footnotetext%[\value{footnote}\stepcounter{footnote}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \begin{tablenotes}\footnotesize
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich {The list of problem classes for each ATP system is not
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich exhaustive, but only the most appropriate problem classes are
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich named according to benchmark tests made with MathServe by
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich J\"urgen Zimmer.}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \end{tablenotes}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \end{threeparttable}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \caption{ATP systems provided as Web services by MathServe}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\vspace*{-4mm}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \label{tab:MathServe}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsubsection*{\SPASS}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe ATP system \SPASS \cite{WeidenbachEtAl02} is a resolution-based
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiprover for first-order logic with equality. Furthermore, it provides a soft
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskityping mechanism with subsorting that treats sorts as unary
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichpredicates. The ATP \SPASS should be installed locally and available
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichthrough your \verb,$PATH, environment variable.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsubsection*{Vampire}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich% http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe ATP system Vampire is the winner of the last 5 CADE ATP System
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichCompetitions (CASC) (2002--2006) in the devisions \verb,FOF, and
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\verb,CNF,. It is a resolution based ATP system supporting the calculi
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichof ordered binary resolution and superposition for handling equality.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\url{http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichfor detailed information. The connection to Vampire is achieved by
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichusing an Web service of the MathServe system.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsubsection*{MathServe Broker}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich% The classes ``effectively propositional'' and ``real first-order''
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich% apply to first-order problems that are distinguished by the finiteness
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich% of the Herbrand universe; an effectively propositional problem has
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich% only constants (generated by finitely many terms) whereas a real
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich% first-order problem contains true functions with an infinite Herbrand
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe brokering service chooses the most appropriate ATP system
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichupon a classification based on the SPCs, and on a training with the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichlibrary Thousands of Problems for Theorem Provers (TPTP)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\cite{ZimmerAutexier06}. The TPTP format
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichhas been introduced by Sutcliffe and Suttner for the annual
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcompetition CASC \cite{Sutcliffe:2006:CASC} and provides a unified
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsyntax for untyped FOL with equality, but without any symbol
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsection{Isabelle}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\Isabelle \cite{NipPauWen02} is an interactive theorem prover, which is
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichmore powerful than ATP systems, but also requires more user interaction.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskihas a very small core guaranteeing correctness, and its provers,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskilike the simplifier or the tableaux prover, are built on top of this
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskicore. Furthermore, there is over fifteen years of experience with it,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederand several mathematical textbooks have been partially
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \index{formal!verification}%
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\Isabelle is a tactic based theorem prover implemented in standard ML.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe main \Isabelle logic (called Pure) is some weak intuitionistic type
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskitheory with polymorphism. The logic Pure is used to represent a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskivariety of logics within \Isabelle; one of them being \HOL (higher-order
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskilogic). For example, logical implication in Pure (written
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\texttt{==>}, also called meta-implication), is different from logical
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiimplication in \HOL (written \texttt{-->}, also called object
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiIt is essential to be aware of the fact that the \Isabelle/\HOL logic
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiis different from the logics that are encoded into it via comorphisms.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiTherefore, the formulas appearing in subgoals of proofs with \Isabelle
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiwill not conform to the syntax of the original input logic. They may
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskieven use features of \Isabelle/\HOL such as higher-order functions
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithat are not present in an input logic like \CASL.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\Isabelle is started with ProofGeneral
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\cite{url:Emacs,url:XEmacs}.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe \Isabelle theory file conforms to the Isabelle/Isar syntax
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\cite{NipPauWen02}. It starts with the theory (encoded along the selected
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski comorphism), followed by a list of theorems. Initially, all the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski theorems have trivial proofs, using the `oops` command. However, if
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski you have saved earlier proof attempts, \Hets will patch these into
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski the generated \Isabelle theory file, ensuring that your previous work
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski is not lost. (But note that this patching can only be successful
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski if you do not rename specifications, or change their structure.) You
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski now can replace the 'oops' commands with real \Isabelle proofs, and
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski use Proof General to step through the proofs. You finish your session
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski by saving your file (using the Emacs file menu, or the Ctrl-x Ctrl-s
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder key sequence), and by exiting Emacs (Ctrl-x Ctrl-c).
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\subsection{VSE}
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder\label{subsec:VSE}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski The specification environment Verification Support Environment
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski(VSE) \cite{VSE00}, developed at
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederDFKI Saarbr\"ucken, provides an industrial-strength methodology
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederfor specification and verification of imperative programs.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiVSE provides an interactive prover, which supports a Gentzen style
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskinatural deduction calculus for dynamic logic.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThis logic is an extension of first-order logic with two additional
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskikinds of formulas
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskithat allow for reasoning about programs. One of them is the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskibox formula $[\alpha]\varphi$, where $\alpha$ is a program written in an imperative
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskilanguage, and $\varphi$ is a dynamic logic formula.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe meaning of $[\alpha]\varphi$ can be roughly put as
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski``After every terminating execution of $\alpha$, $\varphi$ holds.''.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe other new kind
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiof formulas is the diamond formula $\langle\alpha\rangle\varphi$, which is the dual counter part
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiof a box formula. The meaning of $\langle\alpha\rangle\varphi$
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskican be described as ``After some terminating execution of $\alpha$,
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski$\varphi$ holds''.
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederA VSE specification or something that can be translated to VSE (currently only
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maeder\CASL) can be sent to the VSE prover via the node menu of development graph
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedernodes in two different ways. You can either select VSE from the theorem prover
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederchoice box shown after ``Prove'' or you can select ``Prove VSE Structured''.
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederThe first choice will call VSE with a single flattened theory whereas a
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederstructured call will translate all nodes with ingoing links to the current one
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederVSE pops up with a ``project'' window. In this window you can choose ``Work
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederon'' and ``specification''. Besides the builtin specification ``boolean''
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederthere is at least one specification from your development graph that you
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedercan select for proving. For a structured choice you'll have specifications
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederfor all underlying nodes that you should work on in a bottom up fashion.
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian MaederThe state created by VSE will be stored in a \texttt{.tar} file (within the
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maedercurrent directory) that preserves proofs for replay later on as long as you
2158a22599ee3ace186a7ce197cedda5d9bcadbfChristian Maederdon't change library or node names.
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke\subsection{zChaff}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederzChaff is a solver for satisfiabily problems of boolean formulas
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke(\normalTEXTSC{S}{AT})
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederin CNF. It is connected as a prover for propositional logic to \Hets. The prover
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\SPASS is used to transform arbitrary boolean formulas to CNF. zChaff
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederimplements the \normalTEXTSC{C}{HAFF}\xspace algorithm. We are
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckeusing the property, that a conjecture under the assumption of a set of axioms is
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedertrue, if the variables of axioms together with the negation of the conjecture
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckehave no satisfying assignment, to prove theorems with zChaff. That is why you see
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckethe result \normalTEXTSC{U}{NSAT}\xspace in the proof details, if a theorem has been proved
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederto be true. zChaff uses the same ATP GUI as the provers for SoftFOL (ref. to section
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\ref{sec:ATP}). zChaff does not accept any options apart from the time-limit. The
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckecurrent integration of zChaff into \Hets has been tested with zChaff 2004.11.15.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\subsection{Reduce}
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian MaederThis is a connection to the computer algebra system from
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\url{http://www.reduce-algebra.com/}. Installation is possible as follows:
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\begin{verbatim}
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maedersvn co https://reduce-algebra.svn.sourceforge.net/svnroot/reduce-algebra
6e1fc365493855f4d07aaa5eb4dd4df47911cacaChristian Maeder./configure --with-csl
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maeder\end{verbatim}
a05d3f31f5b28c68df892a785c1adb870ae430d7Christian MaederThe binary \texttt{redcsl} will be searched in the \texttt{PATH} or is taken
45dc2929dcad39b4dcc6a8e11cd9a4ab7b2ef8b4Christian Maederfrom the \texttt{HETS\_REDUCE} environment variable.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\subsection{Pellet}
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederPellet is a popular open-source \DL-reasoner for \SROIQ, which is the logic
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian Maederunderlying OWL 2, written in Java. A Java Runtime Environment (in version $> 1.5$)
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeis needed to run Pellet. For the integration into \Hets the environment variable
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\verb+PELLET_PATH+ has to be set to the root-directory of the Pellet installation.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckePellet uses the same ATP GUI as the provers for SoftFOL (ref. to section
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\ref{sec:ATP}).
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\subsection{Fact++}
07f9230ffdf4bb128e4e07f2d01efdf433ebe45bChristian MaederFact++ is a \DL-reasoner for \SROIQ, which is the logic underlying OWL 2, written in
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederC++. Fact++ is integrated into \Hets via the OWL-API, which is written in Java.
1f9823949404b1a298541f38aa7fb4f129ff46f0cmaederA Java Runtime Environment (in version $>= 1.6$) has to be installed. To use Fact++,
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederthe environment variable \verb+HETS_OWL_TOOLS+ has to be set to the directory
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckecontaining the files
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\begin{verbatim}
4ffc423a7df8af7e7d7e563a15471da4505ddeb5ignaziolib/uk.ac.manchester.cs.owl.factplusplus-P5.0-v1.6.3.1.jar
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\end{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\begin{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\end{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeon a 32bits-Linux-system or
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\begin{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\end{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckein a 64bits-Linux-system. Fact++ does not support options.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeFact++ uses the same ATP GUI as the provers for SoftFOL (ref. to section
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\ref{sec:ATP}).
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\subsection{E-KRHyper}
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederE-KRHyper\footnote{\url{http://www.uni-koblenz.de/~bpelzer/ekrhyper/}}
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederis an extension of
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeKRHyper\footnote{\url{http://www.uni-koblenz.de/~wernhard/krhyper/}} by
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckehandling of equality. E-KRHyper is an automatic first order theorem
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeprover and model finder based on the Hyper Tableaux Calculus\cite{Baumgartner:1996}.
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederE-KRHyper is optimized for being integrated into other systems. In the current
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeimplementation we use a default tactics script, that can be influenced by the user.
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederThe options of E-KRHyper are written in a Prolog-like syntax as in
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\begin{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke#(set_parameter(timeout_termination_method,0)).
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\end{verbatim}
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maederthe ``.'' at the end of each option is mandatory. To get an overview of
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeE-KRHyper's options, run the command
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\begin{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\end{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckein a terminal. Then enter the command
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\begin{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\end{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeat the prompt of E-KRHyper, to display its help information, which is basically
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckea long list of all available parameters. You can exit E-KRHyper by the command
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\begin{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\end{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeE-KRHyper uses the same ATP GUI as the other provers for SoftFOL (ref. to section
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\ref{sec:ATP}).
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\subsection{Darwin}
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederDarwin is an automatic first order prover and model finder implementing the Model
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeCalculus\cite{Baumgartner:2003}. The integration of Darwin as a consistency checker
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maedersupports the display of models (if they can be constructed) in \CASL-syntax.
0093b49b89d814da4164d43e754509a90a00e9eeChristian MaederEprover is needed to be in the system-path, if Darwin is used with \Hets, since
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeDarwin uses Eprover for clausification of first-order formulae.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeDarwin supports a wide range of options, to get an overview of them run the command
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\begin{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\end{verbatim}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckein a terminal.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeDarwin uses the same ATP GUI as the other provers for SoftFOL (ref. to section
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\ref{sec:ATP}).
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\subsection{QuickCheck}
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\subsection{minisat}
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\subsection{Truth tables}
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder\subsection{CspCASLProver}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Limits of Hets}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\Hets is still intensively under development. In particular, the
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskifollowing points are still missing:
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\begin{itemize}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item There is no proof support for architectural specifications.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\item Distributed libraries are always downloaded from the local disk,
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskinot from the Internet.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\item Version numbers of libraries are not considered properly.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item The proof engine for development graphs provides only experimental
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskisupport for hiding links and for conservativity.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Architecture of Hets}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe architecture of \Hets is shown in Fig.~\ref{fig:hets}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHow is a single logic implemented in the Heterogeneous Tool Set?
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThis is depicted in the left column of Fig.~\ref{fig:hets}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\Hets provides an abstract interface for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{institution!independence}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{independence, institution}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinstitutions, so
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthat new logics can be integrated smoothly.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn order to do so, a parser,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia static checker and a prover for basic specifications in the logic have
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito be provided.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{figure}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{center}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederclass Logic lid sign morphism sentence basic_spec symbol_map
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | lid -> sign morphism sentence basic_spec symbol_map where
30256573a343132354b122097b0ee1215dda1364Till Mossakowski identity :: lid -> sign -> morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowski compose :: lid -> morphism -> morphism -> morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowski dom, codom :: lid -> morphism -> sign
30256573a343132354b122097b0ee1215dda1364Till Mossakowski parse_basic_spec :: lid -> String -> basic_spec
30256573a343132354b122097b0ee1215dda1364Till Mossakowski parse_symbol_map :: lid -> String -> symbol_map
30256573a343132354b122097b0ee1215dda1364Till Mossakowski parse_sentence :: lid -> String -> sentence
30256573a343132354b122097b0ee1215dda1364Till Mossakowski empty_signature :: lid -> sign
30256573a343132354b122097b0ee1215dda1364Till Mossakowski basic_analysis :: lid -> sign -> basic_spec -> (sign, [sentence])
30256573a343132354b122097b0ee1215dda1364Till Mossakowski stat_symbol_map :: lid -> sign -> symbol_map -> morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowski map_sentence :: lid -> morphism -> sentence -> sentence
30256573a343132354b122097b0ee1215dda1364Till Mossakowski lid -> [(sign, [sentence]) -> [sentence] -> Proof_status]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski cons_checkers :: lid -> [(sign, [sentence]) -> Proof_status]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederclass Comorphism cid
30256573a343132354b122097b0ee1215dda1364Till Mossakowski lid1 sign1 morphism1 sentence1 basic_spec1 symbol_map1
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder lid2 sign2 morphism2 sentence2 basic_spec2 symbol_map2
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | cid -> lid1 lid2 where
30256573a343132354b122097b0ee1215dda1364Till Mossakowski sourceLogic :: cid -> lid1 targetLogic :: cid -> lid2
30256573a343132354b122097b0ee1215dda1364Till Mossakowski map_theory :: cid -> (sign1, [sentence1]) -> (sign2, [sentence2])
30256573a343132354b122097b0ee1215dda1364Till Mossakowski map_morphism :: cid -> morphism1 -> morphism2
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{verbatim}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\caption{The basic ingredients of logics and logic comorphisms}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\label{fig:logic:all}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiEach logic is realized in the programming language Haskell
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{PeytonJones03} by a set of types and functions, see
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFig.~\ref{fig:logic:all}, where we present a simplified, stripped down
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiversion, where e.g.\ error handling is ignored. For technical reasons
30256573a343132354b122097b0ee1215dda1364Till Mossakowskia logic is \emph{tagged} with a unique identifier type (\texttt{lid}),
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiwhich is a singleton type the only purpose of which is to determine
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiall other type components of the given logic. In Haskell jargon, the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinterface is called a multiparameter type class with functional
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidependencies \cite{TypeClasses}. The Haskell interface for logic
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitranslations is realised similarly.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe logic-independent modules in \Hets can be found in the right half
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof Fig.~\ref{fig:hets}. These modules comprise roughly one third of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\Hets' 100.000 lines of Haskell code.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe heterogeneous parser transforms a string
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiconforming to the syntax in Fig.~\ref{fig:lang}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskito an abstract syntax tree, using the \texttt{Parsec} combinator parser
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{Parsec}. Logic and translation names are looked up in the logic
30256573a343132354b122097b0ee1215dda1364Till Mossakowskigraph --- this is necessary to be able to choose the correct parser
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor basic specifications. Indeed, the parser has a state that carries
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe current logic, and which is updated if an explicit specification
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof the logic is given, or if a logic translation is encountered (in
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe latter case, the state is set to the target logic of the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitranslation). With this, it is possible to parse basic specifications
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiby just using the logic-specific parser of the current logic as
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiobtained from the state.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe static analysis is based on the static analysis of basic
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispecifications, and transforms an abstract syntax tree to a
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidevelopment graph (cf.\ Sect.~\ref{sec:DevGraph} above). Starting with a
30256573a343132354b122097b0ee1215dda1364Till Mossakowskinode corresponding to the empty theory, it successively extends (using
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe static analysis of basic specifications) and/or translates (along
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe intra- and inter-logic translations) the theory, while
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisimultaneously adding nodes and links to the development graph.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHeterogeneous proof management is done using heterogeneous
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidevelopment graphs, as described in Sect.~\ref{sec:DevGraph}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFor local proof goals, logic-specific provers are invoked,
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskisee Sect.~\ref{sec:Proofs}.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\Hets can store development graphs, including their proofs.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiTherefore, \Hets uses the so-called
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \index{ATerms}%
30256573a343132354b122097b0ee1215dda1364Till MossakowskiATerm format \cite{BJKO00}, which is used as interchange format
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor interfacing with other tools.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiMore details can be found in \cite{Habil,MossakowskiEtAl07b}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiand in the overview of modules provided in the developers section
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof the \Hets home page at \url{http://www.dfki.de/sks/hets}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{center}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\includegraphics[scale=0.4]{hets2007}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Architecture of the heterogeneous tool set.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{fig:hets}}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets is mainly maintained by
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiChristian Maeder (Christian.Maeder@dfki.de) and Till Mossakowski
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(Till.Mossakowski@dfki.de). The mailing list is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \url{hets-users@informatik.uni-bremen.de}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskithe homepage is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\url{http://www.informatik.uni-bremen.de/mailman/listinfo/hets-users}.
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiYou need to subscribe to the list before you can send a mail.
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiBut note that subscription is very easy!
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiIf your favourite logic is missing in \Hets, please tell us
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maeder(hets-users@informatik.uni-bremen.de). We will take your feedback into account
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maederwhen deciding which logics and proof tools to integrate next into \Hets. Help
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maederwith integration of more logics and proof tools into \Hets is also welcome.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\paragraph{Acknowledgement}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe heterogeneous tool set \Hets would not have possible
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiwithout cooperation with many people.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiBesides the authors, the following people have been involved
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiin the implementation of \Hets:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiKatja Abu-Dib,
650631bddf665ec5ef991bf4ce2f569b7709d104Christian MaederFrancisc Nicolae Bungiu,
3cca22bf00dd189214595454eb696fdf954f366fMihai CodescuCodru\c ta G\^ arlea,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederDominik Dietrich,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCarsten Fischer,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiJorina Freya Gerken,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederAndy Gimblett,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiRainer Grabbe,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSonja Gr\"{o}ning,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiDaniel Hausmann,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiWiebke Herding,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCui ``Ken'' Jian,
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till MossakowskiAnton Kirilov,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiTina Krausser,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMartin K\"{u}hl,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederKlaus L\"{u}ttich,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMaciek Makowski,
650631bddf665ec5ef991bf4ce2f569b7709d104Christian MaederFelix Gabriel Mance,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederFlorian Mossakowski,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiImmanuel Normann,
38914aa544a92aa72e537446cfff297dc6109e04Christian MaederSebastian Raible,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederLiam O'Reilly,
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till MossakowskiRazvan Pascanu,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDaniel Pratsch,
38914aa544a92aa72e537446cfff297dc6109e04Christian MaederCorneliu-Claudiu Prodescu,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiFelix Reckers,
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian MaederAdri\'{a}n Riesco,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederMarkus Roggenbach,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederPascal Schmidt,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederEwaryst Schulz,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederKristina Sojakova,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiPaolo Torrini,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederJonathan von Schroeder,
38914aa544a92aa72e537446cfff297dc6109e04Christian MaederSimon Ulbricht,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiRen\'{e} Wagner,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederJian Chun Wang,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederZicheng Wang, and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThiemo Wiedemeyer.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\Hets has been built based on experiences with its
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \index{Cats@\Cats}%
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \index{Maya@\MAYA}%
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe \CASL Tool Set (\Cats)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\cite{Mossakowski:2000:CST,Mossakowski:1998:SSA}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiprovides parsing and static analysis for \CASL.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIt has been developed by the first author with help
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederof Mark van den Brand, Kolyang, Bartek Klin, Pascal Schmidt and
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiFrederic Voisin.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\MAYA \cite{Autexier:2002:IHD,AutexierEtal02} is a proof management
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskitool based on development graphs. \MAYA only supports development
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskigraphs without hiding and without logic translations. \MAYA has been
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskideveloped by Serge Autexier and Dieter Hutter.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiWe also want to thank Agn\`es Arnould, Thibaud Brunet, Pascale LeGall,
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian MaederKathrin Hoffmann, Bruno Langenstein, Katiane Lopes,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski%Klaus L\"uttich, Christian Maeder,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederStefan Merz, Maria Martins Moreira, Christophe
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiRingeissen, Markus Roggenbach, Dmitri Schamschurko, Lutz Schr\"oder,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederKonstantin Tchekine and Stefan W\"olfl
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifor giving feedback about \Cats, HOL-CASL and \Hets. Finally,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskispecial thanks to Christoph L\"uth and George Russell
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifor help with connecting \Hets to their UniForM workbench.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\bibliographystyle{plain}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\bibliography{cofibib,cofi-ann,UM,hets,kl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{document}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%%% Local Variables:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% mode: latex
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% TeX-master: "UserGuide"