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