UserGuideCommonLogic.tex revision c1d5a80013fc6210bcf4e140c0e668a14d281d0a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\setlength{\textwidth}{16cm}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\setlength{\topmargin}{-1cm}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\setlength{\evensidemargin}{0cm}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\setlength{\oddsidemargin}{0cm}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\setlength{\textheight}{22.5cm}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage[utf8]{inputenc}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage[T1]{fontenc}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{charter} % very clean and readable font
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{courier}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{unicode-chars}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage[show]{ed} % set to hide for producing a released version
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{alltt}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{color}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{url}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{threeparttable,hhline}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{tabularx}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{paralist}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{listings}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\lstset{basicstyle=\ttfamily,columns=fixed}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage[pdfborder=0 0 0,bookmarks,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipdfauthor={Till Mossakowski, Christian Maeder, Mihai Codescu, Eugen Kuksa, Christoph Lange},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipdftitle={Hets for Common Logic Users}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{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]{}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\IEXT}[1] {\\#1\I}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\IEND} {\I\END}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{EXAMPLEFORMAT} {}{}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Added by MB to have some extra vertical space after the ``main'' examples
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% following the points (and some others in the text):
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{DETAILSFORMAT} {}{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{minipage}{0.9\textwidth}\it}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski {\end{minipage}\par\medskip}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SLIDESMALL} {}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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}}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich%\newcommand {\CoFI}{CoFI\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%% Klaus macros
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SROIQ}{$\mathcal{SROIQ}$(\textbf{D})\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\DL}{DL\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
12a1614014912501fbfc30a74242d6f3a5c97e80Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski\begin{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\title{{\bf \protect{\LARGEHets} for Common Logic Users}\\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski-- Version 0.99 --}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\author{Till Mossakowski, Christian Maeder,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski Mihai Codescu, Eugen Kuksa, Christoph Lange\\[1em]
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiDFKI GmbH, Bremen, Germany.\\[1em]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiComments to: \href{mailto:hets-users@informatik.uni-bremen.de}{hets-users@informatik.uni-bremen.de} \\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(the latter needs subscription to the mailing list)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\setcounter{tocdepth}{1}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\tableofcontents
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\section{Introduction}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiCommon Logic (CL) is an ISO standard published as ``ISO/IEC 24707:2007
30256573a343132354b122097b0ee1215dda1364Till Mossakowski--- Information technology — Common Logic (CL): a framework for a family
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof logic-based languages'' \cite{CommonLogic:oldfashioned}. CL is based on untyped first-order
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilogic, but extends first-order logic in two ways: \begin{inparaenum}[(1)]\item any term can be
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiused as function or predicate, and \item sequence markers allow
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor talking about sequences of individuals directly\end{inparaenum}.\footnote
30256573a343132354b122097b0ee1215dda1364Till Mossakowski{Strictly speaking, only the second feature goes beyond first-order
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe Heterogeneous Tool Set (\Hets) is an open source software providing
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiseveral kinds of tool support for Common Logic:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{itemize}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item a parser for the Common Logic Interchange Format (CLIF) --- CLIF
30256573a343132354b122097b0ee1215dda1364Till Mossakowski is a Lisp-like syntax for CL;
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item a connection of CL to well-known first-order theorem provers
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilike SPASS, darwin and Vampire, such that logical consequences
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof CL theories can be proved;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item a connection of CL to the higher-order provers Isabelle/HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand Leo-II in order to perform induction proofs in theories
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiinvolving sequence markers;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item a connection to first-order model finders like darwin that
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiallow one to find models for CL theories;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item support for proving interpretations between CL theories to be correct;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item a translation that eliminates the use of CL modules\footnote{Actually, we are using a revised semantics for modules, as proposed
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirecently in~\cite{NH:CommonLogicHoratio}.}. Since the semantics of CL modules
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis special to CL, this elimination of modules is necessary before
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisending CL theories to a standard first-order prover;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item a translation of the Web Ontology Language OWL to CL;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item a translation of propositional logic to CL.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThis guide will introduce you to these functionalities of \Hets.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiFor the full functionalities of \Hets, see the \Hets user guide
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\cite{HetsUserGuide}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{The Heterogeneous Tool Set and Its Input Languages}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThe central idea of the Heterogeneous Tool Set (\protect\Hets) is to
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiprovide a general framework for formal methods integration and proof
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskimanagement. One can think of \Hets acting like a motherboard where
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidifferent expansion cards can be plugged in, the expansion cards here
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskibeing individual logics (with their analysis and proof tools) as well
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskias logic translations. The \Hets motherboard already has plugged in
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskia number of expansion cards (e.g., the theorem provers Isabelle, SPASS
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiand more, as well as model finders). Hence, a variety of tools is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiavailable, without the need to hard-wire each tool to the logic at
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \includegraphics[width=0.45\textwidth]{hets-motherboard}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\caption{The \Hets motherboard and some expansion cards}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets consists of logic-specific tools for the parsing and static
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskianalysis of the different involved logics, as well as a
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowskilogic-independent parsing and static analysis tool for structured and
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maederarchitectural specifications and libraries. The latter of course needs
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskito call the logic-specific tools whenever a basic specification is
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets is based on the theory of institutions \cite{GoguenBurstall92},
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiwhich formalise the notion of a logic. The theory behind \Hets is laid
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiout in \cite{Habil}. A short overview of \Hets is given in
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{MossakowskiEA06,MossakowskiEtAl07b}.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\Hets supports a number of input languages directly, such as Common
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiLogic and OWL2 and \HetCASL. They will be described in the next
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\subsection{Common Logic and the Common Logic Interchange Format (CLIF)}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCLIF is specified in Annex A of the Common Logic standard
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{CommonLogic:oldfashioned}. \Hets can directly read in files in
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCLIF syntax, and also recursively reads in any imported files (cf.\ Sect.~\ref{relationsInCL} for the syntax).
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCommon Logic itself does not support the specification of logical
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiconsequences, nor relative theory interpretations, nor other
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskifeatures that speak about structuring and comparing logical
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitheories. Michael Gr\"uninger has suggested certain special annotations comments for
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithis purpose, which are supported by \Hets, see
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSect.~\ref{relationsInCL}. Alternatively, CLIF syntax can be used
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskifor specifications within \HetCASL files, or CLIF files can be referred to within \HetCASL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskifiles. \HetCASL is a structuring language supporting relative theory
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiinterpretations and other things, see Sect.~\ref{HetCASL} below.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\subsection{OWL2}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiOWL2 is a W3C standard \cite{w3c:owl2-overview}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\Hets can directly read in OWL2 files in all syntaxes (called ``serialisations'') that the OWL API supports \cite{OWLAPI:URL}, including
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe native OWL XML syntax \cite{w3c:owl2-xml}, the human-readable
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiManchester syntax \cite{w3c:owl2-manchester}, as well as RDF \cite{w3c:owl2-RDF-mapping}. The RDF data model has multiple possible syntaxes itself, including RDF/XML \cite{w3c04:rdf-xml} and the text-oriented Turtle syntax \cite{w3c:turtle}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSince OWL2 does not support relative theory interpretations and other
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskistructuring features, such things can only be expressed in \HetCASL
7a8592051724fa46499bde120f44cdc8db270876Till Mossakowskifiles. For this purpose, OWL2 Manchester syntax can be used within
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\HetCASL files, or OWL2 files can be referred to within \HetCASL files.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\subsection{HetCASL}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\label{HetCASL}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor heterogeneous specification, \Hets offers the Heterogeneous
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilanguage \HetCASL. \HetCASL is not so much a logic, but a meta
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilanguage that can express relations of theories written in different
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilogics, like logical consequences, relative interpretations of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitheories, conservative extensions, translations of theories
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskialong logic translations, etc.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \HetCASL generalises the structuring
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\CASL (Common Algebraic Specification Language \cite{CASL-UM,CASL/RefManual}) to arbitrary logics
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(if they are formalised as institutions and plugged into
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe \Hets motherboard), as well as to heterogeneous
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicombinations of specifications written in different logics.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFig.~\ref{fig:lang} for a simple subset of the
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\HetCASL syntax, where \emph{basic specifications} are unstructured
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskispecifications or modules written in a specific logic. The graph of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicurrently supported logics and logic translations (the latter are also
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicalled comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidegree of support by \Hets in Fig.~\ref{fig:Languages}.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% We give an ad hoc listing language definition of EBNF here. This should probably go into lstlang0.sty.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{lstlisting}[float,label={fig:lang},caption={Syntax of a simple subset of the heterogeneous specification language. \texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic specific syntax, while \texttt{ID} stands for some form of identifiers.},basicstyle=\ttfamily\small,morecomment={[l]{\%\%\ }},morekeywords={then,with,logic,spec,end,view,to},escapeinside={<>}]
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiSPEC ::= BASIC-SPEC %% logic-specific syntax, e.g. CLIF or Manchester syntax
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski | SPEC then SPEC %% extension of a spec with new symbols and axioms
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | SPEC then %implies SPEC %% annotation: extension is logically implied
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich | SPEC with SYMBOL-MAP %% renaming of SPEC along SYMBOL-MAP
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | SPEC with logic ID %% translation of SPEC to a different logic
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiDEFINITION ::= logic ID %% select a new logic for subsequent items
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | spec ID = SPEC end %% give the name ID to SPEC
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | view ID : SPEC to SPEC = SYMBOL-MAP end
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski %% interpretation of theories
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | view ID : SPEC to SPEC = logic ID end
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski %% dto., but across different logics
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLIBRARY = DEFINITION*
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{lstlisting}
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiWith \emph{heterogeneous structured specifications}, it is possible to
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskicombine and rename specifications, hide parts thereof, and also
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiprescribe the structure of implementations. \emph{Specification
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski libraries} are collections of named structured and architectural
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskispecifications. \emph{Refinements} express the fact the a specification
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiis becoming more specific. All this is supported by \HetCASL.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiFor details, see \cite{Mossakowski04,Habil,CASL/RefManual}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\section{Logics supported by Hets}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\Hets supports a variety of different logics. The following are most important for use with Common Logic:
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\begin{figure}
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich \begin{center}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \includegraphics[width=.67\textwidth]{LogicGraph-CL}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\caption{Graph of logics related to Common Logic that are currently supported by \Hets. The more an
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichellipse is filled with green, the more stable is the implementation of the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichlogic. Blue indicates a prover-supported logic.}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\label{fig:LogicGraph}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{figure}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{tabular}{|l|c|c|c|}\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\CASL & x & x & -- \\\hline
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill MossakowskiCommon Logic & x (CLIF) & x & -- \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiOWL2 & x & x & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiPropositional & x & x & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSoftFOL & x & -- & x \\\hline
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\caption{Current degree of \Hets support for some of the languages.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiLanguages without prover can still ``borrow'' provers
30256573a343132354b122097b0ee1215dda1364Till Mossakowskivia logic translations.\label{fig:Languages}}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{description}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[Common Logic] is an ISO standard published as ``ISO/IEC 24707:2007 - Information technology — Common Logic (CL): a framework for a family of logic-based languages'' \cite{CommonLogic:oldfashioned}. It is based on first-order logic, but extends first-order
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilogic in several ways. The Common Logic
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Interchange Format (CLIF) provides a Lisp-like syntax for Common
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Logic. \Hets currently only supports parsing CLIF. If you need
30256573a343132354b122097b0ee1215dda1364Till Mossakowski other dialects, send us a message and we will add them.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[OWL2] is the Web Ontology Language recommended by the
30256573a343132354b122097b0ee1215dda1364Till Mossakowski World Wide Web Consortium (W3C, \url{http://www.w3c.org}); see \cite{w3c:owl2-overview}. It is
30256573a343132354b122097b0ee1215dda1364Till Mossakowski used for knowledge representation on the Semantic Web
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \cite{berners:2001:SWeb}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiHets calls an external OWL2 parser
30256573a343132354b122097b0ee1215dda1364Till Mossakowski written in Java to obtain the abstract syntax for an OWL file and its
30256573a343132354b122097b0ee1215dda1364Till Mossakowski imports. The Java parser also does a first analysis classifying
30256573a343132354b122097b0ee1215dda1364Till Mossakowski the OWL ontology into the sublanguages OWL Full (all of OWL, under the RDF semantics, undecidable \cite{w3c:owl2-rdf-based-semantics}), OWL DL (all of OWL, under the direct semantics \cite{w3c:owl2-direct-semantics}), and the so-called OWL Profiles (i.e.\ proper sublanguages) OWL EL, OWL QL, and OWL RL \cite{w3c:owl2-profiles}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski Hets supports all except OWL Full.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski structuring of the OWL imports is displayed as a Development Graph.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[Propositional] is classical propositional logic, with
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe zChaff SAT solver \cite{Herbstritt03} connected to it.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[SoftFOL] \cite{LuettichEA06a} offers several automated theorem
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski proving (ATP) systems for first-order logic with equality: \begin{inparaenum}[(1)]\item \SPASS
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \cite{WeidenbachEtAl02}, see \url{http://www.spass-prover.org};
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item Vampire \cite{RiazanovV02} see \url{http://www.vprover.org};
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item Eprover \cite{Schulz:AICOM-2002}, see \url{http://www.eprover.org};
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item E-KRHyper \cite{DBLP:conf/cade/PelzerW07}, see \url{http://www.uni-koblenz.de/~bpelzer/ekrhyper}, and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski MathServe Broker\footnote{which chooses an appropriate ATP upon a
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski classification of the FOL problem} \cite{ZimmerAutexier06}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{inparaenum}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski These together comprise some of the most advanced theorem provers
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski for first-order logic. SoftFOL is essentially the first-order
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski interchange language TPTP \cite{DBLP:conf/lpar/Sutcliffe10},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[CASL] extends many sorted first-order logic with partial
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski functions and subsorting. It also provides induction sentences,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski expressing the (free) generation of datatypes.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiFor Common Logic, \CASL can be seen as kind of transitional hub, linking
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiCommon Logic to other logics, most importantly SoftFOL.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[\Isabelle] \cite{NipPauWen02} is the logic of the interactive
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski theorem prover Isabelle for higher-order logic.
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski\item[THF] is an interchange language for higher-order logic
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski \cite{DBLP:conf/cade/BenzmullerRS08}, similar to what TPTP
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski is for first-order logic. \Hets connects THF to the automated
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski higher-order prover Leo-II.
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski\item[HasCASL] is a higher order extension of \CASL allowing
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski polymorphic datatypes and functions. It is closely related to the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski programming language Haskell and allows program constructs being
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski embedded in the specification. For Common Logic, \HasCASL
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski is mainly interesting as a transitional hub for paths
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski to the provers Isabelle and Leo-II.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[RelScheme] is a logic for relational databases \cite{DBLP:journals/ao/SchorlemmerK08}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiVarious logics are supported with proof tools. Proof support for the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiother logics can be obtained by using logic translations to a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiprover-supported logic. For Common Logic, the paths to SoftFOL
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiare particularly interesting, because this offers an interface
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskito standard first-order provers. Moreover, the paths to THF
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichand Isabelle offer interfaces to higher-order provers, which
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiis essential if you want to prove inductive theorems about
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAn introduction to \CASL can be found in the \CASL User Manual
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\cite{CASL-UM}; the detailed language reference is given in
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiexplain both the \CASL logic and language of basic specifications as
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiwell as the logic-independent constructs for structured and
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiarchitectural specifications. The corresponding document explaining the
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\HetCASL language constructs for \emph{heterogeneous} structured specifications
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiis the \HetCASL language summary \cite{Mossakowski04}; a formal
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskisemantics as well as a user manual with more examples are in preparation.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiSome of \HetCASL's heterogeneous constructs will be illustrated
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiin Sect.~\ref{sec:HetSpec} below.\\
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiFor further information on logics supported by \Hets, see the \Hets user guide
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\cite{HetsUserGuide}.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\section{Logic translations supported by Hets}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\label{comorphisms}
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiLogic translations (formalised as institution comorphisms
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\cite{GoguenRosu02}) translate from a given source logic to a given
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskitarget logic. More precisely, one and the same logic translation
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskimay have several source and target \emph{sub}logics: for
c5e63ec138b908ac9d15e6843120033bf36a1862Till Mossakowskieach source sublogic, the corresponding sublogic of the target
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskilogic is indicated.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiIn more detail, the following list of logic translations involving Common Logic
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiis currently supported by \Hets:\\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\noindent\begin{tabularx}{\textwidth}{|l|X|}\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCommonLogic2CASL & Coding Common Logic to \CASL. Module elimination
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski is applied before translating to \CASL. \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCommonLogic2CASLCompact & Coding compact Common Logic to \CASL.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski Compact Common Logic is a sublogic of Common Logic
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski where no sequence markers occur. Module elimination
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski is applied before translating to \CASL. We recommend
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski using this comorphism whenever possible because it
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski results in simpler specifications.\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCommonLogicModuleElimination & Eliminating modules from a Common Logic theory
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski resulting in an equivalent specification without
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski modules. \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiOWL22CommonLogic & Inclusion of OWL2 description logic \\\hline
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiProp2CommonLogic & Inclusion of propositional logic \\\hline
30256573a343132354b122097b0ee1215dda1364Till MossakowskiSoftFOL2CommonLogic & Inclusion of first order logic \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCASL2SoftFOL & Coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskimapping types to soft types \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCASL2SoftFOLInduction & Same as CASL2SoftFOL but with instances of induction
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiaxioms for all proof goals \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCASL2SoftFOLInduction2 & Similar to CASL2SoftFOLInduction but replaces goals with induction premises \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCASL2Propositional & Translation of propositional FOL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{tabularx}\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThose comorphisms can be chained, e.g., for theorem proving, you can translate
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichCommon Logic to SoftFOL with \texttt{CommonLogic2CASLCompact;CASL2SoftFOLInduction}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisince there is no prover for Common Logic or \CASL.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor further information on logic translations supported by \Hets, see the \Hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiuser guide \cite{HetsUserGuide}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Getting started}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe latest \Hets version can be obtained from the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets tools home page
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Since \Hets is being
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets is currently available (on Intel architectures only) for Linux
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThere are several possibilities to install \Hets.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{enumerate}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe best support is currently given via Ubuntu packages.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor Ubuntu Lucid Lynx, enter the following into a terminal:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-add-repository ppa:hets/hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-add-repository \
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski "deb http://archive.canonical.com/ubuntu lucid partner"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisudo apt-get update
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-get install hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor later Ubuntu versions, replace lucid by maverick, natty or oneiric.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis will also install quite a couple of tools for proving requiring about
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski800 MB of disk space. For a minimal installation use \texttt{apt-get install
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski hets-core} instead of \texttt{hets}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item For Mac OS X 10.6 (Snow Leopard) we provide a meta package
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{Hets.mpkg} based on MacPorts that will be extended by further tools
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for proving in the future.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThen we have Java based \Hets installer that we may drop in the future.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDownload a \texttt{.jar} file and start it with
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{lstlisting}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{lstlisting}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiNote that you need Sun/Oracle Java 1.4.2 or later. On a Mac, you can just
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidouble-click on the \texttt{.jar} file, but you have to install the MacPorts
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{libglade2} package (and all its dependencies) yourself. In order to
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispeed this up we provide a meta package \texttt{libglade2.mpkg}, too.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe installer will lead you through the installation with
30256573a343132354b122097b0ee1215dda1364Till Mossakowskia graphical interface. It will download and install further
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisoftware (if not already installed on your computer):
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\begin{tabularx}{\linewidth}{|l|l|X|}\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiTcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiDarwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\end{tabularx}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiIf you do not have Sun/Oracle Java, you can just download the hets binary.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiYou have to unpack it with \texttt{bunzip2} and then put it into
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskisome place covered by your \texttt{PATH} environment variable. You also have to
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiinstall the above mentioned software and set
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiseveral environment variables, as explained on the installation page.
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiYou may compile \Hets from the sources (they are licensed under GPL),
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiplease follow the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilink ``Hets: source code and information for developers''
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskion the \Hets web page, download the sources (as tarball or from
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisvn), and follow the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinstructions in the \texttt{INSTALL} file, but be prepared to take some time.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{enumerate}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDepending on your application further tools are supported and may be
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinstalled in addition:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{tabularx}{\linewidth}{|l|l|X|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskizChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiminisat & SAT solver & \url{http://minisat.se/} \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiE-KRHyper & theorem prover
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiReduce & computer algebra system
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski & \url{http://www.reduce-algebra.com/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiVSE & theorem prover & (non-public) \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTwelf & & \url{http://twelf.plparty.org/} \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{tabularx}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Analysis of Specifications}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiConsider the following Common Logic text written in CLIF:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{lstlisting}[language=clif]
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(and (P x) (Q y))
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(or (Cat x) (Mat y))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(not (On x y))
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski(if (P x) (Q x))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(exists (z) (and (Pet x) (Happy z) (Attr x z)))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{lstlisting}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets can be used for parsing and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskichecking static well-formedness of specifications.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{parsing}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \index{static!analysis}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{analysis, static}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiLet us assume that the example is in a file named
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThen you can check the well-formedness of the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification by typing (into some shell):
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets checks both the correctness of this specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski with respect to the CLIF syntax, as
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiwell as its correctness with respect to the static semantics.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe following flags are available in this context:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-p}, \texttt{-{}-just-parse}] Just do the parsing
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski -- the static analysis is skipped and no development graph is created.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-s}, \texttt{-{}-just-structured}] Do the parsing and the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski static analysis of (heterogeneous) structured specifications, but
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski leave out the analysis of basic specifications. This can be used
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski for prototyping issues, namely to quickly produce a development graph
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski showing the dependencies among the specifications (cf.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Sect.~\ref{sec:DevGraph}) even if the individual specifications are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski not correct yet.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\texttt{-L DIR}, \texttt{-{}-hets-libdir=DIR}]
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill MossakowskiUse \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicalling \Hets).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThere are more flags which can be used with \Hets, see \cite{HetsUserGuide}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets accepts plain text input files (for the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipresented logics) with the following endings:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|c|c|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifilename extension & default logic & structuring language\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.owl} & OWL2 & OWL2 \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.clf} or \texttt{.clif} & CommonLogic & custom, see Sect.~\ref{relationsInCL} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinterchangeable, the former should be used for libraries of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof heterogeneous specifications (that use the \CASL structuring
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed, e.g.,
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskito Common Logic in the following way:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{lstlisting}[morekeywords=logic]
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskilogic CommonLogic
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{lstlisting}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe subsequent specifications are then parsed and analysed as
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiCommon Logic specifications. Within such specifications,
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiit is possible to use references to named \CASL specifications;
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskithese are then automatically translated along the default
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiembedding of \CASL into Common Logic (cf.\ Fig.~\ref{fig:LogicGraph}).
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski(There are also heterogeneous constructs
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskifor explicit translations between logics, see \cite{Mossakowski04}.)
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe endings \texttt{.clf} and \texttt{.clif} are available for directly reading in
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiCommon Logic CLIF texts, as in the example of \texttt{Cat.clif}.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskithe logic Common Logic has to be chosen explicitly, and the \CASL structuring
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskisyntax needs to be used:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{lstlisting}[language=clif,morekeywords={library,logic,spec,then}]
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskilogic CommonLogic
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (and (P x) (Q y))
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski. (or (Cat x) (Mat y))
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (not (On x y))
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (if (P x) (Q x))
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskispec PetHappy =
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiPred and Cat then
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski. (exists (z) (and (Pet x) (Happy z) (Attr x z)))
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{lstlisting}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiNote that the dot at the beginning of a line indicates that a new text begins.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiHence, it is possible to have multiple texts in a \CASL specification.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThis specification is the \HetCASL-structured equivalent to the following three
30256573a343132354b122097b0ee1215dda1364Till MossakowskiCLIF files:\footnote{Note that where the Common Logic specification requires ``cl:text'', some samples available on the Web use ``cl-text''. Therefore, \Hets also supports the latter.}\\
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{lstlisting}[language=clif]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (and (P x) (Q y))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{lstlisting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{lstlisting}[language=clif]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (or (Cat x) (Mat y))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (not (On x y))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (if (P x) (Q x))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{lstlisting}[language=clif]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(cl:text PetHappy
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (cl:imports Pred) (cl:imports Cat)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (exists (z) (and (Pet x) (Happy z) (Attr x z)))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBoth can be directly used with \Hets, where the former content would be in a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifile with the extension \texttt{.het} and the latter in a file with one of the extensions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.clf} or \texttt{.clif}. This specification is divided into three
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiparts, which are linked to each other. These links and some more information can
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibe seen in the development graph of the file.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Development Graphs}\label{sec:DevGraph}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructured theorem proving and proof management.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiA development graph consists of a set of nodes (corresponding to whole
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructured specifications or parts thereof), and a set of edges
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicalled \emph{definition links}, indicating the dependency of each
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinvolved structured specification on its subparts. Each node is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiassociated with a signature and some set of local axioms. The axioms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof other nodes are inherited via definition links. Definition links
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare usually drawn as black solid arrows, denoting an import of another
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispecification.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiComplementary to definition links, which \emph{define} the theories of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirelated nodes, \emph{theorem links} serve for \emph{postulating}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskirelations between different theories. Theorem links are the central
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidata structure to represent proof obligations arising in formal
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTheorem links can be \emph{global} (drawn as solid arrows) or
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\emph{local} (drawn as dashed arrows): a global theorem link
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipostulates that all axioms of the source node (including the inherited
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiones) hold in the target node, while a local theorem link only postulates
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat the local axioms of the source node hold in the target node.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiBoth definition and theorem links can be \emph{homogeneous},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskii.e.\ stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe logic changes along the arrow.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTheorem links are initially displayed in red.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe \emph{proof calculus} for development graphs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{MossakowskiEtAl05,Habil} is given by rules
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithat allow for proving global theorem links by decomposing them
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinto simpler (local and global) ones. Theorem links that have been
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproved with this calculus are drawn in green by {\Hets}. Local theorem links can
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibe proved by turning them into \emph{local proof goals}. The latter
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskican be discharged using a logic-specific calculus as given by an
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskientailment system for a specific institution. Open local
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiproof goals are indicated by marking the corresponding node in the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidevelopment graph as red; if all local implications are proved, the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinode is turned into green. This implementation ultimately is based
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskion a theorem \cite{Habil} stating soundness and relative completeness
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the proof calculus for heterogeneous development graphs.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following options let \Hets display the development graph of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia specification library:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-g}, \texttt{-{}-gui}] shows the development graph in a GUI window
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-u}, \texttt{-{}-uncolored}] no colours in shown graphs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following additional options also apply typical rules from the development
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigraph calculus to the final graph and save applying these rules via the GUI.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-A}, \texttt{-{}-apply-automatic-rule}] apply the automatic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski strategy to the development graph. This is what you usually want in order to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski get goals within nodes for proving.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-N}, \texttt{-{}-normal-form}] compute all normal forms for nodes
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with incoming hiding links. (This may take long and may not be implemented
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for all logics.)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor a summary of the types of nodes and links occurring in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidevelopment graphs, see the \Hets user guide \cite{HetsUserGuide}.\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMost of the pull-down menus of the development graph window are
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiuDraw(Graph)-specific layout menus; their function can be looked up in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe uDraw(Graph) documentation\footnote{see
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill MossakowskiThe Edit menu is the only exception.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWith choosing Edit→Proofs→Auto-DG prover, you can can prove red theorem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilinks (which may be generated by relative interpretations of theories).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiActually, this will generate new proof obligations at some node,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhich then can be discharged there.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMoreover, the nodes and links of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigraph have attached pop-up menus, which appear when clicking (and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiholding) the right mouse button.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe node menus ``Prove'' and ``Check consistency'' are the most
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimportant ones. With ``Add sentence'', you can add axioms and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof goals on the fly.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor a detailed explanation of the menus
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisee the \Hets User Guide \cite{HetsUserGuide}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{Relations between Common Logic Texts}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{relationsInCL}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets supports several relations between Common Logic Texts. However only one of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithem is defined in ISO/IEC 24707:2007 \cite{iso24a}. All the other relations are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiunofficial extensions used e.g.\ by the Common Logic Repository COLORE \cite{Colore}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Importation] \label{descr:link_import}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski is defined in ISO/IEC 24707:2007 \cite{iso24a} as virtual copying of a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski resource. In \Hets a whole file is ``copied'' into the importing
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski specification. Hets cannot currently handle cyclic imports. If you really need
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski them, send us a message at \href{mailto:hets@informatik.uni-bremen.de}{hets@informatik.uni-bremen.de}, and we will fix it.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Using CLIF, you can import \texttt{someFile.clif} via
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{lstlisting}[language=clif]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \end{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Omitting the file extension will also succeed. In this case \Hets will look
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for a file called \texttt{someFile.clif} in first place and then for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{someFile.clf} in the current directory and then in the library paths.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \Hets also supports URIs for importing resources. The allowed URI schemes are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{file:}, \texttt{http:} and \texttt{https:}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{lstlisting}[language=clif]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(cl:imports file:///absolute/path/to/someFile.clif)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(cl:imports http://someDomain.com/path/to/someFile.clif)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(cl:imports https://someDomain.com/path/to/someFile.clif)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \end{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski The importation is indicated by a global definition link (black arrow) in the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski development graph.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Relative interpretation]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski is described in \cite{colore-fois}. It is represented by a theorem link
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (red arrow) in the development graph. In a Common Logic file it is specified
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski inside of a comment on text-level, that is a comment in the uppermost level
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski of the (optionally named) Common Logic text instead of a comment in a sentence or
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \begin{lstlisting}[language=clif]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(cl:text someText
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (cl:comment '(relative-interprets someTranslationFile someTargetFile)')
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \end{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Just as with imports (\ref{descr:link_import}), \Hets supports different types
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski of references to resources here, such as URIs.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Alternatively, the \HetCASL syntax for relative interpretations is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\textbf{view} \textit{v} : \textit{sp1} \textbf{to} \textit{sp2} \textbf{end}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Views are declared outside of specifications, as can be seen from List.~\ref{fig:lang}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Nonconservative extension]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski is represented by a theorem link (red arrow) in the development graph. In a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Common Logic file it is specified inside of a comment on text-level:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{lstlisting}[language=clif]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(cl:comment '(nonconservative-extension someTargetFile)')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \end{lstlisting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Just as with imports (\ref{descr:link_import}), \Hets supports different types
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski of references to resources here, as e.g. URIs.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%TODO: briefly describe colore-relations.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%TODO: include other colore-relations
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[Inclusion]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski is not a relation between theories. However inclusion can useful. It is used
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski to show other theories in the development graph, without any connection
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski to the current theory. In a Common Logic file inclusion is specified in a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski text-level comment:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \begin{lstlisting}[language=clif]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(cl:comment '(include-libs someFile someOtherFile nextFile andSoOn)')
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski \end{lstlisting}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski The keyword \texttt{include-libs} is followed by a whitespace-separated list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski of resources to be shown in the development graph. The resource-names can be
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski of different type here, too.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiExcept for importation and inclusion, you can specify an optional symbol map
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(name map) in a relation.\footnote{While the ``copy'' semantics of Common Logic importations does not permit renamings, \HetCASL's extension mechanism offers an alternative possibility to reuse ontologies and rename some of their symbols, using the ``\textit{importedSpec} \textbf{with} \textit{name1Old} |-> \textit{name1New}, \textit{name2Old} |-> \textit{name2New} \textbf{then} \textit{importingSpec}'' syntax.}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Names from the target file are mapped to names from the current
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifile (including the translation file, if the relation uses one).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe example has two almost identical files, \texttt{upper.clif} and
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\texttt{lower.clif}. The only difference in the actual axioms is that
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\texttt{upper.clif} uses uppercase predicates while \texttt{lower.clif}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiuses lowercase predicates. The symbol is added at the end of the relation
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskidefinition in parentheses. Only those names that differ between source
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiand target need to be listed. The other names are implicitly the same.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiA mapping of a single name is defined with
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski``\texttt{nameInTargetFile |-> nameInCurrentFile}''; multiple mappings are
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiseparated by commas. Note that in Common Logic, a comma can be part of a name.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHence a space must be placed between the separation-comma and a name.\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{lstlisting}[language=clif]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(cl:text upper
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (cl:comment '(nonconservative-extension lower
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (forall (x y) (iff (A x y)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{lstlisting}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{lstlisting}[language=clif]
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(cl:text lower
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (cl:comment '(nonconservative-extension upper (A |-> a , B |-> b))')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (forall (x y) (iff (a x y)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\end{lstlisting}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiNote that is is possible to use cyclic relations in \Hets. Only the cyclic
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiimportation is not supported.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\section{Proofs with \Hets}\label{sec:Proofs}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe proof calculus for development graphs (Sect.~\ref{sec:DevGraph}) reduces
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiglobal theorem links to local proof goals. You can do this reduction by clicking
30256573a343132354b122097b0ee1215dda1364Till Mossakowskion the Edit-menu in the development graph window and selecting
30256573a343132354b122097b0ee1215dda1364Till MossakowskiProofs/Auto-DG-Prover. Local proof goals (indicated by red
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskinodes in the development graph) can be eventually discharged using a theorem
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiprover, i.e.\ by using the ``Prove'' menu of a red node.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThe graphical user interface (GUI) for calling a prover is shown in
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiFig.~\ref{fig:proof_window} --- we call it ``Proof Management GUI''.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThe top list on the left shows all goal names prefixed with their proof
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskistatus in square brackets. A proved goal is indicated by a `+', a `–'
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiindicates a disproved goal, a space denotes an open goal, and a
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski`$\times$' denotes an inconsistent specification (aka a fallen `+';
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskisee below for details).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{figure}[ht]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \includegraphics[width=0.5\linewidth,keepaspectratio=true]{UserGuideCL_Prove_devGraph}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \caption{Prove local proof obligation\label{fig:Prove_devGraph}}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{figure}[ht]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{minipage}[b]{0.5\linewidth}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Prove_Prove}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \caption{\Hets Goal and Prover Interface\label{fig:proof_window}}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\end{minipage}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\hspace{0.1\linewidth}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{minipage}[b]{0.5\linewidth}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Prove_Vampire}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski \caption{Interface of Vampire Prover\label{fig:Vampire}}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\end{minipage}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiIf you open this GUI when processing the goals of one node for the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifirst time, it will show all goals as open. Within this list you can
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiselect those goals that should be inspected or proved. The GUI elements are the following:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{itemize}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item The button `Display' shows the selected goals in the ASCII syntax of
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski this theory's logic in a separate window.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\item By pressing the `Proof details' button a window is opened where for each
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski proved goal the used axioms, its proof script, and its proof are shown ---
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski the level of detail depends on the used theorem prover.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item With the `Prove' button the actual prover is launched. The provers are described
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich in more detail in the \Hets user guide \cite{HetsUserGuide}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item The list `Pick Theorem Prover:' lets you choose one of the connected
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski provers (among them \Isabelle, MathServe Broker, \SPASS, Vampire, and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski zChaff, described below). By pressing `Prove' the selected prover is
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski launched and the theory along with the selected goals is translated via the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski shortest possible path of comorphisms into the prover's logic.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item The pop-up choice box below `Selected comorphism path:' lets you pick a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (composed) comorphism to be used for the chosen prover. If the specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski does not contain any sequence markers, it is possible to use the comorphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \texttt{CommonLogic2CASLCompact} which results in a simpler
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \CASL specification. We recommend using this comorphism whenever possible.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item Since the amount and kind of sentences sent to an ATP system is a major
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski factor for the performance of the ATP system, it is possible to select in
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski the bottom lists the axioms and proven theorems that will comprise the
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski theory of the next proof attempt. Based on this selection the sublogic may
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski vary \ednote{CL: From here, my brain can't parse this sentence.}and also the available provers and comorphisms to provers. Former
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski theorems that are imported from other specifications are marked with the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski prefix `(Th)'. Since former theorems do not add additional logical content,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski they may be safely removed from the theory.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item If you press the bottom-right `Close' button the window is closed and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski the status of the goals' list is integrated into the development graph. If
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski all goals have been proved, the selected node turns from red into green.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item All other buttons control selecting list entries.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiIn order to prove or disprove a theorem, it needs to be declared as proof
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiobligation. This is done by the keyword \texttt{\%implied} at the end of a text:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{lstlisting}[morekeywords={logic,spec,and,implied,end}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilogic CommonLogic
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskispec ToProve =
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (and (P x) (Q y))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski. (Q y) %implied %(correct)%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski. (P y) %implied %(incorrect)%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{lstlisting}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiIn this specification the theorems, annotated (named) by \texttt{correct} and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{incorrect} are the ones, that can be proven or disproven.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiNote that they are separate texts inside the specification \texttt{ToProve}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe annotations are optional. For proving, they are the names shown in the
30256573a343132354b122097b0ee1215dda1364Till Mossakowski``Axioms to include'' section of the prover interface
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(Fig.~\ref{fig:proof_window}).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThe same specification can be written down in CLIF:
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{lstlisting}[language=clif,morekeywords={implied}]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski(cl:text axiom
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (and (P x) (Q y))
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(cl:text correct
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(cl:text incorrect (P y)) %implied
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{lstlisting}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiIn CLIF, there is no notion of proof obligation. Hence the \texttt{\%implied}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskikeyword of \Hets must be used, and thus the specification is not pure CLIF. Because the texts have
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskinames, these are also used in the prover interface. Otherwise, \Hets invents
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection{Consistency Checker}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\label{sec:CC}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiSince proofs are void if specifications are inconsistent, the consistency
30256573a343132354b122097b0ee1215dda1364Till Mossakowskishould be checked (if possible for the given logic) by the ``Consistency
30256573a343132354b122097b0ee1215dda1364Till Mossakowskichecker'' shown in Fig.~\ref{fig:cons_window}. This GUI is invoked from
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe `Edit' menu as it operates on all nodes.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe list on the left shows all node names prefixed with a consistency status
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiin square brackets that is initially empty. A consistent node is indicated by
30256573a343132354b122097b0ee1215dda1364Till Mossakowskia `+', a `–' indicates an inconsistent node, a `t' denotes a timeout of the last
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskichecking attempt.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}[ht]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{minipage}[b]{0.5\linewidth}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Consistency_devGraph}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \caption{Selection of consistency checker\label{fig:cons_devGraph}}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{minipage}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\hspace{0.1\linewidth}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{minipage}[b]{0.5\linewidth}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Consistency_Interface}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \caption{\Hets Consistency Checker Interface\label{fig:cons_window}}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{minipage}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFor some selection of nodes (of a common logic) a model finder should be
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiselectable from the `Pick Model finder:' list. Currently only for ``darwin''
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisome \CASL models can be re-constructed. When pressing `Check', possibly after
30256573a343132354b122097b0ee1215dda1364Till Mossakowski`Select comorphism path:', all selected nodes will be checked, spending at
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimost the number of seconds given under `Timeout:' on each node. Pressing
30256573a343132354b122097b0ee1215dda1364Till Mossakowski`Stop' allows to terminate this process if too many nodes have been chosen.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiEither by `View results' or automatically the `Results of consistency check'
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(Fig.~\ref{fig:cons_res}) will pop up and allow you to inspect the models for
30256573a343132354b122097b0ee1215dda1364Till Mossakowskinodes, if they could be constructed.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{figure}[ht]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \includegraphics[width=0.75\linewidth,keepaspectratio=true]{UserGuideCL_Consistency_Result}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \caption{Consistency checker results\label{fig:cons_res}}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsection[Automated Theorem Proving Systems]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski{Automated Theorem Proving Systems\\(Logic SoftFOL)}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\label{sec:ATP}
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski\begin{figure}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\includegraphics[width=\textwidth]{spassGUI1}
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski\caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAll ATPs integrated into \Hets share the same GUI, with only a slight
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskimodification for the MathServe Broker: the input field for extra options is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiinactive. Fig.~\ref{fig:SPASS_GUI} shows the instantiation for \SPASS, where
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiin the top right part of the window the batch mode can be controlled. The
30256573a343132354b122097b0ee1215dda1364Till Mossakowskileft side shows the list of goals (with status indicators). If goals are
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitimed out (indicated by `t') it may help to activate the check box `Include
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipreceding proven theorems in next proof attempt' and pressing `Prove all'
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiOn the bottom right the result of the last proof
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiattempt is displayed. The `Status:' indicates `Open', `Proved', `Disproved',
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski`Open (Time is up!)', or `Proved (Theory inconsistent!)'. The list of `Used
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAxioms:' is filled by \SPASS. The button `Show Details' shows the whole output
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof the ATP system. The `Save' buttons allow you to save the input and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiconfiguration of each proof for documentation. By `Close' the results for all
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskigoals are transferred back to the Proof Management GUI.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiZimmer provides a unified interface to a range of different ATP
a231094086321e19f9a689de4745512c91e00e4bTill Mossakowskisystems; the most important systems are listed in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiTab.~\ref{tab:MathServe}, along with their capabilities. These
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicapabilities are derived from the \emph{Specialist Problem Classes}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski(SPCs) defined upon the basis of logical, language and syntactical
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiproperties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiOnly two of the Web services provided by the MathServe system are used
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskiby \Hets currently: Vampire and the brokering system. The ATP systems
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiare offered as Web Services using standardised protocols and formats
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisuch as SOAP, HTTP and XML. Currently, the ATP system Vampire may be
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiaccessed from \Hets via MathServe; the other systems are only reached
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiafter brokering.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{table}[t]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \begin{threeparttable}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \begin{tabular}{|l|c|p{7cm}|}\firsthline
30256573a343132354b122097b0ee1215dda1364Till Mossakowski ATP System & Version & Suitable Problem Classes\tnote{a}\\
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \hhline{|=|=|=|}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich DCTP & 10.21p & effectively propositional \\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich EP & 0.91 & effectively propositional; real first-order, no
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich equality; real first-order, equality\\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich Otter & 3.3 & real first-order, no equality\\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \SPASS & 2.2 & effectively propositional; real first-order, no
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich equality; real first-order, equality\\\hline
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich Vampire & 8.0 & effectively propositional; pure equality, equality
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski clauses contain non-unit equality clauses; real first-order, no
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski equality, non-Horn\\\hline
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski Waldmeister & 704 & pure equality, equality clauses are unit
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski equality clauses\\\lasthline
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \end{tabular}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski %\renewcommand{\thempfootnote}{\arabic{mpfootnote}}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski %\footnotetext%[\value{footnote}\stepcounter{footnote}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \begin{tablenotes}\footnotesize
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich {The list of problem classes for each ATP system is not
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich exhaustive, but only the most appropriate problem classes are
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich named according to benchmark tests made with MathServe by
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich J\"urgen Zimmer.}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \end{tablenotes}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \end{threeparttable}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \caption{ATP systems provided as Web services by MathServe}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\vspace*{-4mm}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \label{tab:MathServe}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichFor details on the ATPs supported, see the \Hets user guide \cite{HetsUserGuide}.
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich\section{Reading, Writing and Formatting}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\Hets provides several options controlling the types of files
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskithat are read and written.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{description}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\item[\texttt{-i ITYPE}, \texttt{-{}-input-type=ITYPE}] Specify \texttt{ITYPE}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski as explicit type of the input file.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski \texttt{exp} files contain a development graph in a new experimental OMDoc
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski format. \texttt{prf} files contain additional development steps (as shared
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski ATerms) to be applied on top of an underlying development graph created from
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski a corresponding \texttt{env}, \texttt{casl}, or \texttt{het}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich file. \texttt{hpf} files are plain text files representing heterogeneous
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich proof scripts. The contents of a \texttt{hpf} file must be valid input for
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \Hets in interactive mode. (\texttt{gen\_trm} formats are currently not
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe possible input types are:
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{lstlisting}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski | [tree.]gen_trm[.baf]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{lstlisting}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-O DIR}, \texttt{-{}-output-dir=DIR}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichSpecify \texttt{DIR} as destination directory for output files.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-o OTYPES}, \texttt{-{}-output-types=OTYPES}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\texttt{OTYPES} is a comma-separated list of output types:
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{lstlisting}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich | (sig|th)[.delta]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich | pp.(het|tex|xml|html)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{lstlisting}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{env} and \texttt{prf} formats are for subsequent reading,
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichavoiding the need to re-analyse downloaded libraries. \texttt{prf} files
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcan also be stored or loaded via the GUI's File menu.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{omn} option \cite{w3c:owl2-manchester} will produce OWL files in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichManchester Syntax for each specification of a structured OWL library.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{clif} option will produce Common Logic files in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichCLIF dialect for each specification of a Common Logic library.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichmarkup format and data model for Open Mathematical Documents. It
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichserves as semantics-oriented representation format and ontology
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichlanguage for mathematical knowledge. Although this is still in experimental
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichstate, Common Logic theories can be exported to and imported from OMDoc.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{xml} option will produce an XML-version of the development graph
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichfor our change management broker.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{exp} format is the new experimental omdoc format.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{hs} format is used for Haskell modules. Executable \CASL or
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\HasCASL specifications can be translated to Haskell.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichWhen the \texttt{thy} format is selected, \Hets will try to translate
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luetticheach specification in the library to \Isabelle, and write one \Isabelle
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\texttt{.thy} file per specification.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichWhen the \texttt{comptable.xml} format is selected, \Hets will extract
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichthe composition and inverse table of a Tarskian relation algebra from
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichspecification(s) (selected with the \texttt{-n} or \texttt{-{}-spec}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichoption). It is assumed that the relation algebra is
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichgenerated by basic relations, and that the specification is written
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichin the \CASL logic. A sample specification of a relation
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichalgebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichavailable from \url{http://www.cofi.info/Libraries}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe output format is XML, the URL of the DTD is included in the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{sig} or \texttt{th} option will create \HetCASL signature or
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichtheory files for each development graph node. (The \texttt{.delta} extension
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichis not yet supported.)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{pp} format is for pretty printing, either as plain text
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich(\texttt{het}), \LaTeX\ input (\texttt{tex}), HTML (\texttt{html}) or XML
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich(\texttt{xml}). For example, it is possible to generate a pretty printed
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\LaTeX\ version of \texttt{Cat.clif} by typing:
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThis will generate a file \texttt{Cat.pp.tex}. It can be included
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichcoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe format \texttt{pp.xml} represents just a parsed library in XML.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichFormats with \texttt{graph} are reserved for future usage.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{dfg} format is used by the \SPASS theorem prover
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\cite{WeidenbachEtAl02}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichexchange format for first-order theorem provers.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichAppending \texttt{.c} to \texttt{dfg} or \texttt{tptp} will create files for
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichconsistency checks by SPASS or Darwin respectively.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichFor all output formats it is recommended to increase the verbosity to at least
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichlevel 2 (by using the option \texttt{-v2}) to get feedback which files are
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiactually written. (\texttt{-v2} also shows which files are read.)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item[\texttt{-t TRANS}, \texttt{-{}-translation=TRANS}]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskichooses a translation option. \texttt{TRANS} is a colon-separated list
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiwithout blanks of one or more comorphism names (see Sect.~\ref{comorphisms})
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-n SPECS}, \texttt{-{}-spec=SPECS}]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskichooses a list of named specifications for processing
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-w NVIEWS}, \texttt{-{}-view=NVIEWS}]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskichooses a list of named views for processing
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-R}, \texttt{-{}-recursive}] output also imported libraries
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-I}, \texttt{-{}-interactive}] run \Hets in interactive mode
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-X}, \texttt{-{}-server}] run \Hets as web server (see
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski Sect.~\ref{sec:Server})
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-x}, \texttt{-{}-xml}] use XML-PGIP\footnote{Proof General Interface Protocol} packets to communicate with
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \Hets in interactive mode
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-S PORT}, \texttt{-{}-listen=PORT}] communicate
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski with \Hets in interactive mode by listening to the port \texttt{PORT}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-c HOSTNAME:PORT}, \texttt{-{}-connect=HOSTNAME:PORT}] communicate
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski with \Hets in interactive mode via connecting to the port on host
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \texttt{HOSTNAME}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item[\texttt{-d STRING}, \texttt{-{}-dump=STRING}] produces implementation
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski dependent output for debugging purposes only
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (i.e.\ \texttt{-d LogicGraph} lists the logics and comorphisms)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\end{description}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\section{Hets as a web server}\label{sec:Server}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiLarge parts of \Hets are now also available via a web interface. A running
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiserver should be accessible on
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\url{http://pollux.informatik.uni-bremen.de:8000/}. It allows to browse the
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\Hets library, upload a file or just a \HetCASL specification. Development
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskigraphs for well-formed specifications can be displayed in various formats
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiwhere the \texttt{svg} format is supposed to look like the graphs displayed by
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiuDrawGraph. Besides browsing, the web server is supposed to be accessed by
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichother programs using queries. The possible queries are described at
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\url{http://trac.informatik.uni-bremen.de:8080/hets/wiki/RESTfulInterface}.
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiFor details on this topic, see the \Hets user guide \cite{HetsUserGuide}.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\section{Miscellaneous Options}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\begin{description}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-v[Int]}, \texttt{-{}-verbose[=Int]}]
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiSet the verbosity level according to \texttt{Int}. Default is 1.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\item[\texttt{-q}, \texttt{-{}-quiet}]
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiBe quiet -- no diagnostic output at all. Overrides -v.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-V}, \texttt{-{}-version}] Print version number and exit.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-h}, \texttt{-{}-help}, \texttt{-{}-usage}]
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiPrint usage information and exit.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \texttt{Int} megabytes (needed in case of a stack overflow).
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThis must be the first option.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-l LOGIC}, \texttt{-{}-logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskideclaration. The default is \CASL.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\texttt{-e ENCODING}, \texttt{-{}-encoding=ENCODING}] Read input files using latin1 or utf8 encoding. The default is still latin1.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\texttt{-{}-unlit}] Read literate input files.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-{}-relative-positions}] Just uses the relative library name in positions of warning or errors.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-U FILE}, \texttt{-{}-xupdate=FILE}] update a development graph according to special XML update information (still experimental).
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-m FILE}, \texttt{-{}-modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\bibliographystyle{plain}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\bibliography{cofibib,cofi-ann,UM,hets,kl,hetsForCL}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% Local Variables:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%% mode: latex
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%%% TeX-master: "UserGuideCommonLogic"
30256573a343132354b122097b0ee1215dda1364Till Mossakowski%%% ispell-local-dictionary: "british"
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: SPASS darwin uninger Hets HetCASL SoftFOL EL QL RL zChaff TPTP
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: Eprover KRHyper MathServe CASL THF HasCASL RelScheme CommonLogic
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: CASLCompact CommonLogicModuleElimination SuleCFOL hets oneiric
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: SoftFOLInduction mpkg MacPorts libglade uDraw Tcl Tk bunzip VSE
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: minisat Twelf Attr clif libdir casl het clf Pred PetHappy gui DG
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: uncolored COLORE someFile http https someText someTargetFile sp
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: someTranslationFile someAxiom Nonconservative nonconservative EP
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: libs someOtherFile nextFile andSoOn nameInTargetFile forall iff
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: nameInCurrentFile ToProve ATPs rgen Zimmer SPCs Sutcliffe DCTP
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: Suttner Waldmeister urgen ITYPE OMDoc prf ATerms env hpf trm hs
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: maude hol omdoc xml baf dir OTYPES omn comptable sig th tex html
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: dfg tptp Tarskian hetcasl NVIEWS pgip HOSTNAME LogicGraph svg
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: uDrawGraph RTS KIntM latin utf xupdate modelSparQ SparQ cofibib
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: cofi ann hetsForCL Mossakowski Maeder Mihai Codescu
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: Kuksa DFKI GmbH IEC lang basicstyle morecomment
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% LocalWords: escapeinside importedSpec importingSpec