UserGuideCommonLogic.tex revision f4aeb94f5c4d7055923e81b9ed2443cee3ded2c5
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\setlength{\textwidth}{16cm}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\setlength{\topmargin}{-1cm}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\setlength{\evensidemargin}{0cm}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\setlength{\oddsidemargin}{0cm}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\setlength{\textheight}{22.5cm}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage[utf8]{inputenc}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage[T1]{fontenc}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{charter} % very clean and readable font
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{courier}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage{unicode-chars}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\usepackage[hide]{ed} % set to hide for producing a released version
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\usepackage{alltt}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{casl}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{color}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage{url}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{threeparttable,hhline}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{tabularx}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{paralist}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{lstsemantic} % loads listings and defines some languages
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\lstset{basicstyle=\ttfamily,columns=fixed}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{amssymb}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{mathtools}
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}]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder{hyperref} %% do not load more packages after this line!!
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\QUERY}[1]%{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\eat}[1]{}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\IEXT}[1] {\\#1\I}
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} {}{}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\newcommand {\CoFI}{CoFI\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till 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}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SDF}{SDF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
e91e02579a34e005734059ad09e0d1d1304a03e0Till Mossakowski%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
464c78620a182d2e8fbd125098045eae8788e2bdTill 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}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{document}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\title{{\bf \protect{\LARGEHets} for Common Logic Users}\\
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski-- Version 0.99 --}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\author{Till Mossakowski, Christian Maeder,
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski Mihai Codescu, Eugen Kuksa, Christoph Lange\\[1em]
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiDFKI GmbH, Bremen, Germany.\\[1em]
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiComments to: \href{mailto:hets-users@informatik.uni-bremen.de}{hets-users@informatik.uni-bremen.de} \\
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski(the latter needs subscription to the mailing list)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\setcounter{tocdepth}{1}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\tableofcontents
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\section{Introduction}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiCommon Logic (CL) is an ISO standard published as ``ISO/IEC 24707:2007
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski--- Information technology — Common Logic (CL): a framework for a family
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiof logic-based languages'' \cite{CommonLogic:oldfashioned}. CL is based on untyped first-order
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskilogic, but extends first-order logic in two ways: \begin{inparaenum}[(1)]\item any term can be
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiused as function or predicate, and \item sequence markers allow
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskifor talking about sequences of individuals directly\end{inparaenum}.\footnote
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski{Strictly speaking, only the second feature goes beyond first-order
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe Heterogeneous Tool Set (\Hets) is an open source software providing
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiseveral kinds of tool support for Common Logic:
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{itemize}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item a parser for the Common Logic Interchange Format (CLIF) --- CLIF
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski is a Lisp-like syntax for CL;
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\item a connection of CL to well-known first-order theorem provers
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilike SPASS, darwin and Vampire, such that logical consequences
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiof CL theories can be proved;
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item a connection of CL to the higher-order provers Isabelle/HOL
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiand Leo-II in order to perform induction proofs in theories
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinvolving sequence markers;
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item a connection to first-order model finders like darwin that
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederallow one to find models for CL theories;
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item support for proving interpretations between CL theories to be correct;
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item a translation that eliminates the use of CL modules\footnote{Actually, we are using a revised semantics for modules, as proposed
30256573a343132354b122097b0ee1215dda1364Till Mossakowskirecently in~\cite{NH:CommonLogicHoratio}.}. Since the semantics of CL modules
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis special to CL, this elimination of modules is necessary before
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisending CL theories to a standard first-order prover;
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item a translation of the Web Ontology Language OWL to CL;
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item a translation of propositional logic to CL.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThis guide will introduce you to these functionalities of \Hets.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFor the full functionalities of \Hets, see the \Hets user guide
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{HetsUserGuide}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\section{The Heterogeneous Tool Set and Its Input Languages}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe central idea of the Heterogeneous Tool Set (\protect\Hets) is to
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiprovide a general framework for formal methods integration and proof
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimanagement. One can think of \Hets acting like a motherboard where
30256573a343132354b122097b0ee1215dda1364Till Mossakowskidifferent expansion cards can be plugged in, the expansion cards here
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskibeing individual logics (with their analysis and proof tools) as well
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskias logic translations. The \Hets motherboard already has plugged in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia number of expansion cards (e.g., the theorem provers Isabelle, SPASS
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskiand more, as well as model finders). Hence, a variety of tools is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiavailable, without the need to hard-wire each tool to the logic at
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \includegraphics[width=0.45\textwidth]{hets-motherboard}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{The \Hets motherboard and some expansion cards}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets consists of logic-specific tools for the parsing and static
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskianalysis of the different involved logics, as well as a
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskilogic-independent parsing and static analysis tool for structured and
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskito call the logic-specific tools whenever a basic specification is
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\Hets is based on the theory of institutions \cite{GoguenBurstall92},
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiwhich formalise the notion of a logic. The theory behind \Hets is laid
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiout in \cite{Habil}. A short overview of \Hets is given in
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\cite{MossakowskiEA06,MossakowskiEtAl07b}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets supports a number of input languages directly, such as Common
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLogic and OWL2 and \HetCASL. They will be described in the next
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\subsection{Common Logic and the Common Logic Interchange Format (CLIF)}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCLIF is specified in Annex A of the Common Logic standard
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{CommonLogic:oldfashioned}. \Hets can directly read in files in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCLIF syntax, and also recursively reads in any imported files (cf.\ Sect.~\ref{relationsInCL} for the syntax).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCommon Logic itself does not support the specification of logical
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiconsequences, nor relative theory interpretations, nor other
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifeatures that speak about structuring and comparing logical
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowskifor specifications within \HetCASL files, or CLIF files can be referred to within \HetCASL
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maederfiles. \HetCASL is a structuring language supporting relative theory
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiinterpretations and other things, see Sect.~\ref{HetCASL} below.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till 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}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiSince OWL2 does not support relative theory interpretations and other
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskistructuring features, such things can only be expressed in \HetCASL
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\subsection{HetCASL}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\label{HetCASL}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor heterogeneous specification, \Hets offers the Heterogeneous
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilanguage \HetCASL. \HetCASL is not so much a logic, but a meta
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederlanguage 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
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL (Common Algebraic Specification Language \cite{CASL-UM,CASL/RefManual}) to arbitrary logics
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(if they are formalised as institutions and plugged into
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe \Hets motherboard), as well as to heterogeneous
30256573a343132354b122097b0ee1215dda1364Till 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
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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.
7a8592051724fa46499bde120f44cdc8db270876Till 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={<>}]
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSPEC ::= BASIC-SPEC %% logic-specific syntax, e.g. CLIF or Manchester syntax
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski | SPEC then SPEC %% extension of a spec with new symbols and axioms
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski | SPEC then %implies SPEC %% annotation: extension is logically implied
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski | SPEC with SYMBOL-MAP %% renaming of SPEC along SYMBOL-MAP
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | SPEC with logic ID %% translation of SPEC to a different logic
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederDEFINITION ::= 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder %% dto., but across different logics
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiLIBRARY = DEFINITION*
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\end{lstlisting}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederspecifications. \emph{Refinements} express the fact the a specification
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederis becoming more specific. All this is supported by \HetCASL.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFor details, see \cite{Mossakowski04,Habil,CASL/RefManual}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till 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:
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{figure}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \begin{center}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \includegraphics[width=.67\textwidth]{LogicGraph-CL}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\caption{Graph of logics related to Common Logic that are currently supported by \Hets. The more an
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskiellipse is filled with green, the more stable is the implementation of the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederlogic. Blue indicates a prover-supported logic.}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\label{fig:LogicGraph}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\begin{figure}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{center}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\begin{tabular}{|l|c|c|c|}\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\CASL & x & x & -- \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiCommon Logic & x (CLIF) & x & -- \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiOWL2 & x & x & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiPropositional & x & x & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till MossakowskiSoftFOL & x & -- & x \\\hline
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\caption{Current degree of \Hets support for some of the languages.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiLanguages without prover can still ``borrow'' provers
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedervia logic translations.\label{fig:Languages}}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{description}
89118fd658073a87eddf4ead4bb63c6adb30550dTill 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
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskilogic in several ways. The Common Logic
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Interchange Format (CLIF) provides a Lisp-like syntax for Common
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder Logic. \Hets currently only supports parsing CLIF. If you need
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich other dialects, send us a message and we will add them.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski\item[OWL2] is the Web Ontology Language recommended by the
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski World Wide Web Consortium (W3C, \url{http://www.w3c.org}); see \cite{w3c:owl2-overview}. It is
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski used for knowledge representation on the Semantic Web
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \cite{berners:2001:SWeb}.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiHets calls an external OWL2 parser
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski written in Java to obtain the abstract syntax for an OWL file and its
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski imports. The Java parser also does a first analysis classifying
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Hets supports all except OWL Full.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski structuring of the OWL imports is displayed as a Development Graph.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Propositional] is classical propositional logic, with
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe zChaff SAT solver \cite{Herbstritt03} connected to it.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[SoftFOL] \cite{LuettichEA06a} offers several automated theorem
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder proving (ATP) systems for first-order logic with equality: \begin{inparaenum}[(1)]\item \SPASS
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \cite{WeidenbachEtAl02}, see \url{http://www.spass-prover.org};
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item Vampire \cite{RiazanovV02} see \url{http://www.vprover.org};
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill 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}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\end{inparaenum}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski These together comprise some of the most advanced theorem provers
30256573a343132354b122097b0ee1215dda1364Till Mossakowski for first-order logic. SoftFOL is essentially the first-order
30256573a343132354b122097b0ee1215dda1364Till Mossakowski interchange language TPTP \cite{DBLP:conf/lpar/Sutcliffe10},
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[CASL] extends many sorted first-order logic with partial
30256573a343132354b122097b0ee1215dda1364Till Mossakowski functions and subsorting. It also provides induction sentences,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski expressing the (free) generation of datatypes.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiFor Common Logic, \CASL can be seen as kind of transitional hub, linking
30256573a343132354b122097b0ee1215dda1364Till MossakowskiCommon Logic to other logics, most importantly SoftFOL.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\Isabelle] \cite{NipPauWen02} is the logic of the interactive
30256573a343132354b122097b0ee1215dda1364Till Mossakowski theorem prover Isabelle for higher-order logic.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[THF] is an interchange language for higher-order logic
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \cite{DBLP:conf/cade/BenzmullerRS08}, similar to what TPTP
30256573a343132354b122097b0ee1215dda1364Till Mossakowski is for first-order logic. \Hets connects THF to the automated
30256573a343132354b122097b0ee1215dda1364Till Mossakowski higher-order prover Leo-II.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till 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
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski embedded in the specification. For Common Logic, \HasCASL
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till 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}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiVarious logics are supported with proof tools. Proof support for the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiother logics can be obtained by using logic translations to a
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiprover-supported logic. For Common Logic, the paths to SoftFOL
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiare particularly interesting, because this offers an interface
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskito standard first-order provers. Moreover, the paths to THF
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiand Isabelle offer interfaces to higher-order provers, which
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiis essential if you want to prove inductive theorems about
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiAn introduction to \CASL can be found in the \CASL User Manual
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\cite{CASL-UM}; the detailed language reference is given in
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowskithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowskiexplain both the \CASL logic and language of basic specifications as
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowskiwell as the logic-independent constructs for structured and
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiarchitectural specifications. The corresponding document explaining the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\HetCASL language constructs for \emph{heterogeneous} structured specifications
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiis the \HetCASL language summary \cite{Mossakowski04}; a formal
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskisemantics as well as a user manual with more examples are in preparation.
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiSome of \HetCASL's heterogeneous constructs will be illustrated
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiin Sect.~\ref{sec:HetSpec} below.\\
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskiFor further information on logics supported by \Hets, see the \Hets user guide
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski\cite{HetsUserGuide}.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\section{Logic translations supported by Hets}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\label{comorphisms}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiLogic translations (formalised as institution comorphisms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{GoguenRosu02}) translate from a given source logic to a given
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitarget logic. More precisely, one and the same logic translation
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedermay have several source and target \emph{sub}logics: for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskieach source sublogic, the corresponding sublogic of the target
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskilogic is indicated.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIn more detail, the following list of logic translations involving Common Logic
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskiis currently supported by \Hets:\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent\begin{tabularx}{\textwidth}{|l|X|}\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCommonLogic2CASL & Coding Common Logic to \CASL. Module elimination
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski is applied before translating to \CASL. \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederCommonLogic2CASLCompact & Coding compact Common Logic to \CASL.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCommonLogicModuleElimination & Eliminating modules from a Common Logic theory
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski resulting in an equivalent specification without
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski modules. \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiOWL22CommonLogic & Inclusion of OWL2 description logic \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiProp2CommonLogic & Inclusion of propositional logic \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiSoftFOL2CommonLogic & Inclusion of first order logic \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2SoftFOL & Coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskimapping types to soft types \\\hline
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiCASL2SoftFOLInduction & Same as CASL2SoftFOL but with instances of induction
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiaxioms for all proof goals \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL2SoftFOLInduction2 & Similar to CASL2SoftFOLInduction but replaces goals with induction premises \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiCASL2Propositional & Translation of propositional FOL \\\hline
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\end{tabularx}\\
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThose comorphisms can be chained, e.g., for theorem proving, you can translate
c5e63ec138b908ac9d15e6843120033bf36a1862Till MossakowskiCommon Logic to SoftFOL with \texttt{CommonLogic2CASLCompact;CASL2SoftFOLInduction}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskisince there is no prover for Common Logic or \CASL.
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiFor further information on logic translations supported by \Hets, see the \Hets
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiuser guide \cite{HetsUserGuide}.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\section{Getting started}
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiThe latest \Hets version can be obtained from the
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\Hets tools home page
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski Since \Hets is being
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski\Hets is currently available (on Intel architectures only) for Linux
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThere are several possibilities to install \Hets.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{enumerate}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till MossakowskiThe best support is currently given via Ubuntu packages.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor Ubuntu Lucid Lynx, enter the following into a terminal:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{lstlisting}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisudo apt-add-repository ppa:hets/hets
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisudo apt-add-repository \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski "deb http://archive.canonical.com/ubuntu lucid partner"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisudo apt-get update
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-get install hets
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor later Ubuntu versions, replace lucid by maverick, natty or oneiric.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThis 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.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDownload a \texttt{.jar} file and start it with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote that you need Sun/Oracle Java 1.4.2 or later. On a Mac, you can just
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidouble-click on the \texttt{.jar} file, but you have to install the MacPorts
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{libglade2} package (and all its dependencies) yourself. In order to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispeed this up we provide a meta package \texttt{libglade2.mpkg}, too.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe installer will lead you through the installation with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia graphical interface. It will download and install further
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisoftware (if not already installed on your computer):
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{tabularx}{\linewidth}{|l|l|X|}\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDarwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{tabularx}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIf you do not have Sun/Oracle Java, you can just download the hets binary.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiYou have to unpack it with \texttt{bunzip2} and then put it into
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisome place covered by your \texttt{PATH} environment variable. You also have to
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinstall the above mentioned software and set
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiseveral environment variables, as explained on the installation page.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiYou may compile \Hets from the sources (they are licensed under GPL),
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiplease follow the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilink ``Hets: source code and information for developers''
30256573a343132354b122097b0ee1215dda1364Till Mossakowskion the \Hets web page, download the sources (as tarball or from
30256573a343132354b122097b0ee1215dda1364Till Mossakowskisvn), and follow the
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinstructions in the \texttt{INSTALL} file, but be prepared to take some time.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{enumerate}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDepending on your application further tools are supported and may be
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinstalled in addition:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{tabularx}{\linewidth}{|l|l|X|}\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskizChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowskiminisat & SAT solver & \url{http://minisat.se/} \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiPellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiE-KRHyper & theorem prover
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiReduce & computer algebra system
30256573a343132354b122097b0ee1215dda1364Till Mossakowski & \url{http://www.reduce-algebra.com/} \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiVSE & theorem prover & (non-public) \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiTwelf & & \url{http://twelf.plparty.org/} \\\hline
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\end{tabularx}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski\section{Analysis of Specifications}
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek MakowskiConsider the following Common Logic text written in CLIF:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{lstlisting}[language=clif]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(and (P x) (Q y))
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski(or (Cat x) (Mat y))
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski(not (On x y))
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski(if (P x) (Q x))
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski(exists (z) (and (Pet x) (Happy z) (Attr x z)))
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\end{lstlisting}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\Hets can be used for parsing and
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskichecking static well-formedness of specifications.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \index{parsing}%
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \index{static!analysis}%
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \index{analysis, static}%
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiLet us assume that the example is in a file named
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThen you can check the well-formedness of the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecification by typing (into some shell):
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till 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.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder static analysis of (heterogeneous) structured specifications, but
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski leave out the analysis of basic specifications. This can be used
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for prototyping issues, namely to quickly produce a development graph
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski showing the dependencies among the specifications (cf.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Sect.~\ref{sec:DevGraph}) even if the individual specifications are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski not correct yet.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-L DIR}, \texttt{-{}-hets-libdir=DIR}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiUse \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicalling \Hets).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThere are more flags which can be used with \Hets, see \cite{HetsUserGuide}.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski\Hets accepts plain text input files (for the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskipresented logics) with the following endings:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|c|c|}\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifilename extension & default logic & structuring language\\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.owl} & OWL2 & OWL2 \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\texttt{.clf} or \texttt{.clif} & CommonLogic & custom, see Sect.~\ref{relationsInCL} \\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederAlthough the endings \texttt{.casl} and \texttt{.het} are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinterchangeable, the former should be used for libraries of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof heterogeneous specifications (that use the \CASL structuring
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed, e.g.,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskito Common Logic in the following way:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{lstlisting}[morekeywords=logic]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederlogic CommonLogic
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{lstlisting}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThe subsequent specifications are then parsed and analysed as
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederCommon Logic specifications. Within such specifications,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederit is possible to use references to named \CASL specifications;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithese are then automatically translated along the default
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiembedding of \CASL into Common Logic (cf.\ Fig.~\ref{fig:LogicGraph}).
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(There are also heterogeneous constructs
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifor explicit translations between logics, see \cite{Mossakowski04}.)
a8ce558d09f304be325dc89458c9504d3ff7fe80Till MossakowskiThe endings \texttt{.clf} and \texttt{.clif} are available for directly reading in
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCommon Logic CLIF texts, as in the example of \texttt{Cat.clif}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederthe logic Common Logic has to be chosen explicitly, and the \CASL structuring
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowskisyntax needs to be used:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{lstlisting}[language=hetcasl,alsolanguage=clif]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilogic CommonLogic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (and (P x) (Q y))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski. (or (Cat x) (Mat y))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (not (On x y))
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (if (P x) (Q x))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispec PetHappy =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiPred and Cat then
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski. (exists (z) (and (Pet x) (Happy z) (Attr x z)))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{lstlisting}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiNote that the dot at the beginning of a line indicates that a new text begins.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHence, it is possible to have multiple texts in a \CASL specification.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThis specification is the \HetCASL-structured equivalent to the following three
5277e290ad70afdf97f359019afd8fb5816f4102Till 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.}\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{description}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{lstlisting}[language=clif]
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (and (P x) (Q y))
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{lstlisting}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{lstlisting}[language=clif]
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (or (Cat x) (Mat y))
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (not (On x y))
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (if (P x) (Q x))
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{lstlisting}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\begin{lstlisting}[language=clif]
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski(cl:text PetHappy
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (cl:imports Pred) (cl:imports Cat)
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (exists (z) (and (Pet x) (Happy z) (Attr x z)))
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{lstlisting}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{description}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiBoth can be directly used with \Hets, where the former content would be in a
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskifile with the extension \texttt{.het} and the latter in a file with one of the extensions
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\texttt{.clf} or \texttt{.clif}. This specification is divided into three
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiparts, which are linked to each other. These links and some more information can
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskibe seen in the development graph of the file.
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\section{Development Graphs}\label{sec:DevGraph}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskistructured theorem proving and proof management.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiA development graph consists of a set of nodes (corresponding to whole
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskistructured specifications or parts thereof), and a set of edges
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskicalled \emph{definition links}, indicating the dependency of each
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiinvolved structured specification on its subparts. Each node is
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiassociated with a signature and some set of local axioms. The axioms
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiof other nodes are inherited via definition links. Definition links
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiare usually drawn as black solid arrows, denoting an import of another
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskispecification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiComplementary to definition links, which \emph{define} the theories of
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskirelated nodes, \emph{theorem links} serve for \emph{postulating}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskirelations between different theories. Theorem links are the central
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskidata structure to represent proof obligations arising in formal
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiTheorem links can be \emph{global} (drawn as solid arrows) or
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\emph{local} (drawn as dashed arrows): a global theorem link
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskipostulates that all axioms of the source node (including the inherited
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiones) hold in the target node, while a local theorem link only postulates
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithat the local axioms of the source node hold in the target node.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBoth definition and theorem links can be \emph{homogeneous},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskii.e.\ stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskican be discharged using a logic-specific calculus as given by an
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskientailment system for a specific institution. Open local
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof goals are indicated by marking the corresponding node in the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidevelopment graph as red; if all local implications are proved, the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinode is turned into green. This implementation ultimately is based
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskion a theorem \cite{Habil} stating soundness and relative completeness
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the proof calculus for heterogeneous development graphs.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following options let \Hets display the development graph of
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedera 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}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\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
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederdevelopment 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/}.}.
5277e290ad70afdf97f359019afd8fb5816f4102Till 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
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiimportant ones. With ``Add sentence'', you can add axioms and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof goals on the fly.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiFor a detailed explanation of the menus
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisee the \Hets User Guide \cite{HetsUserGuide}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till 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
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithem is defined in ISO/IEC 24707:2007 \cite{CommonLogic:oldfashioned}. All the other relations are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiunofficial extensions used e.g.\ by the Common Logic Repository COLORE \cite{Colore}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski\item[Importation] \label{descr:link_import}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski is defined in ISO/IEC 24707:2007 \cite{CommonLogic:oldfashioned} 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]
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill 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
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{lstlisting}[language=clif]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(cl:text someText
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (cl:comment '(relatively-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 the syntax specification in List.~\ref{fig:lang}. We provide a concrete example in Sect.~\ref{sec:relat-interpr} below.
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)')
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, as e.g. URIs.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%TODO: briefly describe colore-relations.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%TODO: include other colore-relations
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[Inclusion]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski is not a relation between theories. However inclusion can useful. It is used
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski to show other theories in the development graph, without any connection
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski to the current theory. In a Common Logic file inclusion is specified in a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski text-level comment:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{lstlisting}[language=clif]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(cl:comment '(include-libs someFile someOtherFile nextFile andSoOn)')
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \end{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski The keyword \texttt{include-libs} is followed by a whitespace-separated list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski of resources to be shown in the development graph. The resource-names can be
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski of different type here, too.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiExcept for importation and inclusion, you can specify an optional symbol map
5277e290ad70afdf97f359019afd8fb5816f4102Till 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.}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Names from the target file are mapped to names from the current
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederfile (including the translation file, if the relation uses one). Note that is is possible to use cyclic relations in \Hets. Only the cyclic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimportation is not supported.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{Examples}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\label{sec:examples}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian MaederThis section introduces several typical examples of using Common Logic ontologies with \Hets.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsubsection{Renaming Symbols with Symbol Maps}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{sec:renam-symb-with}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis example has two almost identical files, \texttt{upper.clif} and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{lower.clif}; these can be found in the \texttt{CommonLogic} directory in the \Hets library \cite{hets-library:URL}. The only difference in the actual axioms is that
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{upper.clif} uses uppercase predicates while \texttt{lower.clif}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiuses lowercase predicates. The symbol is added at the end of the relation
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederdefinition in parentheses. Only those names that differ between source
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand target need to be listed. The other names are implicitly the same.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiA mapping of a single name is defined with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski``\texttt{nameInTargetFile |-> nameInCurrentFile}''; multiple mappings are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiseparated by commas. Note that in Common Logic, a comma can be part of a name.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHence a space must be placed between the separation-comma and a name.\\
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{lstlisting}[language=clif]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(cl:text upper
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (cl:comment '(nonconservative-extension lower
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (forall (x y) (iff (A x y)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{lstlisting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{lstlisting}[language=clif]
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(cl:text lower
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (cl:comment '(nonconservative-extension upper
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski , B |-> b))')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (forall (x y) (iff (a x y)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{lstlisting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\subsubsection{Relative Interpretation in COLORE}\label{sec:relat-interpr}
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiWe give two examples for relative interpretation: one from COLORE (in this section), and one standalone one (in Sect.~\ref{sec:rel-intpr-standalone}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe COLORE \cite{Colore} module \texttt{Region\-Boolean\-Contact\-Algebra} relatively interprets the module \texttt{Atomless\-Boolean\-Lattice}. These two modules specify axioms about booleans; thus, they have the same signature. In the graph of imports, they have several common imported modules (e.g.\ \texttt{Bounded\-Distributive\-Lattice}), but no common importing module, as can be seen from Fig.~\ref{fig:colore-graph}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{figure}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski \begin{center}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \includegraphics[width=.75\textwidth]{colore-subset}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\caption{Boolean algebras and lattices in COLORE (subgraph)}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\label{fig:colore-graph}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiFor use with \Hets, we have made a dump of the COLORE contents available in \texttt{CommonLogic/colore} in the \Hets library \cite{hets-library:URL}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWe first show how to express the relative interpretation using COLORE's CLIF annotations, then how to express it using \HetCASL syntax.\ednote{CL: The latter is not currently part of the \Hets library; should I add it? Maybe as one *.het file in the ``CommonLogic'' directory? That file could then reference the imported ontologies via the ``get *.clif from library'' mechanism. OK? TM: yes}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\paragraph{Common Logic Syntax:}\ednote{CL: TODO fix the second argument of ``relatively-interprets''}~\\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{lstlisting}[language=clif]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(cl:module AtomlessBooleanLattice
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (cl:imports BooleanLattice)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (and (not (= y 0))
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (leq y x)))))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski(cl:module RegionBooleanContactAlgebra
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (cl:imports BooleanContactAlgebra)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (cl:comment '(relatively-interprets ??? AtomlessBooleanLattice)')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if (and (not (= x 0))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (not (= x 1)))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (and (complement x y)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{lstlisting}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\paragraph{\HetCASL Syntax:}~\\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\begin{lstlisting}[language=hetcasl,alsolanguage=clif]
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilogic CommonLogic
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispec AtomlessBooleanLattice =
30256573a343132354b122097b0ee1215dda1364Till Mossakowski BooleanLattice
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (and (not (= y 0))
e683cd5ffcfa43e18a9b3eb7c7aeec32dab50c06Mihai Codescu (leq y x)))))
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskispec RegionBooleanContactAlgebra =
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski BooleanContactAlgebra
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (if (and (not (= x 0))
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (not (= x 1)))
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (and (complement x y)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiview v : AtomlessBooleanLattice to RegionBooleanContactAlgebra
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{lstlisting}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\subsubsection{Relative Interpretation (Standalone Example)}\label{sec:rel-intpr-standalone}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill MossakowskiThis example defines a partial order twice: once as an extension of a strict partial order, and once directly. Then, we connect both definitions by a ``relative interpretation'' link. The sources are available from the \texttt{CommonLogic/Examples} directory in the \Hets library \cite{hets-library:URL}.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\paragraph{Common Logic Syntax:}\ednote{CL: TODO fix the second argument of ``relatively-interprets''}~\\
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{lstlisting}[language=clif]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski(cl:module Partial_Order
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (cl:comment 'reflexive')
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski (forall (x y)
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski (cl:comment 'asymmetric')
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (if (and (le x y)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (forall (x y z)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (cl:comment 'transitive')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if (and (le x y)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski(cl:module Partial_Order_From_Strict_Partial_Order
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (forall (x y)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (cl:comment 'define "less or equal" in terms of "less than"')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (iff (le x y)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(cl:module Partial_Order_From_Strict_Partial_Order
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (cl:comment '(relatively-interprets ??? Partial_Order)')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (forall (x y)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (cl:comment 'define "less or equal" in terms of "less than"')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (iff (le x y)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{lstlisting}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\paragraph{\HetCASL Syntax:}~\\
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski\begin{lstlisting}[language=hetcasl,alsolanguage=clif]
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskilogic CommonLogic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispec Strict_Partial_Order =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski. (forall (x y)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if (and (le x y)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski. (forall (x y z)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if (and (le x y)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskispec Partial_Order_From_Strict_Partial_Order =
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski Strict_Partial_Order
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski. (forall (x y)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (cl:comment 'define "less or equal" in terms of "less than"')
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (iff (le x y)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispec Partial_Order =
30256573a343132354b122097b0ee1215dda1364Till Mossakowski. (forall (x y)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (cl:comment 'define "less or equal" in terms of "less than"')
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (iff (le x y)
b740c481cef85409c373a87756fa394051cb4a37Christian Maederview v : Partial_Order to Partial_Order_From_Strict_Partial_Order
b740c481cef85409c373a87756fa394051cb4a37Christian Maeder\end{lstlisting}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsubsection{Ontology-based Ambient Assisted Living Services and Devices}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\label{sec:aal-example}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% Source: https://svn-agbkb.informatik.uni-bremen.de/sfb-repos/Projects/I1_OntoSpace/standards/OntoIOp/WD_OntoIOp_current.tex
30256573a343132354b122097b0ee1215dda1364Till MossakowskiConsider the following ambient assisted living (AAL) scenario:
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski Clara instructs her \textbf{wheelchair} to get her to the \textbf{kitchen} (\textbf{\underline{next door}} to the \textbf{living room}. For \textbf{dinner}, she would like to take a pizza from the \textbf{freezer} and bake it in the \textbf{oven}. (Her diet is vegetarian.) \textbf{\underline{Afterwards}} she needs to rest in \textbf{bed}.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiExisting ontologies for ambient assisted living (e.g.\ the OpenAAL\footnote{\url{http://openaal.org}} OWL ontology) cover the \emph{core} of these concepts; they provide at least classes (or generic superclasses) corresponding to the concepts highlighted in \textbf{bold}. However, that does not cover the scenario completely. In particular, there are relevant concepts (here: space and time, \underline{underlined}), which are not covered at the required level of complexity. OpenAAL says that appointments have a date and that rooms can be connected to each other, but not what exactly that means. Foundational ontologies and spatial calculi, often formalized in first-order logic, cover space and time at the level of complexity required by a central controller of an apartment and by an autonomously navigating wheelchair.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiMore concretely, Common Logic is useful in this scenario for expressing knowledge on the arrangement of rooms, e.g.\ as follows in a first-order formalization of an RCC-style spatial calculus:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{align*}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski \forall a_1, a_2 .&\mathrm{equal}(a_1, a_2) \veebar \mathrm{overlapping}(a_1, a_2) \veebar \mathrm{bordering}(a_1, a_2) \veebar \mathrm{disconnected}(a_1, a_2) \veebar\\
30256573a343132354b122097b0ee1215dda1364Till Mossakowski &\mathrm{proper\_part\_of}(a_1, a_2) \veebar \mathrm{proper\_part\_of}(a_2, a_1)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(“Two areas in a house (e.g.\ a working area in a room) are either the same, or intersecting, or bordering, or separated, or one is a proper part of the other.”)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe following listing shows a relevant excerpt of the heterogeneous specification, which can be found
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiunder \texttt{Ontology/Examples/AAL.het} in the \Hets library \cite{hets-library:URL}. The key features include:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{itemize}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item Heterogeneous specification allows for reusing the OpenAAL OWL ontology, but at the same time formalizing a first-order spatial calculus.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\item In particular, the compact representation of mutual disjointness chosen here makes use of Common Logic's sequence markers.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item As Common Logic module extends the previously imported OWL ontology, it has access to all entities of the OWL ontology by name; in particular, we can specify that two rooms are connected (in terms of the OpenAAL terminology) if certain conditions in terms of our Common Logic module, or certain conditions in terms of OpenAAL hold.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\begin{lstlisting}[language=HetCASL,basicstyle={\small\ttfamily},alsolanguage=clif,alsoletter={-}]
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifrom Ontology/Examples/OpenAALOntology get OpenAAL
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski %% Import the OpenAAL OWL ontology.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski ... %% some other extensions not shown here
30256573a343132354b122097b0ee1215dda1364Till Mossakowski %% Extend it by an RCC-style spatial calculus
30256573a343132354b122097b0ee1215dda1364Till Mossakowski %% formalized in first order logic.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski then logic CommonLogic : {
30256573a343132354b122097b0ee1215dda1364Till Mossakowski . (forall (a1 a2)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (or (equal a1 a2)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (overlapping a1 a2)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (bordering a1 a2)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (disconnected a1 a2)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (proper_part_of a1 a2)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (proper_part_of a2 a1)))
30256573a343132354b122097b0ee1215dda1364Till Mossakowski %% mutual disjointness of predicates (need this for an exclusive or)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski . (forall (p)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (mutually-disjoint p))
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich . (forall (p q ...)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (iff (mutually-disjoint p q ...)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (and (forall (...x)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (mutually-disjoint p ...)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski (mutually-disjoint q ...))))
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski %% a utility predicate for talking about inverse relations
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder %% (similar to owl:inverseOf)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski . (forall (r x y)
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski (iff ((converse r) x y) (r y x)))
30256573a343132354b122097b0ee1215dda1364Till Mossakowski %% make the above "or" exclusive
30256573a343132354b122097b0ee1215dda1364Till Mossakowski . (mutually-disjoint equal overlapping bordering disconnected
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski proper_part_of (converse proper_part_of))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski %% if some RCC relations hold (so far it would also work in OWL)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski %% or if there is a door that connects two rooms, then ...
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski %% (the latter would only work in OWL if we used an explicit subproperty
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski %% is-door-of of is-in-room; then we could chain "inverse is-door-of"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski %% and "is-door-of", but otherwise we wouldn't be able to restrict the
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder %% "connecting element" to a Door)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski . (forall (a1 a2)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (if (or (equal a1 a2)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (overlapping a1 a2)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (proper_part_of a1 a2)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (proper_part_of a2 a1)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (exists (door)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (and (Door door)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder (is-in-room door a1)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (is-in-room door a2)))
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (is-connected-to-room a1 a2)))
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{lstlisting}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\subsubsection{Heterogeneous Views from OWL to Common Logic}
b740c481cef85409c373a87756fa394051cb4a37Christian Maeder\label{sec:heter-views-from}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn the previous example, we established a link between an OWL ontology and a Common Logic ontology by reusing elements of the signature of the OWL ontology (concretely: OpenAAL's \texttt{is-in-room} predicate) in the Common Logic ontology.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\HetCASL's view mechanism offers an alternative to that. A view from one ontology to another ontology in the same logic has been shown in Sect.~\ref{sec:relat-interpr}, but it is also possible to have views across logics, as long as there is a translation between these logics that is known to \Hets (cf.\ Sect.~\ref{comorphisms}).
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe following example establishes a view between the OWL Time ontology and its reimplementation in Common Logic, \ednote{CL: There is no way to make that explicit in \HetCASL, is there? TM: you mean the datatype stuff that the OWL to CL translation generates? We should modify the translation to generate this only if really needed.}using the ``OWL22CommonLogic'' translation:\ednote{CL: I will also put this into the \Hets library}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski% The following doesn't work, as in CLIF ":" is part of keywords, whereas in OWL Manchester it is not.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski%% \begin{lstlisting}[language=hetcasl,alsolanguage=clif,alsolanguage=owl2Manchester]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich% Therefore we specify the relevant keywords manually:
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{lstlisting}[language=hetcasl,morekeywords={Class,ObjectProperty,Domain,Range,Characteristics,Transitive,forall,if,and,or}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichspec TimeOWL =
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich Class: TemporalEntity
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich ObjectProperty: before
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich Domain: TemporalEntity
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski Range: TemporalEntity
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski Characteristics: Transitive
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskilogic CommonLogic
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski%% CommonLogic equivalent of Domain and Range above
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich. (forall (t1 t2)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (if (before t1 t2)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (and (TemporalEntity t1)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (TemporalEntity t2))))
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich%% CommonLogic equivalent of Transitive above
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich. (forall (t1 t2 t3)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (if (and (before t1 t2)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (before t2 t3))
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (before t1 t3)))
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich%% A new axiom that cannot be expressed in OWL
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich. (forall (t1 t2)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (or (before t1 t2)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (before t2 t1)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiview TimeOWLtoCL : TimeOWL to TimeCL
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\end{lstlisting}
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich\section{Proofs with \Hets}\label{sec:Proofs}
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe proof calculus for development graphs (Sect.~\ref{sec:DevGraph}) reduces
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiglobal theorem links to local proof goals. You can do this reduction by clicking
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskion the Edit-menu in the development graph window and selecting
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiProofs/Auto-DG-Prover. Local proof goals (indicated by red
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskinodes in the development graph) can be eventually discharged using a theorem
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowskiprover, i.e.\ by using the ``Prove'' menu of a red node.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe graphical user interface (GUI) for calling a prover is shown in
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiFig.~\ref{fig:proof_window} --- we call it ``Proof Management GUI''.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe top list on the left shows all goal names prefixed with their proof
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichstatus in square brackets. A proved goal is indicated by a `+', a `–'
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichindicates a disproved goal, a space denotes an open goal, and a
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich`$\times$' denotes an inconsistent specification (aka a fallen `+';
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichsee below for details).
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{figure}[ht]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \includegraphics[width=0.5\linewidth,keepaspectratio=true]{UserGuideCL_Prove_devGraph}
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke \caption{Prove local proof obligation\label{fig:Prove_devGraph}}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}[ht]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{minipage}[b]{0.5\linewidth}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Prove_Prove}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \caption{\Hets Goal and Prover Interface\label{fig:proof_window}}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{minipage}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\hspace{0.1\linewidth}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{minipage}[b]{0.5\linewidth}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Prove_Vampire}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \caption{Interface of Vampire Prover\label{fig:Vampire}}
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski\end{minipage}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIf you open this GUI when processing the goals of one node for the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichfirst time, it will show all goals as open. Within this list you can
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichselect those goals that should be inspected or proved. The GUI elements are the following:
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{itemize}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item The button `Display' shows the selected goals in the ASCII syntax of
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich this theory's logic in a separate window.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item By pressing the `Proof details' button a window is opened where for each
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich proved goal the used axioms, its proof script, and its proof are shown ---
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich the level of detail depends on the used theorem prover.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item With the `Prove' button the actual prover is launched. The provers are described
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich in more detail in the \Hets user guide \cite{HetsUserGuide}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item The list `Pick Theorem Prover:' lets you choose one of the connected
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich provers (among them \Isabelle, MathServe Broker, \SPASS, Vampire, and
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich zChaff, described below). By pressing `Prove' the selected prover is
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich launched and the theory along with the selected goals is translated via the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich shortest possible path of comorphisms into the prover's logic.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item The pop-up choice box below `Selected comorphism path:' lets you pick a
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (composed) comorphism to be used for the chosen prover. If the specification
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich does not contain any sequence markers, it is possible to use the comorphism
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \texttt{CommonLogic2CASLCompact} which results in a simpler
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \CASL specification. We recommend using this comorphism whenever possible.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item Since the amount and kind of sentences sent to an ATP system is a major
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich factor for the performance of the ATP system, it is possible to select in
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich the bottom lists the axioms and proven theorems that will comprise the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich theory of the next proof attempt. Based on this selection the sublogic may
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich vary and so do the available provers and the comorphism paths leading to provers. Former
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich theorems that are imported from other specifications are marked with the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich prefix `(Th)'. Since former theorems do not add additional logical content,
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich they may be safely removed from the theory.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item If you press the bottom-right `Close' button the window is closed and
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich the status of the goals' list is integrated into the development graph. If
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich all goals have been proved, the selected node turns from red into green.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\item All other buttons control selecting list entries.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIn order to prove or disprove a theorem, it needs to be declared as proof
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichobligation. This is done by the keyword \texttt{\%implied} at the end of a text:
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{lstlisting}[language=hetcasl,alsolanguage=clif]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichlogic CommonLogic
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichspec ToProve =
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich (and (P x) (Q y))
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich. (Q y) %implied %(correct)%
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich. (P y) %implied %(incorrect)%
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{lstlisting}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIn this specification the theorems, annotated (named) by \texttt{correct} and
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\texttt{incorrect} are the ones, that can be proven or disproven.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichNote that they are separate texts inside the specification \texttt{ToProve}.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe annotations are optional. For proving, they are the names shown in the
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich``Axioms to include'' section of the prover interface
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich(Fig.~\ref{fig:proof_window}).
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe same specification can be written down in CLIF:
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{lstlisting}[language=clif,morekeywords={implied}]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich(cl:text axiom
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski (and (P x) (Q y))
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich(cl:text correct
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich(cl:text incorrect (P y)) %implied
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{lstlisting}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichIn CLIF, there is no notion of proof obligation. Hence the \texttt{\%implied}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichkeyword of \Hets must be used, and thus the specification is not pure CLIF. Because the texts have
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichnames, these are also used in the prover interface. Otherwise, \Hets invents
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\subsection{Consistency Checker}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\label{sec:CC}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichSince proofs are void if specifications are inconsistent, the consistency
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichshould be checked (if possible for the given logic) by the ``Consistency
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichchecker'' shown in Fig.~\ref{fig:cons_window}. This GUI is invoked from
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichthe `Edit' menu as it operates on all nodes.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichThe list on the left shows all node names prefixed with a consistency status
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederin square brackets that is initially empty. A consistent node is indicated by
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luetticha `+', a `–' indicates an inconsistent node, a `t' denotes a timeout of the last
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichchecking attempt.
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{figure}[ht]
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\begin{minipage}[b]{0.5\linewidth}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Consistency_devGraph}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \caption{Selection of consistency checker\label{fig:cons_devGraph}}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\end{minipage}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich\hspace{0.1\linewidth}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{minipage}[b]{0.5\linewidth}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Consistency_Interface}
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich \caption{\Hets Consistency Checker Interface\label{fig:cons_window}}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\end{minipage}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiFor some selection of nodes (of a common logic) a model finder should be
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederselectable from the `Pick Model finder:' list. Currently only for ``darwin''
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskisome \CASL models can be re-constructed. When pressing `Check', possibly after
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski`Select comorphism path:', all selected nodes will be checked, spending at
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maedermost the number of seconds given under `Timeout:' on each node. Pressing
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski`Stop' allows to terminate this process if too many nodes have been chosen.
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiEither by `View results' or automatically the `Results of consistency check'
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski(Fig.~\ref{fig:cons_res}) will pop up and allow you to inspect the models for
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskinodes, if they could be constructed.
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}[ht]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \includegraphics[width=0.75\linewidth,keepaspectratio=true]{UserGuideCL_Consistency_Result}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski \caption{Consistency checker results\label{fig:cons_res}}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\subsection[Automated Theorem Proving Systems]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski{Automated Theorem Proving Systems\\(Logic SoftFOL)}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\label{sec:ATP}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\begin{figure}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\includegraphics[width=\textwidth]{spassGUI1}
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski\caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiAll ATPs integrated into \Hets share the same GUI, with only a slight
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskimodification for the MathServe Broker: the input field for extra options is
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiinactive. Fig.~\ref{fig:SPASS_GUI} shows the instantiation for \SPASS, where
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskiin the top right part of the window the batch mode can be controlled. The
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskileft side shows the list of goals (with status indicators). If goals are
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskitimed out (indicated by `t') it may help to activate the check box `Include
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskipreceding proven theorems in next proof attempt' and pressing `Prove all'
53eb610e03705ac6499371cde16cc37482fb3313Till MossakowskiOn the bottom right the result of the last proof
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederattempt is displayed. The `Status:' indicates `Open', `Proved', `Disproved',
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski`Open (Time is up!)', or `Proved (Theory inconsistent!)'. The list of `Used
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiAxioms:' is filled by \SPASS. The button `Show Details' shows the whole output
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiof the ATP system. The `Save' buttons allow you to save the input and
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiconfiguration of each proof for documentation. By `Close' the results for all
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskigoals are transferred back to the Proof Management GUI.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiThe MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiZimmer provides a unified interface to a range of different ATP
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskisystems; the most important systems are listed in
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiTab.~\ref{tab:MathServe}, along with their capabilities. These
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskicapabilities are derived from the \emph{Specialist Problem Classes}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski(SPCs) defined upon the basis of logical, language and syntactical
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiproperties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiOnly two of the Web services provided by the MathServe system are used
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiby \Hets currently: Vampire and the brokering system. The ATP systems
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiare offered as Web Services using standardised protocols and formats
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskisuch as SOAP, HTTP and XML. Currently, the ATP system Vampire may be
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiaccessed from \Hets via MathServe; the other systems are only reached
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskiafter brokering.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\begin{table}[t]
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \begin{threeparttable}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \begin{tabular}{|l|c|p{7cm}|}\firsthline
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke ATP System & Version & Suitable Problem Classes\tnote{a}\\
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke \hhline{|=|=|=|}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder DCTP & 10.21p & effectively propositional \\\hline
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke EP & 0.91 & effectively propositional; real first-order, no
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder equality; real first-order, equality\\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder Otter & 3.3 & real first-order, no equality\\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \SPASS & 2.2 & effectively propositional; real first-order, no
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke equality; real first-order, equality\\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder Vampire & 8.0 & effectively propositional; pure equality, equality
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke clauses contain non-unit equality clauses; real first-order, no
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke equality, non-Horn\\\hline
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder Waldmeister & 704 & pure equality, equality clauses are unit
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder equality clauses\\\lasthline
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke \end{tabular}
f8a33e72909e67885a9ecbae881fc75134c362cbDominik Luecke %\renewcommand{\thempfootnote}{\arabic{mpfootnote}}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski %\footnotetext%[\value{footnote}\stepcounter{footnote}]
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \begin{tablenotes}\footnotesize
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski {The list of problem classes for each ATP system is not
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski exhaustive, but only the most appropriate problem classes are
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski named according to benchmark tests made with MathServe by
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski J\"urgen Zimmer.}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \end{tablenotes}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \end{threeparttable}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \caption{ATP systems provided as Web services by MathServe}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\vspace*{-4mm}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski \label{tab:MathServe}
c9d53cd78829e538aee56b84db508d8d944e6551Till MossakowskiFor details on the ATPs supported, see the \Hets user guide \cite{HetsUserGuide}.
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\section{Reading, Writing and Formatting}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski\Hets provides several options controlling the types of files
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskithat are read and written.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{description}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\item[\texttt{-i ITYPE}, \texttt{-{}-input-type=ITYPE}] Specify \texttt{ITYPE}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski as explicit type of the input file.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski \texttt{exp} files contain a development graph in a new experimental OMDoc
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski format. \texttt{prf} files contain additional development steps (as shared
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski ATerms) to be applied on top of an underlying development graph created from
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski a corresponding \texttt{env}, \texttt{casl}, or \texttt{het}
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski file. \texttt{hpf} files are plain text files representing heterogeneous
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski proof scripts. The contents of a \texttt{hpf} file must be valid input for
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski \Hets in interactive mode. (\texttt{gen\_trm} formats are currently not
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe possible input types are:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | [tree.]gen_trm[.baf]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{lstlisting}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\texttt{-O DIR}, \texttt{-{}-output-dir=DIR}]
30256573a343132354b122097b0ee1215dda1364Till MossakowskiSpecify \texttt{DIR} as destination directory for output files.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\item[\texttt{-o OTYPES}, \texttt{-{}-output-types=OTYPES}]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{OTYPES} is a comma-separated list of output types:
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\begin{lstlisting}
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | (sig|th)[.delta]
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder | pp.(het|tex|xml|html)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{lstlisting}
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{env} and \texttt{prf} formats are for subsequent reading,
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maederavoiding the need to re-analyse downloaded libraries. \texttt{prf} files
30256573a343132354b122097b0ee1215dda1364Till Mossakowskican also be stored or loaded via the GUI's File menu.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{omn} option \cite{w3c:owl2-manchester} will produce OWL files in
30256573a343132354b122097b0ee1215dda1364Till MossakowskiManchester Syntax for each specification of a structured OWL library.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{clif} option will produce Common Logic files in
30256573a343132354b122097b0ee1215dda1364Till MossakowskiCLIF dialect for each specification of a Common Logic library.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
30256573a343132354b122097b0ee1215dda1364Till Mossakowskimarkup format and data model for Open Mathematical Documents. It
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiserves as semantics-oriented representation format and ontology
30256573a343132354b122097b0ee1215dda1364Till Mossakowskilanguage for mathematical knowledge. Although this is still in experimental
30256573a343132354b122097b0ee1215dda1364Till Mossakowskistate, Common Logic theories can be exported to and imported from OMDoc.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{xml} option will produce an XML-version of the development graph
30256573a343132354b122097b0ee1215dda1364Till Mossakowskifor our change management broker.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{exp} format is the new experimental omdoc format.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{hs} format is used for Haskell modules. Executable \CASL or
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\HasCASL specifications can be translated to Haskell.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiWhen the \texttt{thy} format is selected, \Hets will try to translate
30256573a343132354b122097b0ee1215dda1364Till Mossakowskieach specification in the library to \Isabelle, and write one \Isabelle
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\texttt{.thy} file per specification.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiWhen the \texttt{comptable.xml} format is selected, \Hets will extract
30256573a343132354b122097b0ee1215dda1364Till Mossakowskithe composition and inverse table of a Tarskian relation algebra from
30256573a343132354b122097b0ee1215dda1364Till Mossakowskispecification(s) (selected with the \texttt{-n} or \texttt{-{}-spec}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskioption). It is assumed that the relation algebra is
30256573a343132354b122097b0ee1215dda1364Till Mossakowskigenerated by basic relations, and that the specification is written
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiin the \CASL logic. A sample specification of a relation
30256573a343132354b122097b0ee1215dda1364Till Mossakowskialgebra can be found under \texttt{Calculi/Space/RCC8.het} in the \Hets library \cite{hets-library:URL}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe output format is XML, the URL of the DTD is included in the
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{sig} or \texttt{th} option will create \HetCASL signature or
30256573a343132354b122097b0ee1215dda1364Till Mossakowskitheory files for each development graph node. (The \texttt{.delta} extension
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiis not yet supported.)
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{pp} format is for pretty printing, either as plain text
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(\texttt{het}), \LaTeX\ input (\texttt{tex}), HTML (\texttt{html}) or XML
30256573a343132354b122097b0ee1215dda1364Till Mossakowski(\texttt{xml}). For example, it is possible to generate a pretty printed
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\LaTeX\ version of \texttt{Cat.clif} by typing:
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThis will generate a file \texttt{Cat.pp.tex}. It can be included
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinto \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicoming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiThe format \texttt{pp.xml} represents just a parsed library in XML.
3532dcfda4dd76997072fcda24e75c305d105233Till MossakowskiFormats with \texttt{graph} are reserved for future usage.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{dfg} format is used by the \SPASS theorem prover
30256573a343132354b122097b0ee1215dda1364Till Mossakowski\cite{WeidenbachEtAl02}.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiThe \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiexchange format for first-order theorem provers.
30256573a343132354b122097b0ee1215dda1364Till MossakowskiAppending \texttt{.c} to \texttt{dfg} or \texttt{tptp} will create files for
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiconsistency checks by SPASS or Darwin respectively.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiFor all output formats it is recommended to increase the verbosity to at least
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskilevel 2 (by using the option \texttt{-v2}) to get feedback which files are
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiactually written. (\texttt{-v2} also shows which files are read.)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[\texttt{-t TRANS}, \texttt{-{}-translation=TRANS}]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskichooses a translation option. \texttt{TRANS} is a colon-separated list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwithout blanks of one or more comorphism names (see Sect.~\ref{comorphisms})
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-n SPECS}, \texttt{-{}-spec=SPECS}]
30256573a343132354b122097b0ee1215dda1364Till Mossakowskichooses a list of named specifications for processing
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-w NVIEWS}, \texttt{-{}-view=NVIEWS}]
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskichooses a list of named views for processing
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[\texttt{-R}, \texttt{-{}-recursive}] output also imported libraries
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[\texttt{-I}, \texttt{-{}-interactive}] run \Hets in interactive mode
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[\texttt{-X}, \texttt{-{}-server}] run \Hets as web server (see
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Sect.~\ref{sec:Server})
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-x}, \texttt{-{}-xml}] use XML-PGIP\footnote{Proof General Interface Protocol} packets to communicate with
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski \Hets in interactive mode
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski\item[\texttt{-S PORT}, \texttt{-{}-listen=PORT}] communicate
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski with \Hets in interactive mode by listening to the port \texttt{PORT}
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski\item[\texttt{-c HOSTNAME:PORT}, \texttt{-{}-connect=HOSTNAME:PORT}] communicate
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski with \Hets in interactive mode via connecting to the port on host
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski \texttt{HOSTNAME}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-d STRING}, \texttt{-{}-dump=STRING}] produces implementation
30256573a343132354b122097b0ee1215dda1364Till Mossakowski dependent output for debugging purposes only
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (i.e.\ \texttt{-d LogicGraph} lists the logics and comorphisms)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\end{description}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\section{Hets as a web server}\label{sec:Server}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiLarge parts of \Hets are now also available via a web interface. A running
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiserver should be accessible on
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\url{http://pollux.informatik.uni-bremen.de:8000/}. It allows to browse the
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\Hets library, upload a file or just a \HetCASL specification. Development
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskigraphs for well-formed specifications can be displayed in various formats
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiwhere the \texttt{svg} format is supposed to look like the graphs displayed by
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiuDrawGraph. Besides browsing, the web server is supposed to be accessed by
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiother programs using queries. The possible queries are described at
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\url{http://trac.informatik.uni-bremen.de:8080/hets/wiki/RESTfulInterface}.
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till MossakowskiFor details on this topic, see the \Hets user guide \cite{HetsUserGuide}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Miscellaneous Options}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\begin{description}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[\texttt{-v[Int]}, \texttt{-{}-verbose[=Int]}]
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiSet the verbosity level according to \texttt{Int}. Default is 1.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-q}, \texttt{-{}-quiet}]
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiBe quiet -- no diagnostic output at all. Overrides -v.
2ef350ad6e8df3c2c1d76bb6a9dca42a267b3eb1Till Mossakowski\item[\texttt{-V}, \texttt{-{}-version}] Print version number and exit.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[\texttt{-h}, \texttt{-{}-help}, \texttt{-{}-usage}]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiPrint usage information and exit.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder \texttt{Int} megabytes (needed in case of a stack overflow).
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiThis must be the first option.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[\texttt{-l LOGIC}, \texttt{-{}-logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskideclaration. The default is \CASL.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski\item[\texttt{-e ENCODING}, \texttt{-{}-encoding=ENCODING}] Read input files using latin1 or utf8 encoding. The default is still latin1.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-{}-unlit}] Read literate input files.
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-{}-relative-positions}] Just uses the relative library name in positions of warning or errors.
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\item[\texttt{-U FILE}, \texttt{-{}-xupdate=FILE}] update a development graph according to special XML update information (still experimental).
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\item[\texttt{-m FILE}, \texttt{-{}-modelSparQ=FILE}] model check a qualitative calculus given in SparQ lisp notation \cite{SparQ06} against a \CASL specification
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\end{description}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder\bibliographystyle{plain}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\bibliography{cofibib,cofi-ann,UM,hets,kl,hetsForCL}
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski\end{document}
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder%%% Local Variables:
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski%%% mode: latex
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski%%% TeX-master: "UserGuideCommonLogic"
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski%%% ispell-local-dictionary: "british"
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% LocalWords: SPASS darwin uninger Hets HetCASL SoftFOL EL QL RL zChaff TPTP
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% LocalWords: Eprover KRHyper MathServe CASL THF HasCASL RelScheme CommonLogic
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% LocalWords: CASLCompact CommonLogicModuleElimination SuleCFOL hets oneiric
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski% LocalWords: SoftFOLInduction mpkg MacPorts libglade uDraw Tcl Tk bunzip VSE
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder% LocalWords: minisat Twelf Attr clif libdir casl het clf Pred PetHappy gui DG
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski% LocalWords: uncolored COLORE someFile http https someText someTargetFile sp
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder% LocalWords: someTranslationFile someAxiom Nonconservative nonconservative EP
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% LocalWords: libs someOtherFile nextFile andSoOn nameInTargetFile forall iff
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder% LocalWords: nameInCurrentFile ToProve ATPs rgen Zimmer SPCs Sutcliffe DCTP
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% LocalWords: Suttner Waldmeister urgen ITYPE OMDoc prf ATerms env hpf trm hs
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% LocalWords: maude hol omdoc xml baf dir OTYPES omn comptable sig th tex html
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski% LocalWords: dfg tptp Tarskian hetcasl NVIEWS pgip HOSTNAME LogicGraph svg
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% LocalWords: uDrawGraph RTS KIntM latin utf xupdate modelSparQ SparQ cofibib
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski% LocalWords: cofi ann hetsForCL Mossakowski Maeder Mihai Codescu
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski% LocalWords: Kuksa DFKI GmbH IEC lang basicstyle morecomment
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski% LocalWords: escapeinside importedSpec importingSpec