UserGuide.tex revision 749b7d8ea5a481831375f49ae50239dd8e3d2d12
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage[show]{ed} % set to hide for producing a released version
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{alltt}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{color}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{url}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{threeparttable,hhline}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage[pdfborder=0 0 0,bookmarks,
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskipdfauthor={Till Mossakowski, Christian Maeder, Mihai Codescu},
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichpdftitle={Hets User Guide}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich{hyperref} %% do not load more packages after this line!!
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\QUERY}[1]%{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\eat}[1]{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\IEXT}[1] {\\#1\I}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\IEND} {\I\END}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{EXAMPLEFORMAT} {}{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%% Added by MB to have some extra vertical space after the ``main'' examples
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%% following the points (and some others in the text):
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{DETAILSFORMAT} {}{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \begin{minipage}{0.9\textwidth}\it}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {\end{minipage}\par\medskip}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\SLIDESMALL} {}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\SLIDESONLY}[1] {}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% SIMULATING SMALL-CAPS FOR BOLD, EMPH
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%\newcommand {\CoFI}{CoFI\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%%%% Klaus macros
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\newcommand{\SROIQ}{$\mathcal{SROIQ}$(\textbf{D})\xspace}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\newcommand{\DL}{DL\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%%%%% end of Klaus macros
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LCF}{LCF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\ASF}{ASF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SDF}{SDF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CCC}{CCC\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{document}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\title{{\bf \protect{\LARGEHets} User Guide}\\
c488ac18796ad6383b1edf7fa2820edc8296c89eChristian Maeder-- Version 0.95 --}
e91e02579a34e005734059ad09e0d1d1304a03e0Till Mossakowski\author{Till Mossakowski, Christian Maeder,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Mihai Codescu, Dominik L\"{u}cke\\[1em]
464c78620a182d2e8fbd125098045eae8788e2bdTill MossakowskiDFKI Lab Bremen, Bremen, Germany.\\[1em]
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiComments to: hets-users@informatik.uni-bremen.de \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(the latter needs subscription to the mailing list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Introduction}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe central idea of the Heterogeneous Tool Set (\protect\Hets) is to
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiprovide a general framework for formal methods integration and proof
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskimanagement. One can think of \Hets acting like a motherboard where
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskidifferent expansion cards can be plugged in, the expansion cards here
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskibeing individual logics (with their analysis and proof tools) as well
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskias logic translations. Individual logics and their analysis and proof
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskitools can be plugged into the \Hets motherboard using an
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiobject-oriented interface based on institutions
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\cite{GoguenBurstall92}. The \Hets motherboard already has plugged in
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskia number of expansion cards (e.g., the theorem provers Isabelle, SPASS
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiand more, as well as model finders). Hence, a variety of tools is
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiavailable, without the need to hard-wire each tool to the logic at
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{figure}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\begin{center}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \includegraphics[width=0.45\textwidth]{hets-motherboard}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\caption{The \Hets motherboard and some expansion cards}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\Hets supports a number of input languages directly, such as \CASL,
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiCommon Logic, OWL-DL, Haskell, and Maude. For heterogeneous
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskispecification, \Hets offers language heterogeneous \CASL.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiHeterogeneous \CASL (\HetCASL) generalises the structuring
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\CASL \cite{CASL-UM,CASL/RefManual} to arbitrary logics
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski(if they are formalised as institutions and plugged into
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskithe \Hets motherboard), as well as to heterogeneous
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskicombination of specification written in different logics.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiFig.~\ref{fig:lang} for a simple subset of the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\HetCASL syntax, where \emph{basic specifications} are unstructured
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskispecifications or modules written in a specific logic. The graph of
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskicurrently supported logics and logic translations (the latter are also
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskicalled comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidegree of support by \Hets in Fig.~\ref{fig:Languages}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{figure}[ht]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederSPEC ::= BASIC-SPEC
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | SPEC then SPEC
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | SPEC then %implies SPEC
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | SPEC with SYMBOL-MAP
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | SPEC with logic ID
30256573a343132354b122097b0ee1215dda1364Till MossakowskiDEFINITION ::= logic ID
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | spec ID = SPEC end
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | view ID : SPEC to SPEC = SYMBOL-MAP end
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | view ID : SPEC to SPEC = with logic ID end
30256573a343132354b122097b0ee1215dda1364Till MossakowskiLIBRARY = DEFINITION*
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{verbatim}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\caption{Syntax of a simple subset of the heterogeneous
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispecification language.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispecific syntax, while \texttt{ID} stands for some form of
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiidentifiers.\label{fig:lang}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWith \emph{heterogeneous structured specifications}, it is possible to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicombine and rename specifications, hide parts thereof, and also
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprescribe the structure of implementations. \emph{Specification
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder libraries} are collections of named structured and architectural
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets consists of logic-specific tools for the parsing and static
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskianalysis of the different involved logics, as well as a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic-independent parsing and static analysis tool for structured and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito call the logic-specific tools whenever a basic specification is
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\Hets is based on the theory of institutions \cite{GoguenBurstall92},
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiwhich formalize the notion of a logic. The theory behind \Hets is laid
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiout in \cite{Habil}. A short overview of \Hets is given in
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\cite{MossakowskiEA06,MossakowskiEtAl07b}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Logics supported by Hets}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe following list of logics (formalized as so-called institutions
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{GoguenBurstall92}) is currently supported by \Hets:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \includegraphics[scale=0.4]{LogicGraph}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\caption{Graph of logics currently supported by \Hets. The more an
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{fig:LogicGraph}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{figure}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{center}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|c|c|c|}\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL & x & x & - \\\hline
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski\CoCASL & x & x & - \\\hline
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maeder\ModalCASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\HasCASL & x & x & - \\\hline
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiHaskell & (x) & x & - \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\CspCASL & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CspCASL\_Trace & - & - & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CspCASL\_Failure & - & - & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiConstraint\CASL & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiTemporal & x & (x) & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiRelScheme & x & (x) & - \\\hline
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiDFOL & x & (x) & - \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiExtModal & x & (x) & - \\\hline
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiLF & x & (x) & - \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%Structured specifications & x & x & (x) \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%Architectural specifications & x & x & -\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\CASLDL & x & - & - \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDMU & x & - & - \\\hline
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiOWL DL & x & x & - \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiPropositional & x & x & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSoftFOL & x & - & x \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederMaude & x & x & - \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiVSE & x & x & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Isabelle & (x) & - & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\caption{Current degree of \Hets support for the different languages.\label{fig:Languages}}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{description}
30256573a343132354b122097b0ee1215dda1364Till 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
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski%specify calculi for time and space.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiWe have implemented the \CASL logic in such a way that much of the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiimplementation can be re-used for \CASL extensions as well; this
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiis achieved via ``holes'' (realized via polymorphic variables) in the
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskitypes for signatures, morphisms, abstract syntax etc. This eases
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederintegration 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,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskisuited for the specification of process types and reactive systems.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe central proof method is coinduction.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[ModalCASL] \cite{ModalCASL}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski is an extension of \CASL with multi-modalities and
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiterm modalities. It allows the specification of modal systems with
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiKripke's possible worlds semantics. It is also possible to express
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicertain forms of dynamic logic.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[HasCASL] is a higher order extension of \CASL allowing
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski polymorphic datatypes and functions. It is closely related to the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski programming language Haskell and allows program constructs being
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski embedded in the specification.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe language is summarized in \cite{HasCASL/Summary}, the semantics
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiin \cite{Schroder05b,Schroder-habil}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Haskell] is a modern, pure and strongly typed functional
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski programming language. It simultaneously is the implementation
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski language of \Hets, such that in the future, \Hets might be applied
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiThe definitive reference for Haskell is \cite{PeytonJones03},
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski with the process algebra CSP.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[ConstraintCASL] is an experimental logic for the specification
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiof qualitative constraint calculi.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[OWL DL] is the Web Ontology Language (OWL) recommended by the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski World Wide Web Consortium (W3C, \url{http://www.w3c.org}). It is
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski used for knowledge representation and the Semantic Web
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \cite{berners:2001:SWeb}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederHets calls an external OWL DL parser
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski written in JAVA to obtain the abstract syntax for an OWL file and its
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski imports. The JAVA parser is also doing a first analysis classifying
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Hets only supports the last two, more restricted variants.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski structuring of the OWL imports is displayed as Development Graph.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[CASL-DL] \cite{OWL-CASL-WADT2004}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiis an extension of a restriction of \CASL, realizing
30256573a343132354b122097b0ee1215dda1364Till Mossakowskia strongly typed variant of OWL DL in \CASL syntax.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \CASL with cardinality restrictions for the description of sorts and
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski unary predicates. The restrictions are based on the equivalence
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich between \CASLDL, OWL~DL and \SHOIN. Compared to \CASL only unary
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski and binary predicates, predefined datatypes and concepts (subsorts
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich of the topsort Thing) are allowed. It is used to bring OWL DL and
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \CASL closer together.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Propositional] is classical propositional logic, with
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe zChaff SAT solver \cite{Herbstritt03} connected to it.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[SoftFOL] \cite{LuettichEA06a} offers three automated theorem
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski proving (ATP) systems for first-order logic with equality: (1) \SPASS
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \cite{WeidenbachEtAl02}; (2) Vampire \cite{RiazanovV02}; and (3)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski MathServe Broker\footnote{which chooses an appropriate ATP upon a
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski classification of the FOL problem} \cite{ZimmerAutexier06}.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski These together comprise some of the most advanced theorem provers
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski for first-order logic.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[\Isabelle] \cite{NipPauWen02} is an interactive theorem prover
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski for higher-order logic.
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\item[VSE] is an interactive theorem prover, see \ref{subsec:VSE}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[DMU] is a dummy logic to read output of ``Computer Aided
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Three-dimensional Interactive Application'' (Catia).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Maude] is a rewrite system \url{http://maude.cs.uiuc.edu/} for
30256573a343132354b122097b0ee1215dda1364Till Mossakowski first-order logic.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederVarious logics are supported with proof tools. Proof support for the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederother logics can be obtained by using logic translations to a
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprover-supported logic.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiAn introduction to \CASL can be found in the \CASL User Manual
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\cite{CASL-UM}; the detailed language reference is given in
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiexplain both the \CASL logic and language of basic specifications as
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiwell as the logic-independent constructs for structured and
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiarchitectural specifications. The corresponding document explaining the
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\HetCASL language constructs for \emph{heterogeneous} structured specifications
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis the \HetCASL language summary \cite{Mossakowski04}; a formal
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisemantics as well as a user manual with more examples are in preparation.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiSome of \HetCASL's heterogeneous constructs will be illustrated
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiin Sect.~\ref{sec:HetSpec} below.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\section{Logic translations supported
30256573a343132354b122097b0ee1215dda1364Till 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
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskicomorphisms, is shown in Fig.~\ref{fig:SublogicGraph}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{figure}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \begin{center}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \includegraphics[scale=0.4]{SublogicGraph}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\caption{Graph of most important sublogics currently supported by \Hets,
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowskitogether with their comorphisms.}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\label{fig:SublogicGraph}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiIn more detail, the following list of logic translations is currently
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskisupported by \Hets:
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{tabular}{|l|p{8cm}|}\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2CoCASL & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2CspCASL & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2HasCASL & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2Isabelle & inclusion on sublogic CFOL=
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(translation $(7)$ of \cite{Mossakowski02}) \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2Modal & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2PCFOL & coding of subsorting (SubPCFOL=) by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual} \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskipredicates for the subsorts \\\hline
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiCASL2Propositional & translation of propositional FOL \\\hline
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiCASL2SoftFOL & coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowskimapping types to soft types \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2SoftFOLInduction & same as CASL2SoftFOL but with instances of induction
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiaxioms for all proof goals \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2SubCFOL & coding of partial functions by error elements
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting, i.e. sublogic SubPCFOL=) \\\hline
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiCASL2VSE & inclusion on sublogic CFOL= \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2VSEImport & inclusion on sublogic CFOL= \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCASL2VSERefine & refining translation of CASL.CFOL= to VSE \\\hline
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiCASL\_DL2CASL & inclusion \\\hline
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiCoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCoCASL2Isabelle & extended translation similar to CASL2Isabelle \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCspCASL2CspCASL\_Failure & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCspCASL2CspCASL\_Trace & inclusion \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCspCASL2Modal & translating the CASL data part to ModalCASL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDFOL2CASL & translating dependent types \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDMU2OWL & interpreting Catia output as OWL \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{tabular}{|l|p{7cm}|}\hline
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiHasCASL2HasCASLNoSubtypes & coding out subtypes \\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichHasCASL2HasCASLPrograms & coding of \HasCASL axiomatic recursive definitions
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskias \HasCASL recursive program definitions \\\hline
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiHasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHasCASL2IsabelleOption & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell2Isabelle & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHaskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07} \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederMaude2CASL & encoding of rewrites as predicates \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiModal2CASL & the standard translation of modal logic
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskito first-order logic \cite{blackburn_p-etal:2001a} \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiOWL2CASL & inclusion \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiPropositional2CASL & inclusion \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiRelScheme2CASL & inclusion \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\section{Getting started}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiThe latest \Hets version can be obtained from the
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\Hets tools home page
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Since \Hets is being
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimproved constantly, it is recommended always to use the latest version.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\Hets currently is available (on Intel architectures only) for Linux, Solaris
c5e63ec138b908ac9d15e6843120033bf36a1862Till MossakowskiThere are three possibilities to install \Hets:
c488ac18796ad6383b1edf7fa2820edc8296c89eChristian Maeder\begin{enumerate}
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThe Java-based \Hets installer. Download a \texttt{.jar} file and
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskijava -jar \texttt{file.jar}
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiNote that you need Sun Java 1.4.2 or later. On a Mac, you can just
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskidouble-click on the \texttt{.jar} file.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiThe installer will lead you through the installation with
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedera graphical interface. It will download and install further
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskisoftware (if not already installed on your computer):
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{tabular}{|l|l|p{5cm}|}\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
30256573a343132354b122097b0ee1215dda1364Till MossakowskiTcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiDarwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIf you do not have Sun Java, you can just download the hets binary.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiYou have to unpack it with \texttt{bunzip2} and then put it at
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisome place coverd by your \texttt{PATH}. You also have to
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederinstall the above mentioned software and set
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiseveral environment variables, as explained on the installation page.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiYou may compile \Hets from the sources, please follow the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilink ``Hets: source code and information for developers''
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskion the \Hets web page, download the sources (as tarball or from
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisvn), and follow the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinstructions in the \texttt{INSTALL} file, but be prepared to take some time.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{enumerate}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDepending on your application further tools are supported and may be
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinstalled in addition:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{tabular}{|l|l|p{5cm}|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskizChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiminisat & SAT solver & \url{http://minisat.se/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiPellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiE-KRHyper & theorem prover
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiReduce & computer algebra system
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \url{http://www.reduce-algebra.com/} \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiVSE & theorem prover & (non-public) \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTwelf & & \url{http://twelf.plparty.org/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Analysis of Specifications}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiConsider the following \CASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecification:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAME{Strict\_Partial\_Order} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%PDM\I{} \COMMENTENDLINE{Let's start with a simple example !}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{ITEMS}[\PRED]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\SORT \( Elem \)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\I\PRED \( \_\_<\_\_ : Elem \* Elem \)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski% \COMMENTENDLINE{\PRED abbreviates predicate}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\(\[ \FORALL x,y,z : Elem \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \. \NOT(x < x) \RIGHT{\LABEL{strict}} \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \. x < y \IMPLIES \NOT(y < x) \RIGHT{\LABEL{asymmetric}} \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \. x < y \A y < z \IMPLIES x < z \RIGHT{\LABEL{transitive}} \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{COMMENT}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiNote that there may exist \(x, y\) such that\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskineither \(x < y\) nor \(y < x\).
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\end{BIGEXAMPLE}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets can be used for parsing and
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederchecking static well-formedness of specifications.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \index{parsing}%
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \index{static!analysis}%
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski \index{analysis, static}%
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiLet us assume that the example is in a file named
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{Order.casl} (actually, this file is provided
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederwith the \Hets distribution as \texttt{Hets-lib/UserManual/Chapter3.casl}).
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiThen you can check the well-formedness of the
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskispecification by typing (into some shell):
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\Hets checks both the correctness of this specification
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder with respect to the \CASL syntax, as
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiwell as its correctness with respect to the static semantics (e.g.\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederwhether all identifiers have been declared before they are used,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiwhether operators are applied to arguments of the correct sorts,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwhether the use of overloaded symbols is unambiguous, and so on).
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe following flags are available in this context:
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{description}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item[\texttt{-p}, \texttt{--just-parse}] Just do the parsing
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski -- the static analysis is skipped and no development is created.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski static analysis of (heterogeneous) structured specifications, but
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski leave out the analysis of basic specifications. This can be used
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski for prototyping issues, namely to quickly produce a development graph
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski showing the dependencies among the specifications (cf.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski Sect.~\ref{sec:DevGraph}) even if the individual specifications are
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski not correct yet.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-L DIR}, \texttt{--hets-libdir=DIR}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiUse \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskicalling \Hets).
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item[\texttt{-a ANALYSIS}, \texttt{--casl-amalg=ANALYSIS}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski For the analysis of architectural specification (a quite advanced
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski amalgamability checking
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski algorithm for \CASL logic; it is a comma-separated list of zero or
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski more of the following options:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \begin{description}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \item[\texttt{sharing}] perform sharing analysis for sorts,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski operations and predicates.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \item[\texttt{cell}] perform cell condition check; implies
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \texttt{sharing}. With this option on, the subsort embeddings are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \item[\texttt{colimit-thinness}] perform colimit thinness check;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski implies \texttt{sharing}. The colimit thinness check is less
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski complete and usually takes longer than the full cell condition
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder check (\texttt{cell} option), but may prove more efficient in case
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski of certain specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski If \texttt{ANALYSIS} is empty then amalgamability analysis for
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \CASL is skipped.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski The default value for \texttt{--casl-amalg} is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{cell}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\Hets accepts plain text input files with the following endings:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{tabular}{|l|c|c|}\hline
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiEnding & default logic & structuring language\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.hs} & Haskell & Haskell\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.owl} & OWL DL, OWL Lite & OWL\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.elf} & LF & Twelf \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.maude} & Maude & Maude \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiFurthermore, \texttt{.xml} files are accepted as Catia output if the default
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilogic is set to DMU before a library import or by the ``\texttt{-l DMU}''
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedercommand line option of \Hets.
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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed e.g.\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskito \HasCASL in the following way:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe subsequent specifications are then parsed and analysed as
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiembedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(There are also heterogeneous constructs
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifor explicit translations between logics, see \cite{Mossakowski04}.)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiA \CspCASL specification consists of a \CASL specification
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfor the data part and a \Csp process built over this data part.
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill MossakowskiTherefore, \HetCASL provides a heterogeneous language construct
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{data} as follows:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilibrary Buffer
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski free type List[Elem] ::= nil | cons(Elem; List[Elem])
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ops last: List -> ? Elem;
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder rest: List -> ? List
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski channel read, write : Elem
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski process Buf(List): read, write, List;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski EmptyBuffer : read,write, List;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Buf(l)= read? x :: Elem -> Buf(cons(x,nil)) []
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (if l=nil then STOP else
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski write!last(l) -> Buf(rest(l)))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski EmptyBuffer = Buf(nil)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederHere, the construct \texttt{data List} refers to the \CASL specification
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{List}, which is implicitly embedded into \CspCASL.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe ending \texttt{.hs} is available for directly reading in
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiHaskell programs % and HasSLe specifications,
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiand hence supports the Haskell module system.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskithe logic Haskell has to be chosen explicitly, and the \CASL structuring
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskisyntax needs to be used:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{verbatim}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskilibrary Factorial
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskispec Factorial =
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskifac :: Int -> Int
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskifac n = foldl (*) 1 [1..n]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{verbatim}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiNote that according to the Haskell syntax, Haskell function
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskideclarations and definitions need to start with the first column of
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\section{Development Graphs}\label{sec:DevGraph}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskistructured 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.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiComplementary to definition links, which \emph{define} the theories of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskirelated nodes, \emph{theorem links} serve for \emph{postulating}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskirelations between different theories. Theorem links are the central
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidata structure to represent proof obligations arising in formal
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiTheorem links can be \emph{global} (drawn as solid arrows) or
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\emph{local} (drawn as dashed arrows): a global theorem link
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskipostulates that all axioms of the source node (including the inherited
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiones) hold in the target node, while a local theorem link only postulates
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithat the local axioms of the source node hold in the target node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBoth definition and theorem links can be \emph{homogeneous},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskii.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe logic changes along the arrow. Technically, this is the case
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifor Grothendieck signature morphisms $(\rho,\sigma)$ where
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski$\rho\not=id$. This case is indicated with double arrows.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTheorem links are initially displayed in red.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe \emph{proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski calculus} for development graphs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{MossakowskiEtAl05,Habil} is given by rules
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat allow for proving global theorem links by decomposing them
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinto simpler (local and global) ones. Theorem links that have been
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproved with this calculus are drawn in green. Local theorem links can
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibe proved by turning them into \emph{local proof goals}. The latter
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskican be discharged using a logic-specific calculus as given by an
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskientailment system for a specific institution. Open local
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof goals are indicated by marking the corresponding node in the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidevelopment graph as red; if all local implications are proved, the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinode is turned into green. This implementation ultimately is based
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskion a theorem \cite{Habil} stating soundness and relative completeness
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the proof calculus for heterogeneous development graphs.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following options let \Hets show the development graph of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia specification library:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-g}, \texttt{--gui}] Shows the development graph in a GUI window
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-u}, \texttt{--uncolored}] no colors in shown graphs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following additional options also apply typical rules from the development
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedergraph calculus to the final graph and save applying these rule via the GUI.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-A}, \texttt{--apply-automatic-rule}] apply the automatic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski strategy to the development graph. This is what you usual want in order to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski get goals within nodes for proving.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-N}, \texttt{--normal-form}] compute all normal forms for nodes
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with incoming hiding links. (This may take long and may not be implemented
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for all logics.)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLet us extend the above library \texttt{Order.casl}. One use of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary might be to express the fact that the natural numbers form a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistrict partial order as a view, as follows:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{Natural} = ~\FREE \TYPE \(Nat ::= 0 \| suc(Nat)\)~\END
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{EXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEDEFN{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{Natural}} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\PRED \( \_\_<\_\_ : Nat \* Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\(\[ \FORALL x,y:Nat \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. 0 < suc(x) \\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \. \neg x < 0 \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \. suc(x) < suc(y) \IFF x < y
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\I\VIEW \NAMEDEFN{v1} ~:~ \NAMEREF{Strict\_Partial\_Order} \TO
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I{} \( Elem \MAPSTO Nat\)
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAgain, these specifications can be checked with \Hets. However, this
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskionly checks syntactic and static semantic well-formedness -- it is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{not} checked whether the predicate `$\_\_<\_\_$' introduced in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\NAMEREF{Natural\_Order\_2} actually is constrained to be interpreted
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiby a strict partial ordering relation. Checking this requires theorem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproving, which will be discussed below.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHowever, before coming to theorem proving, let us first inspect the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof obligations arising from a specification. This can be done with:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{hets -g Order.casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(assuming that the above two specifications and the view
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihave been added to the file
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets now displays a so-called development graph
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(which is just an overview graph showing the overall structure
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the specifications in the library), see Fig.~\ref{fig:dg0}.
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\includegraphics[scale=0.7]{dg-order-0}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{Sample development graph.\label{fig:dg0}}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNodes in a development graph correspond to \CASL specifications.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiArrows show how specifications are related by the structuring
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe black arrow denotes an ordinary import of
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskishow that the view is well-formed (then its color turns into green).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAs a more complex example, consider the following loose specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof a sorting function, taken from the \CASL User Manual
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{CASL-UM}, Chap.~6:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order\_Sorted}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\\{} [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe \CASL User Manual \cite{CASL-UM}, Chap.~6:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{BIGEXAMPLE}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\I\SPEC \NAMEREF{List\_Order}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder [\,\NAMEREF{Total\_Order} \WITH \SORT \(Elem\), \PRED \(\_\_<\_\_\)\,] =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\phantomsection
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\IEXT{\NAMEREF{List\_Selectors} [\,\SORT \(Elem\)\,]} \THEN
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\WITHIN]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{ITEMS}[\OP]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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)) \]\)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{BIGEXAMPLE}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBoth specifications are related. To see this, we first inspect
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitheir signatures. This is possible with:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\texttt{hets -g Sorting.casl}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiassuming that \texttt{Sorting.casl} contains the above specifications.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{figure}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{center}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\includegraphics[scale=0.7]{dg-order-1}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\caption{Development graph for the two sorting specifications.\label{fig:dg1}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIn the above-mentioned development graph, we have two types of nodes.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe named ones correspond to named specifications, but there
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiare also unnamed nodes corresponding to anonymous basic
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskispecifications like the declaration of the $insert$ operation in
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\NAMEREF{List\_Order} above. Basically, there is an
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiunnamed node for each structured specification that is not named.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiAgain, the black arrows denote an ordinary import of specifications
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(corresponding to the extensions and unions in the
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskispecifications), while the blue arrows denote hiding (corresponding to
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskithe local specification).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBy clicking on the nodes, one can inspect their signatures.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIn this way, we can see that both \NAMEREF{List\_Order\_Sorted} and
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\NAMEREF{List\_Order} have the same signature. Hence, it
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiis legal to add a view:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{EXAMPLE}%[\SLIDESMALL]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\I\VIEW \NAMEDEFN{v2}[\NAMEREF{Total\_Order}] ~:~ \NAMEREF{List\_Order\_Sorted}[\NAMEREF{Total\_Order}] \TO
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\NAMEREF{List\_Order}[\NAMEREF{Total\_Order}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWe have already added this view to \texttt{Sorting.casl}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThe corresponding
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproof obligation between \NAMEREF{List\_Order\_Sorted} and
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\NAMEREF{List\_Order} is displayed in Fig.~\ref{fig:dg1}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski as a red arrow.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederHere is a summary of the types of nodes and links occurring in
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskidevelopment graphs:
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{description}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Named nodes] correspond to a named specification.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Unnamed nodes] correspond to an anonymous specification.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Elliptic nodes] correspond to a specification in the current library.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Rectangular nodes] are external nodes corresponding to a specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski downloaded from another library.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Red nodes] have open proof obligations.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Yellow nodes] have an open conservativity proof obligations.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[Green nodes] have all proof obligations resolved.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Black links] correspond to reference to other specifications (definition
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski links in the sense of \cite[IV:4]{CASL/RefManual}).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Red links] correspond to open proof obligations (theorem links).
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Green links] correspond to proven theorem links.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Yellow links] correspond to proven theorem links with open
30256573a343132354b122097b0ee1215dda1364Till Mossakowski conservativity or to open hiding theorem links.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Blue links] correspond to hiding, free, or cofree definition links.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Violett links] correspond to a mixture of links becoming visible after
30256573a343132354b122097b0ee1215dda1364Till Mossakowski ``expand'' or ``Show unnamed nodes with open proofs''.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Solid links] correspond to global (definition or theorem)
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilinks in the sense of \cite[IV:4]{CASL/RefManual}.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Dashed links] correspond to local (theorem) links in the sense of
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescu \cite[IV:4]{CASL/RefManual}. These are usually created after
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder ``Global-Decomposition'' or only be visible after ``Show newly added proven
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Single line links] have homogeneous signature morphisms (staying within
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski one and the same logic).
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Double line links] have heterogeneous signature morphisms (moving
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski between logics).
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\end{description}
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiWe now explain the menus of the development graph window.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiMost of the pull-down menus of the window are uDraw(Graph)-specific
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskitheir function can be looked up in the uDraw(Graph) documentation\footnote{see
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
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}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Edit] This menu has the following submenus:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{description}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Undo] Undo the last development graph proof step (see under Proofs)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Redo] Restore the last undone development graph proof step (see
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski under Proofs)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe ``Hide/show names/nodes/edges'' menu is a toggle:
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiyou can switch on or off the display of node names, unnamed nodes or
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproven theorem links.
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiWith the ``Hide/show internal node names'' option, the nodes that
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskiare initially unnamed get derived names.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederWith the ``Hide/show unnamed nodes without open proofs'' option, it is possible
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskito reveal the unnamed nodes which do not have open proof goals.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiInitially, the complexity of the graph is reduced by hiding all these nodes;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskionly nodes corresponding to named specifications are displayed.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPaths between named nodes going through unnamed nodes
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiare displayed as edges; these paths are then expanded when showing the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiunnamed nodes.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiWhen applying the development graph calculus rules, theorem links that have
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskibeen proven are removed from the graph. With the ``Hide/Show newly added
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiproven edges'' option, it is possible to re-display these links; they are marked
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskias proven in the link info (see \emph{Pop-up menu for links}, below).
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich\item[Focus node]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis menu is particularly useful when navigating in a large development graph,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiwhich does not fit on a single screen. The list of all nodes is displayed:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe nodes are identified by the internal node number and the internal node name.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiOnce a node is selected, the view centers on it.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Select Linktypes]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis menu allows to select the type of links that are displayed in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidevelopment graph. A selection window appears, where links are grouped into
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthree categories: definition links, proven theorem links and unproven
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskitheorem links. It is possible to select/deselect all links or to invert the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskicurrent selection.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item[Consistency checker]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Checks whether the theories of the nodes of the graph are consistent
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski i.e. have a model. The model finders currently interfaced are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Isabelle-refute, darwin and E-KRHyper.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Proofs] This menu allows to apply some of the deduction rules
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski for development graphs, see Sect. IV:4.4 of the \CASL Reference
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Manual \cite{CASL/RefManual} or one of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}. While support for
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski local and global (definition or theorem) links is stable, support
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski for hiding links and checking conservativity is still experimental.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski In most cases, it is advisable to use ``Automatic'', which
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski automatically applies the rules in the correct order. As a result,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski the open theorem links (marked in red) will be reduced to local
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski proof goals, that is, they become green, and instead, some target nodes
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski may get red, indicating open local proof goals.
b740c481cef85409c373a87756fa394051cb4a37Christian Maeder Besides the deduction rules, the menu contains entries for computing
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski a colimit approximation for the development graph and for
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski computing normal forms of all nodes (needed when dealing with hiding).
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder Also, a \CASL-specific normalisation of free links has been
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Dump Development Graph] This option is available only for
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski debugging purposes; it outputs a textual representation
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski of the development graph.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Show Library Graph] This menu displays the library graph, in a separate
30256573a343132354b122097b0ee1215dda1364Till Mossakowski window, if the library graph window has been closed after \Hets has been
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Save Graph for uDrawGraph] Saves the development graph in a .udg file
30256573a343132354b122097b0ee1215dda1364Till Mossakowski which can be later read by uDrawGraph.
b740c481cef85409c373a87756fa394051cb4a37Christian Maeder\item[Save proof-script] This menu saves the proof rules that have been applied
30256573a343132354b122097b0ee1215dda1364Till Mossakowski to the current development graph in a .hpf file which can be later read by
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \Hets and thus the action performed on the graph are saved.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Pop-up menu for nodes]
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHere, the number of submenus depends on the type of the node:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{description}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[Show node info] Shows the local informations of the node: the internal
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski node name and node number, the xpath that denotes the location of the node
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski within an XML representation, information about consistency of the node,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski origin of the node and the local theory i.e. axioms declared locally.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Show theory] Shows the theory of the node (including axioms
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiimported from other nodes). Notice that axioms imported via hiding links
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiare not part of the theory; they can be made visible only by re-adding
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe hidden symbols, using the normal form of the node, by calling
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\emph{Proofs/Compute Normal Form}. For such nodes, a warning is displayed.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Translate theory] Translates the theory of a node to another logic.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiA menu with the possible translation paths will be displayed.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Taxonomy graphs] (Only available for some logics) Shows the subsort graph
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski of the signature of the node.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Show proof status] Show open and proven local proof goals.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Prove] Try to prove the local proof goals. See Section~\ref{sec:Proofs}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Prove VSE structured] Allows to send a development graph below the
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski current node to the interactive \texttt{hetsvse} prover if that binary is
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski available, see \ref{subsec:VSE}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Check conservativity] Checks conservativity of the inclusion
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski morphism from the empty theory to the theory of the node (see
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski {\bf Check conervativity} for edges).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{description}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFor the nodes which are references to specifications from an external library,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe pop-up menu options are reduced to {\bf Show node info, Show theory,
30256573a343132354b122097b0ee1215dda1364Till MossakowskiShow proof status} and {\bf Prove} and moroever, the option {\bf Show
30256573a343132354b122097b0ee1215dda1364Till Mossakowskireferenced library} is added: on selection, it displays in a new window
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe development graph of the external library from which the specification has
30256573a343132354b122097b0ee1215dda1364Till Mossakowskibeen downloaded.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Pop-up menu for links]
30256573a343132354b122097b0ee1215dda1364Till MossakowskiAgain, the number of submenus depends on the type of the link:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Show info] Shows informations about the edge: internal number and
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinternal nodes it links, the link type and origin and the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisignature morphism of the link. The latter consists
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichof two components: a logic translation and a signature morphism in the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitarget logic of the logic translation.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIn the (most frequent) case
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof an intra-logic signature morphism, the logic translation component is
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederjust the identity.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Check conservativity] (Experimental) Check whether the
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowskitheory of the target node of the link
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederis a conservative extension of the theory of the source node.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[Expand]This menu is available only for paths going through unnamed
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowskinodes which are not displayed and it expands the path to the links forming it.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBesides development graphs there are library graph windows displaying the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary hierarchy. The Edit menu has the following submenus:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Edit] This menu for library graphs has the following submenus:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Reload Library] Reloads all \HetCASL sources in order to avoid closing
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder and restarting the application after sources have changed. However, all
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski previous proof steps will be lost, therefore you have to confirm this
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski action. (A change management tool to keep proofs is in preparation.)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[Translate Library] Translates a library along a comorphism to be chosen.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski This only works for a homogeneous library hierarchy. A finer grained
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder alternative is to use ``Translate theory'' for individual nodes. The
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder original state and proof steps will be lost, therefore you have to confirm
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[Show Logic Graph] Shows the graph of logics and logic comorphisms
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski currently supported by \Hets. The Edit menu of a logic graph window has the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder following submenu:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Show detailed logic graph] Shows the important sublogics and comorphims
b740c481cef85409c373a87756fa394051cb4a37Christian Maeder between them, i.e. translation (blue links) and inclusion (black links).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{description}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\section{Reading, Writing and Formatting}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\Hets provides several options controlling the types of files
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskithat are read and written.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{description}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-i ITYPE}, \texttt{--input-type=ITYPE}] Specify \texttt{ITYPE}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich as explicit type of the input file. By default \texttt{env}, \texttt{casl},
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich or \texttt{het} extensions are tried in this order. An \texttt{env} file
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich contains a shared ATerm of a development graph, whereas \texttt{casl} or
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \texttt{het} files contain plain \HetCASL text. An \texttt{env} file will
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich always be read if it exists and is consistent (aka newer) than the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski corresponding \HetCASL file.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \texttt{exp} files contain a development graph in a new experimental omdoc
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski format. \texttt{prf} files contain additional development steps (as shared
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski ATerms) to be applied on top of an underlying development graph created from
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski a corresponding \texttt{env}, \texttt{casl}, or \texttt{het}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski file. \texttt{hpf} files are plain text files representing heterogeneous
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich proof scripts. The contents of a \texttt{hpf} file must be valid input for
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \Hets in interactive mode. (\texttt{gen\_trm} formats are currently not
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe possible input types are:
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich casl|het|owl|hs|exp|maude|elf|prf
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich |omdoc|hpf|[tree.]gen_trm[.baf]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-O DIR}, \texttt{--output-dir=DIR}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichSpecify \texttt{DIR} as destination directory for output files.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-o OTYPES}, \texttt{--output-types=OTYPES}]
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\texttt{OTYPES} is a comma separated list of output types:
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{verbatim}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski | (sig|th)[.delta]
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski | pp.(het|tex|xml)
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{verbatim}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{env} and \texttt{prf} formats are for subsequent reading,
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichavoiding the need to re-analyse downloaded libraries. \texttt{prf} files
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcan also be stored or loaded via the GUI's File menu.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{owl} option \cite{books/sp/Kohlhase06} will produce OWL files in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichManchester Syntax for each specification of a structured OWL library.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckemarkup format and data model for Open Mathematical Documents. It
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiserves as semantics-oriented representation format and ontology
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskilanguage for mathematical knowledge. Currently, \CASL specifications
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskican be output in this format; support for further logics is planned.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{xml} option will produce an XML-version of the development graph
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskifor our change management broker.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe \texttt{exp} format is the new experimental omdoc format.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{hs} format is used for Haskell modules. Executable \CASL or
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\HasCASL specifications can be translated to Haskell.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiWhen the \texttt{thy} format is selected, \Hets will try to translate
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskieach specification in the library to \Isabelle, and write one \Isabelle
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\texttt{.thy} file per specification.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichWhen the \texttt{comptable.xml} format is selected, \Hets will extract
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichthe composition and inverse table of a Tarskian relation algebra from
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichspecification(s) (selected with the \texttt{-n} or \texttt{--spec}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichoption). It is assumed that the relation algebra is
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichgenerated by basic relations, and that the specification is written
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichin the \CASL logic. A sample specification of a relation
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichalgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichavailable from \texttt{www.cofi.info/Libraries}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe output format is XML, the URL of the DTD is included in the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{sig} or \texttt{th} option will create \HetCASL signature or
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichtheory files for each development graph node. (The \texttt{.delta} extension
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichis not supported, yet.)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{pp} format is for pretty printing, either as plain text
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich(\texttt{het}), \LaTeX input (\texttt{tex}) or XML (\texttt{xml}).
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichFor example, it is possible to generate a pretty
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichprinted \LaTeX\ version of \texttt{Order.casl} by typing:
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThis will generate a file \texttt{Order.pp.tex}. It can be included
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe format \texttt{pp.xml} represents a library in XML for our change
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich management broker.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichFormats with \texttt{graph} are for future usage.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{dfg} format is used by the \SPASS theorem prover
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\cite{WeidenbachEtAl02}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichformat for first-order theorem provers.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichAppending \texttt{.c} to \texttt{dfg} or \texttt{tptp} will create files for
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichconsistency checks by SPASS or Darwin respectively.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichFor all output formats it is recommended to increase the verbosity to at least
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichlevel 2 (by using the option \texttt{-v2}) to get feedback which files are
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichactually written. (\texttt{-v2} also shows which files are read.)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-t TRANS}, \texttt{--translation=TRANS}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichchooses a translation option. \texttt{TRANS} is a colon-separated list
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichwithout blanks of one or more comorphism names (see Sect.~\ref{comorphisms}).
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-n SPECS}, \texttt{--spec=SPECS}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichchooses a list of named specifications for processing
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-R}, \texttt{--recursive}] output also imported libraries.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-I}, \texttt{--interactive}] run \Hets in interactive mode
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-x}, \texttt{--xml}] use xml-pgip packets to communicate with
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \Hets in interactive mode
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[\texttt{-S PORT}, \texttt{--listen=PORT}] communicate
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich with \Hets in interactive mode vy listining to the port \texttt{PORT}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-c HOSTNAME:PORT}, \texttt{--connect=HOSTNAME:PORT}] communicate
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich with \Hets in interactive mode via connecting to the port on host
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \texttt{HOSTNAME}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-d STRING}, \texttt{--dump=STRING}] produces implementation
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich dependent output for debugging purposes only
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{description}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\section{Miscellaneous Options}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{description}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-v[Int]}, \texttt{--verbose[=Int]}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichSet the verbosity level according to \texttt{Int}. Default is 1.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-q}, \texttt{--quiet}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichBe quiet -- no diagnostic output at all. Overrides -v.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-V}, \texttt{--version}] Print version number and exit.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-h}, \texttt{--help}, \texttt{--usage}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichPrint usage information and exit.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \texttt{Int} megabytes (needed in case of a stack overflow).
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThis must be the first option.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-l LOGIC}, \texttt{--logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichdeclaration. The default is \CASL.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-m FILE}, \texttt{--modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{description}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\section{Proofs with \Hets}\label{sec:Proofs}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe proof calculus for development graphs (Sect.~\ref{sec:DevGraph}) reduces
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichglobal theorem links to local proof goals. Local proof goals (indicated by red
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskinodes in the development graph) can be eventually discharged using a theorem
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiprover, i.e. by using the ``Prove'' menu of a red node.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe graphical user interface (GUI) for calling a prover is shown in
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederFig. \ref{fig:proof_window} --- we call it ``Proof Management GUI''.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski(This GUI looks slightly different, if hets was not build with GTK support as
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskifor example under solaris.)
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiThe top list on the left shows all goal names prefixed with the proof
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederstatus in square brackets. A proved goal is indicated by a `+', a `-'
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiindicates a disproved goal, a space denotes an open goal, and a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski`$\times$' denotes an inconsistent specification (aka a fallen `+';
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedersee below for details).
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\includegraphics[width=\textwidth]{proofmanagement1}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\caption{Hets Goal and Prover Interface\label{fig:proof_window}}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiIf you open this GUI when processing the goals of one node for the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskifirst time, it will show all goals as open. Within this list you can
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiselect those goals that should be inspected or proved. The GUI elements are the following:
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{itemize}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item The top-right button `Disprove' is supposed to prove the negation of a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski selected goal, but this functionality is not implemented yet.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item The button `Display' shows the selected goals in the ASCII syntax of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski this theory's logic in a separate window.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item By pressing the `Proof details' button a window is opened where for each
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski proved goal the used axioms, its proof script, and its proof are shown ---
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski the level of detail depends on the used theorem prover.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item With the `Prove' button the actual prover is launched. This is described
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski in more detail in the paragraphs below.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item The list `Pick Theorem Prover:' lets you choose one of the connected
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski provers (among them \Isabelle, MathServe Broker, \SPASS, Vampire, and
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski zChaff, described below). By pressing `Prove' the selected prover is
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski launched and the theory along with the selected goals is translated via the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski shortest possible path of comorphisms into the provers logic.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item The pop-up choice box below `Selected comorphism path:' lets you pick a
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (composed) comorphism to be used for the chosen prover.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item Since the amount and kind of sentences sent to an ATP system is a major
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski factor for the performance of the ATP system, it is possible to select in
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski the bottom lists the axioms and proven theorems that will comprise the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder theory of the next proof attempt. Based on this selection the sublogic may
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski vary and also the available provers and comorphisms to provers. Former
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski theorems that are imported from other specifications are marked with the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski prefix `(Th)'. Since former theorems do not add additional logical content,
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski they may be safely removed from the theory.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item If you press the bottom-right `Close' button the window is closed and
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski the status of the goals' list is integrated into the development graph. If
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski all goals have been proved, the selected node turns from red into green.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item All other buttons control selecting list entries
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\subsection{Consistency Checker}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\label{sec:CC}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiSince proofs are void if specifications are inconsistent, the consistency
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskishould be checked (if possible for the given logic) by the ``Consistency
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskichecker'' shown in Fig. \ref{fig:cons_window}. This GUI is invoked from
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskithe `Edit' menu as it operates on all nodes. (Without GTK support this GUI is
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskimissing, though.)
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe list on the left shows all node names prefixed with a consistency status
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiin square brackets that is initially empty. A consistent node is indicated by
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskia `+', a `-' indicates an inconsistent node, a `t' denotes a timeout of the last
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskichecking attempt.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{figure}
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke\includegraphics[width=\textwidth]{ConsistencyChecker}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\caption{Hets Consistency Checker Interface\label{fig:cons_window}}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederFor some selection of nodes (of a common logic) a model finder should be
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederselectable from the `Pick Model finder:' list. Currently only for ``darwin''
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckesome \CASL models can be re-constructed. When pressing `Check', possibly after
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder`Select comorphism path:', all selected nodes will be checked, spending at
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckemost the number of seconds given under `Timeout:' on each node. Pressing
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke`Stop' allows to terminate this process if too many nodes have been chosen.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederEither by `View results' or automatically the `Results of consistency check'
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder(Fig. \ref{fig:cons_res}) will pop up and allow you to inspect the models for
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Lueckenodes, if they could be constructed.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{figure}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\includegraphics[width=\textwidth]{ConsCheckResults}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\caption{Consistency Checker Results\label{fig:cons_res}}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\subsection[Automated Theorem Proving Systems]
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke{Automated Theorem Proving Systems\\(Logic SoftFOL)}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\label{sec:ATP}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{figure}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\includegraphics[width=\textwidth]{spassGUI1}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeAll ATPs integrated into \Hets share the same GUI, with only a slight
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckemodification for the MathServe Broker: the input field for extra options is
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeinactive. Figure~\ref{fig:SPASS_GUI} shows the instantiation for \SPASS, where
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckein the top right part of the window the batch mode can be controlled. The
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeleft side shows the list of goals (with status indicators). If goals are
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecketimed out (indicated by `t') is may help to activate the check box `Include
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckepreceeding proven theorems in next proof attempt' and pressing `Prove all'
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeOn the bottom right the result of the last proof
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeattempt is displayed. The `Status:' indicates `Open', `Proved', `Disproved',
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke`Open (Time is up!)', or `Proved (Theory inconsistent!)'. The list of `Used
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeAxioms:' is filled by \SPASS. The button `Show Details' shows the whole output
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeof the ATP system. The `Save' buttons allow you to save the input and
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeconfiguration of each proof for documentation. By `Close' the results for all
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckegoals are transferred back to the Proof Management GUI.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeThe MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiZimmer provides a unified interface to a range of different ATP
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskisystems; the most important systems are listed in
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiTable~\ref{tab:MathServe}, along with their capabilities. These
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskicapabilities are derived from the \emph{Specialist Problem Classes}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski(SPCs) defined upon the basis of logical, language and syntactical
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiproperties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeOnly two of the Web services provided by the MathServe system are used
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeby \Hets currently: Vampire and the brokering system. The ATP systems
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeare offered as Web Services using standardized protocols and formats
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckesuch as SOAP, HTTP and XML. Currently, the ATP system Vampire may be
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeaccessed from \Hets via MathServe; the other systems are only reached
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeafter brokering.
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\begin{table}[t]
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \begin{threeparttable}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \begin{tabular}{|l|c|p{7cm}|}\firsthline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke ATP System & Version & Suitable Problem Classes\tnote{a}\\
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \hhline{|=|=|=|}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke DCTP & 10.21p & effectively propositional \\\hline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke EP & 0.91 & effectively propositional; real first-order, no
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke equality; real first-order, equality\\\hline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke Otter & 3.3 & real first-order, no equality\\\hline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \SPASS & 2.2 & effectively propositional; real first-order, no
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke equality; real first-order, equality\\\hline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke Vampire & 8.0 & effectively propositional; pure equality, equality
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke clauses contain non-unit equality clauses; real first-order, no
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke equality, non-Horn\\\hline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke Waldmeister & 704 & pure equality, equality clauses are unit
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke equality clauses\\\lasthline
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \end{tabular}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke %\renewcommand{\thempfootnote}{\arabic{mpfootnote}}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke %\footnotetext%[\value{footnote}\stepcounter{footnote}]
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \begin{tablenotes}\footnotesize
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski {The list of problem classes for each ATP system is not
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke exhaustive, but only the most appropriate problem classes are
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke named according to benchmark tests made with MathServe by
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke J\"urgen Zimmer.}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \end{tablenotes}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \end{threeparttable}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \caption{ATP systems provided as Web services by MathServe}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\vspace*{-4mm}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke \label{tab:MathServe}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke\subsubsection*{\SPASS}
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik LueckeThe ATP system \SPASS \cite{WeidenbachEtAl02} is a resolution-based
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Lueckeprover for first-order logic with equality. Furthermore, it provides a soft
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecketyping mechanism with subsorting that treats sorts as unary
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskipredicates. The ATP \SPASS should be installed locally and available
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskithrough your \verb,$PATH, environment variable.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\subsubsection*{Vampire}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski% http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiThe ATP system Vampire is the winner of the last 5 CADE ATP System
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiCompetitions (CASC) (2002--2006) in the devisions \verb,FOF, and
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\verb,CNF,. It is a resolution based ATP system supporting the calculi
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskiof ordered binary resolution and superposition for handling equality.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\url{http://www.cs.miami.edu/~tptp/CASC/J3/SystemDescriptions.html#Vampire---8.0}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskifor detailed information. The connection to Vampire is achieved by
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskiusing an Web service of the MathServe system.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\subsubsection*{MathServe Broker}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski% The classes ``effectively propositional'' and ``real first-order''
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski% apply to first-order problems that are distinguished by the finiteness
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski% of the Herbrand universe; an effectively propositional problem has
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski% only constants (generated by finitely many terms) whereas a real
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% first-order problem contains true functions with an infinite Herbrand
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe brokering service chooses the most appropriate ATP system
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiupon a classification based on the SPCs, and on a training with the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilibrary Thousands of Problems for Theorem Provers (TPTP)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\cite{ZimmerAutexier06}. The TPTP format
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihas been introduced by Sutcliffe and Suttner for the annual
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicompetition CASC \cite{Sutcliffe:2006:CASC} and provides a unified
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisyntax for untyped FOL with equality, but without any symbol
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{Isabelle}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Isabelle \cite{NipPauWen02} is an interactive theorem prover, which is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimore powerful than ATP systems, but also requires more user interaction.
30256573a343132354b122097b0ee1215dda1364Till Mossakowskihas a very small core guaranteeing correctness, and its provers,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilike the simplifier or the tableaux prover, are built on top of this
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicore. Furthermore, there is over fifteen years of experience with it,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiand several mathematical textbooks have been partially
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \index{formal!verification}%
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\Isabelle is a tactic based theorem prover implemented in standard ML.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe main \Isabelle logic (called Pure) is some weak intuitionistic type
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitheory with polymorphism. The logic Pure is used to represent a
30256573a343132354b122097b0ee1215dda1364Till Mossakowskivariety of logics within \Isabelle; one of them being \HOL (higher-order
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilogic). For example, logical implication in Pure (written
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{==>}, also called meta-implication), is different from logical
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiimplication in \HOL (written \texttt{-->}, also called object
30256573a343132354b122097b0ee1215dda1364Till MossakowskiIt is essential to be aware of the fact that the \Isabelle/\HOL logic
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis different from the logics that are encoded into it via comorphisms.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiTherefore, the formulas appearing in subgoals of proofs with \Isabelle
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederwill not conform to the syntax of the original input logic. They may
30256573a343132354b122097b0ee1215dda1364Till Mossakowskieven use features of \Isabelle/\HOL such as higher-order functions
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthat are not present in an input logic like \CASL.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\Isabelle is started with ProofGeneral
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{DBLP:conf/tacas/Aspinall00,url:ProofGeneral} in a separate Emacs
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{url:Emacs,url:XEmacs}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \Isabelle theory file conforms to the Isabelle/Isar syntax
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{NipPauWen02}. It starts with the theory (encoded along the selected
30256573a343132354b122097b0ee1215dda1364Till Mossakowski comorphism), followed by a list of theorems. Initially, all the
30256573a343132354b122097b0ee1215dda1364Till Mossakowski theorems have trivial proofs, using the `oops` command. However, if
30256573a343132354b122097b0ee1215dda1364Till Mossakowski you have saved earlier proof attempts, \Hets will patch these into
30256573a343132354b122097b0ee1215dda1364Till Mossakowski the generated \Isabelle theory file, ensuring that your previous work
30256573a343132354b122097b0ee1215dda1364Till Mossakowski is not lost. (But note that this patching can only be successful
30256573a343132354b122097b0ee1215dda1364Till Mossakowski if you do not rename specifications, or change their structure.) You
30256573a343132354b122097b0ee1215dda1364Till Mossakowski now can replace the 'oops' commands with real \Isabelle proofs, and
30256573a343132354b122097b0ee1215dda1364Till Mossakowski use Proof General to step through the proofs. You finish your session
30256573a343132354b122097b0ee1215dda1364Till Mossakowski by saving your file (using the Emacs file menu, or the Ctrl-x Ctrl-s
30256573a343132354b122097b0ee1215dda1364Till Mossakowski key sequence), and by exiting Emacs (Ctrl-x Ctrl-c).
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{VSE}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\label{subsec:VSE}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski The specification environment Verification Support Environment
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(VSE) \cite{VSE00}, developed at
30256573a343132354b122097b0ee1215dda1364Till MossakowskiDFKI Saarbr\"ucken, provides an industrial-strength methodology
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor specification and verification of imperative programs.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiVSE provides an interactive prover, which supports a Gentzen style
30256573a343132354b122097b0ee1215dda1364Till Mossakowskinatural deduction calculus for dynamic logic.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThis logic is an extension of first-order logic with two additional
30256573a343132354b122097b0ee1215dda1364Till Mossakowskikinds of formulas
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithat allow for reasoning about programs. One of them is the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskibox formula $[\alpha]\varphi$, where $\alpha$ is a program written in an imperative
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilanguage, and $\varphi$ is a dynamic logic formula.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe meaning of $[\alpha]\varphi$ can be roughly put as
30256573a343132354b122097b0ee1215dda1364Till Mossakowski``After every terminating execution of $\alpha$, $\varphi$ holds.''.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe other new kind
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof formulas is the diamond formula $\langle\alpha\rangle\varphi$, which is the dual counter part
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof a box formula. The meaning of $\langle\alpha\rangle\varphi$
30256573a343132354b122097b0ee1215dda1364Till Mossakowskican be described as ``After some terminating execution of $\alpha$,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski$\varphi$ holds''.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiA VSE specification or something that can be translated to VSE (currently only
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\CASL) can be sent to the VSE prover via the node menu of development graph
30256573a343132354b122097b0ee1215dda1364Till Mossakowskinodes in two different ways. You can either select VSE from the theorem prover
30256573a343132354b122097b0ee1215dda1364Till Mossakowskichoice box shown after ``Prove'' or you can select ``Prove VSE Structured''.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe first choice will call VSE with a single flattened theory whereas a
30256573a343132354b122097b0ee1215dda1364Till Mossakowskistructured call will translate all nodes with ingoing links to the current one
30256573a343132354b122097b0ee1215dda1364Till MossakowskiVSE pops up with a ``project'' window. In this window you can choose ``Work
30256573a343132354b122097b0ee1215dda1364Till Mossakowskion'' and ``specification''. Besides the builtin specification ``boolean''
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithere is at least one specification from your development graph that you
30256573a343132354b122097b0ee1215dda1364Till Mossakowskican select for proving. For a structured choice you'll have specifications
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor all underlying nodes that you should work on in a bottom up fashion.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe state created by VSE will be stored in a \texttt{.tar} file (within the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicurrent directory) that preserves proofs for replay later on as long as you
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskidon't change library or node names.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{zChaff}
30256573a343132354b122097b0ee1215dda1364Till MossakowskizChaff is a solver for satisfiabily problems of boolean formulas
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(\normalTEXTSC{S}{AT})
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiin CNF. It is connected as a prover for propositional logic to \Hets. The prover
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\SPASS is used to transform arbitrary boolean formulas to CNF. zChaff
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiimplements the \normalTEXTSC{C}{HAFF}\xspace algorithm. We are
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiusing the property, that a conjecture under the assumption of a set of axioms is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitrue, if the variables of axioms together with the negation of the conjecture
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskihave no satisfying assignment, to prove theorems with zChaff. That is why you see
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe result \normalTEXTSC{U}{NSAT}\xspace in the proof details, if a theorem has been proved
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskito be true. zChaff uses the same ATP GUI as the provers for SoftFOL (ref. to section
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\ref{sec:ATP}). zChaff does not accept any options apart from the time-limit. The
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicurrent integration of zChaff into \Hets has been tested with zChaff 2004.11.15.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{Reduce}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis is a connection to the computer algebra system from
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\url{http://www.reduce-algebra.com/}. Installation is possible as follows:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisvn co https://reduce-algebra.svn.sourceforge.net/svnroot/reduce-algebra
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski./configure --with-csl --with-psl
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe binary \texttt{redcsl} will be search in the \texttt{PATH} or is taken
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskifrom the \texttt{HETS\_REDUCE} environment variable.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\subsection{Pellet}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiPellet is a popular open-source \DL-reasoner for \SROIQ, which is the logic
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowskiunderlying OWL 2.0, written in Java. A Java Runtime Environment (in version $> 1.5$)
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowskiis needed to run Pellet. For the integration into \Hets the environment variable
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski\verb+PELLET_PATH+ has to be set to the root-directory of the Pellet installation.
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiPellet uses the same ATP GUI as the provers for SoftFOL (ref. to section
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski\ref{sec:ATP}).
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski\subsection{Fact++}
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiFact++ is a \DL-reasoner for \SROIQ, which is the logic underlying OWL 2.0, written in
12a1614014912501fbfc30a74242d6f3a5c97e80Till MossakowskiC++. Fact++ is integrated into \Hets via the OWL-API, which is written in Java.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiA Java Runtime Environment (in version $>= 1.5$) has to be installed. To use Fact++,
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe environment variable \verb+HETS_OWL_TOOLS+ has to be set to the directory
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicontaining the files
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{verbatim}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskion a 32bits-Linux-system or
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{verbatim}
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till Mossakowskiin a 64bits-Linux-system. Fact++ does not support options.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiFact++ uses the same ATP GUI as the provers for SoftFOL (ref. to section
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\ref{sec:ATP}).
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\subsection{E-KRHyper}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiE-KRHyper\footnote{\url{http://www.uni-koblenz.de/~bpelzer/ekrhyper/}}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiis an extension of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiKRHyper\footnote{\url{http://www.uni-koblenz.de/~wernhard/krhyper/}} by
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskihandling of equality. E-KRHyper is an automatic first order theorem
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till Mossakowskiprover and model finder based on the Hyper Tableaux Calculus\cite{Baumgartner:1996}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiE-KRHyper is optimized for being integrated into other systems. In the current
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiimplementation we use a default tactics script, that can be influenced by the user.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe options of E-KRHyper are written in a Prolog-like syntax as in
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski#(set_parameter(timeout_termination_method,0)).
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{verbatim}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskithe ``.'' at the end of each option is mandatory. To get an overview of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiE-KRHyper's options, run the command
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiin a terminal. Then enter the command
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederat the prompt of E-KRHyper, to display its help information, which is basically
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskia long list of all available parameters. You can exit E-KRHyper by the command
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{verbatim}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiE-KRHyper uses the same ATP GUI as the other provers for SoftFOL (ref. to section
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\ref{sec:ATP}).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\subsection{Darwin}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiDarwin is an automatic first order prover and model finder implementing the Model
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiCalculus\cite{Baumgartner:2003}. The integration of Darwin as a consistency checker
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskisupports the display of models (if they can be constructed) in \CASL-syntax.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederEprover is needed to be in the system-path, if Darwin is used with \Hets, since
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiDarwin uses Eprover for clausification of first-order formulae.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiDarwin supports a wide range of options, to get an overview of them run the command
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{verbatim}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiin a terminal.
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiDarwin uses the same ATP GUI as the other provers for SoftFOL (ref. to section
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\ref{sec:ATP}).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{QuickCheck}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{minisat}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{Truth tables}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{CspCASLProver}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Limits of Hets}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\Hets is still intensively under development. In particular, the
version, where e.g.\ error handling is ignored. For technical reasons
the static analysis of basic specifications) and/or translates (along
of the \Hets home page at \url{http://www.dfki.de/sks/hets}.
%\input{hets.tex}