UserGuideCommonLogic.tex revision 2fd0eb33dd1d635a91e5b1a790e194ceaccae489
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\documentclass{article}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\setlength{\textwidth}{16cm}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\setlength{\topmargin}{-1cm}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\setlength{\evensidemargin}{0cm}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\setlength{\oddsidemargin}{0cm}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\setlength{\textheight}{22.5cm}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage[utf8]{inputenc}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage[T1]{fontenc}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{charter} % very clean and readable font
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{courier}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\usepackage{unicode-chars}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage[show]{ed} % set to hide for producing a released version
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{alltt}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{casl}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{color}
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroeder\usepackage{url}
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroeder\usepackage{threeparttable,hhline}
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder\usepackage{tabularx}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{paralist}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage{listings}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\lstset{basicstyle=\ttfamily,columns=fixed}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\usepackage[pdfborder=0 0 0,bookmarks,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederpdfauthor={Till Mossakowski, Christian Maeder, Mihai Codescu, Eugen Kuksa, Christoph Lange},
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederpdftitle={Hets for Common Logic Users}]
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder{hyperref} %% do not load more packages after this line!!
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\QUERY}[1]%{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\eat}[1]{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\IEXT}[1] {\\#1\I}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\IEND} {\I\END}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{EXAMPLEFORMAT} {}{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% Added by MB to have some extra vertical space after the ``main'' examples
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% following the points (and some others in the text):
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{DETAILSFORMAT} {}{}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \begin{minipage}{0.9\textwidth}\it}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder {\end{minipage}\par\medskip}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\SLIDESMALL} {}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\SLIDESONLY}[1] {}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder% SIMULATING SMALL-CAPS FOR BOLD, EMPH
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder%\newcommand {\CoFI}{CoFI\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%%%%% Klaus macros
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\SROIQ}{$\mathcal{SROIQ}$(\textbf{D})\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\DL}{DL\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%%%%% end of Klaus macros
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\LCF}{LCF\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\newcommand{\ASF}{ASF\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\SDF}{SDF\xspace}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\CCC}{CCC\xspace}
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\begin{document}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\title{{\bf \protect{\LARGEHets} for Common Logic Users}\\
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder-- Version 0.99 --}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\author{Till Mossakowski, Christian Maeder,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder Mihai Codescu, Eugen Kuksa, Christoph Lange\\[1em]
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDFKI GmbH, Bremen, Germany.\\[1em]
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederComments to: \href{mailto:hets-users@informatik.uni-bremen.de}{hets-users@informatik.uni-bremen.de} \\
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder(the latter needs subscription to the mailing list)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\setcounter{tocdepth}{1}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\tableofcontents
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Introduction}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederCommon Logic (CL) is an ISO standard published as ``ISO/IEC 24707:2007
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder--- Information technology — Common Logic (CL): a framework for a family
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederof logic-based languages'' \cite{CommonLogic:oldfashioned}. CL is based on untyped first-order
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederlogic, but extends first-order logic in two ways: \begin{inparaenum}[(1)]\item any term can be
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederused as function or predicate, and \item sequence markers allow
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederfor talking about sequences of individuals directly\end{inparaenum}.\footnote
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder{Strictly speaking, only the second feature goes beyond first-order
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe Heterogeneous Tool Set (\Hets) is an open source software providing
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederseveral kinds of tool support for Common Logic:
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\item a parser for the Common Logic Interchange Format (CLIF) --- CLIF
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder is a Lisp-like syntax for CL;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item a connection of CL to well-known first-order theorem provers
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlike SPASS, darwin and Vampire, such that logical consequences
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederof CL theories can be proved;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item a connection of CL to the higher-order provers Isabelle/HOL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederand Leo-II in order to perform induction proofs in theories
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinvolving sequence markers;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item a connection to first-order model finders like darwin that
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederallow one to find models for CL theories;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item support for proving interpretations between CL theories to be correct;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item a translation that eliminates the use of CL modules\footnote{Actually, we are using a revised semantics for modules, as proposed
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederrecently in~\cite{NH:CommonLogicHoratio}.}. Since the semantics of CL modules
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederis special to CL, this elimination of modules is necessary before
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersending CL theories to a standard first-order prover;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item a translation of the Web Ontology Language OWL to CL;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item a translation of propositional logic to CL.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThis guide will introduce you to these functionalities of \Hets.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFor the full functionalities of \Hets, see the \Hets user guide
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\cite{HetsUserGuide}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{The Heterogeneous Tool Set and Its Input Languages}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe central idea of the Heterogeneous Tool Set (\protect\Hets) is to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederprovide a general framework for formal methods integration and proof
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedermanagement. One can think of \Hets acting like a motherboard where
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdifferent expansion cards can be plugged in, the expansion cards here
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederbeing individual logics (with their analysis and proof tools) as well
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederas logic translations. The \Hets motherboard already has plugged in
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedera number of expansion cards (e.g., the theorem provers Isabelle, SPASS
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederand more, as well as model finders). Hence, a variety of tools is
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederavailable, without the need to hard-wire each tool to the logic at
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder \includegraphics[width=0.45\textwidth]{hets-motherboard}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\caption{The \Hets motherboard and some expansion cards}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Hets consists of logic-specific tools for the parsing and static
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederanalysis of the different involved logics, as well as a
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederlogic-independent parsing and static analysis tool for structured and
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederarchitectural specifications and libraries. The latter of course needs
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederto call the logic-specific tools whenever a basic specification is
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Hets is based on the theory of institutions \cite{GoguenBurstall92},
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederwhich formalise the notion of a logic. The theory behind \Hets is laid
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederout in \cite{Habil}. A short overview of \Hets is given in
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\cite{MossakowskiEA06,MossakowskiEtAl07b}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\Hets supports a number of input languages directly, such as Common
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederLogic and OWL2 and \HetCASL. They will be described in the next
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\subsection{Common Logic and the Common Logic Interchange Format (CLIF)}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederCLIF is specified in Annex A of the Common Logic standard
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\cite{CommonLogic:oldfashioned}. \Hets can directly read in files in
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederCLIF syntax, and also recursively reads in any imported files (cf.\ Sect.~\ref{relationsInCL} for the syntax).
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederCommon Logic itself does not support the specification of logical
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederconsequences, nor relative theory interpretations, nor other
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederfeatures that speak about structuring and comparing logical
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertheories. Michael Gr\"uninger has suggested certain special annotations comments for
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederthis purpose, which are supported by \Hets, see
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederSect.~\ref{relationsInCL}. Alternatively, CLIF syntax can be used
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederfor specifications within \HetCASL files, or CLIF files can be referred to within \HetCASL
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederfiles. \HetCASL is a structuring language supporting relative theory
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederinterpretations and other things, see Sect.~\ref{HetCASL} below.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\subsection{OWL2}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederOWL2 is a W3C standard \cite{w3c:owl2-overview}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\Hets can directly read in OWL2 files in all syntaxes (called ``serialisations'') that the OWL API supports \cite{OWLAPI:URL}, including
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederthe native OWL XML syntax \cite{w3c:owl2-xml}, the human-readable
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederManchester 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}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSince OWL2 does not support relative theory interpretations and other
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederstructuring features, such things can only be expressed in \HetCASL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederfiles. For this purpose, OWL2 Manchester syntax can be used within
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\HetCASL files, or OWL2 files can be referred to within \HetCASL files.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\subsection{HetCASL}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFor heterogeneous specification, \Hets offers the Heterogeneous
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlanguage \HetCASL. \HetCASL is not so much a logic, but a meta
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlanguage that can express relations of theories written in different
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlogics, like logical consequences, relative interpretations of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertheories, conservative extensions, translations of theories
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederalong logic translations, etc.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \HetCASL generalises the structuring
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CASL (Common Algebraic Specification Language \cite{CASL-UM,CASL/RefManual}) to arbitrary logics
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(if they are formalised as institutions and plugged into
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe \Hets motherboard), as well as to heterogeneous
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercombinations of specifications written in different logics.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFig.~\ref{fig:lang} for a simple subset of the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\HetCASL syntax, where \emph{basic specifications} are unstructured
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederspecifications or modules written in a specific logic. The graph of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercurrently supported logics and logic translations (the latter are also
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercalled comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederdegree of support by \Hets in Fig.~\ref{fig:Languages}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder% We give an ad hoc listing language definition of EBNF here. This should probably go into lstlang0.sty.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\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={<>}]
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSPEC ::= BASIC-SPEC %% logic-specific syntax, e.g. CLIF or Manchester syntax
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | SPEC then SPEC %% extension of a spec with new symbols and axioms
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | SPEC then %implies SPEC %% annotation: extension is logically implied
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | SPEC with SYMBOL-MAP %% renaming of SPEC along SYMBOL-MAP
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | SPEC with logic ID %% translation of SPEC to a different logic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDEFINITION ::= logic ID %% select a new logic for subsequent items
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | spec ID = SPEC end %% give the name ID to SPEC
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | view ID : SPEC to SPEC = SYMBOL-MAP end
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder %% interpretation of theories
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder | view ID : SPEC to SPEC = logic ID end
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder %% dto., but across different logics
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederLIBRARY = DEFINITION*
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\end{lstlisting}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederWith \emph{heterogeneous structured specifications}, it is possible to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedercombine and rename specifications, hide parts thereof, and also
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedertranslate them to other logics. \emph{Architectural specifications}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederprescribe the structure of implementations. \emph{Specification
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder libraries} are collections of named structured and architectural
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederspecifications. \emph{Refinements} express the fact the a specification
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederis becoming more specific. All this is supported by \HetCASL.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFor details, see \cite{Mossakowski04,Habil,CASL/RefManual}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Logics supported by Hets}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Hets supports a variety of different logics. The following are most important for use with Common Logic:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \includegraphics[width=.67\textwidth]{LogicGraph-CL}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\caption{Graph of logics related to Common Logic that are currently supported by \Hets. The more an
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederellipse is filled with green, the more stable is the implementation of the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlogic. Blue indicates a prover-supported logic.}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\label{fig:LogicGraph}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|c|c|c|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederLanguage & Parser & Static Analysis & Prover \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\CASL & x & x & -- \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCommon Logic & x (CLIF) & x & -- \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederOWL2 & x & x & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederPropositional & x & x & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederSoftFOL & x & -- & x \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\caption{Current degree of \Hets support for some of the languages.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederLanguages without prover can still ``borrow'' provers
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedervia logic translations.\label{fig:Languages}}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{description}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\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
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlogic in several ways. The Common Logic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Interchange Format (CLIF) provides a Lisp-like syntax for Common
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Logic. \Hets currently only supports parsing CLIF. If you need
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder other dialects, send us a message and we will add them.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[OWL2] is the Web Ontology Language recommended by the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder World Wide Web Consortium (W3C, \url{http://www.w3c.org}); see \cite{w3c:owl2-overview}. It is
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder used for knowledge representation on the Semantic Web
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \cite{berners:2001:SWeb}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHets calls an external OWL2 parser
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder written in Java to obtain the abstract syntax for an OWL file and its
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder imports. The Java parser also does a first analysis classifying
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder 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}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder Hets supports all except OWL Full.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder structuring of the OWL imports is displayed as a Development Graph.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[Propositional] is classical propositional logic, with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederthe zChaff SAT solver \cite{Herbstritt03} connected to it.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[SoftFOL] \cite{LuettichEA06a} offers several automated theorem
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder proving (ATP) systems for first-order logic with equality: \begin{inparaenum}[(1)]\item \SPASS
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \cite{WeidenbachEtAl02}, see \url{http://www.spass-prover.org};
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item Vampire \cite{RiazanovV02} see \url{http://www.vprover.org};
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item Eprover \cite{Schulz:AICOM-2002}, see \url{http://www.eprover.org};
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item E-KRHyper \cite{DBLP:conf/cade/PelzerW07}, see \url{http://www.uni-koblenz.de/~bpelzer/ekrhyper}, and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder MathServe Broker\footnote{which chooses an appropriate ATP upon a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder classification of the FOL problem} \cite{ZimmerAutexier06}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\end{inparaenum}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder These together comprise some of the most advanced theorem provers
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder for first-order logic. SoftFOL is essentially the first-order
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder interchange language TPTP \cite{DBLP:conf/lpar/Sutcliffe10},
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[CASL] extends many sorted first-order logic with partial
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder functions and subsorting. It also provides induction sentences,
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder expressing the (free) generation of datatypes.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFor Common Logic, \CASL can be seen as kind of transitional hub, linking
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederCommon Logic to other logics, most importantly SoftFOL.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[\Isabelle] \cite{NipPauWen02} is the logic of the interactive
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder theorem prover Isabelle for higher-order logic.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[THF] is an interchange language for higher-order logic
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \cite{DBLP:conf/cade/BenzmullerRS08}, similar to what TPTP
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder is for first-order logic. \Hets connects THF to the automated
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder higher-order prover Leo-II.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[HasCASL] is a higher order extension of \CASL allowing
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder polymorphic datatypes and functions. It is closely related to the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder programming language Haskell and allows program constructs being
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder embedded in the specification. For Common Logic, \HasCASL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder is mainly interesting as a transitional hub for paths
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder to the provers Isabelle and Leo-II.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item[RelScheme] is a logic for relational databases \cite{DBLP:journals/ao/SchorlemmerK08}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\end{description}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederVarious logics are supported with proof tools. Proof support for the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederother logics can be obtained by using logic translations to a
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederprover-supported logic. For Common Logic, the paths to SoftFOL
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederare particularly interesting, because this offers an interface
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederto standard first-order provers. Moreover, the paths to THF
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederand Isabelle offer interfaces to higher-order provers, which
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederis essential if you want to prove inductive theorems about
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederAn introduction to \CASL can be found in the \CASL User Manual
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\cite{CASL-UM}; the detailed language reference is given in
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederthe \CASL Reference Manual \cite{CASL/RefManual}. These documents
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederexplain both the \CASL logic and language of basic specifications as
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederwell as the logic-independent constructs for structured and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederarchitectural specifications. The corresponding document explaining the
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder\HetCASL language constructs for \emph{heterogeneous} structured specifications
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroederis the \HetCASL language summary \cite{Mossakowski04}; a formal
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroedersemantics as well as a user manual with more examples are in preparation.
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von SchroederSome of \HetCASL's heterogeneous constructs will be illustrated
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroederin Sect.~\ref{sec:HetSpec} below.\\
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederFor further information on logics supported by \Hets, see the \Hets user guide
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\cite{HetsUserGuide}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\section{Logic translations supported by Hets}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\label{comorphisms}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederLogic translations (formalised as institution comorphisms
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\cite{GoguenRosu02}) translate from a given source logic to a given
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedertarget logic. More precisely, one and the same logic translation
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedermay have several source and target \emph{sub}logics: for
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroedereach source sublogic, the corresponding sublogic of the target
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederlogic is indicated.
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederIn more detail, the following list of logic translations involving Common Logic
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederis currently supported by \Hets:\\
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder\noindent\begin{tabularx}{\textwidth}{|l|X|}\hline
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederCommonLogic2CASL & Coding Common Logic to \CASL. Module elimination
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder is applied before translating to \CASL. \\\hline
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederCommonLogic2CASLCompact & Coding compact Common Logic to \CASL.
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder Compact Common Logic is a sublogic of Common Logic
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder where no sequence markers occur. Module elimination
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder is applied before translating to \CASL. We recommend
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder using this comorphism whenever possible because it
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder results in simpler specifications.\\\hline
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederCommonLogicModuleElimination & Eliminating modules from a Common Logic theory
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder resulting in an equivalent specification without
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder modules. \\\hline
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederOWL22CommonLogic & Inclusion of OWL2 description logic \\\hline
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederProp2CommonLogic & Inclusion of propositional logic \\\hline
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederSoftFOL2CommonLogic & Inclusion of first order logic \\\hline
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederCASL2SoftFOL & Coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroedermapping types to soft types \\\hline
dfe355b50888d0dea1c12713288b652741844080Jonathan von SchroederCASL2SoftFOLInduction & Same as CASL2SoftFOL but with instances of induction
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroederaxioms for all proof goals \\\hline
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von SchroederCASL2SoftFOLInduction2 & Similar to CASL2SoftFOLInduction but replaces goals with induction premises \\\hline
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von SchroederCASL2Propositional & Translation of propositional FOL \\\hline
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder\end{tabularx}\\
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von SchroederThose comorphisms can be chained, e.g., for theorem proving, you can translate
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von SchroederCommon Logic to SoftFOL with \texttt{CommonLogic2CASLCompact;CASL2SoftFOLInduction}
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroedersince there is no prover for Common Logic or \CASL.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederFor further information on logic translations supported by \Hets, see the \Hets
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederuser guide \cite{HetsUserGuide}.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\section{Getting started}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederThe latest \Hets version can be obtained from the
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\Hets tools home page
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder Since \Hets is being
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroederimproved constantly, it is recommended always to use the latest version.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\Hets is currently available (on Intel architectures only) for Linux
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederThere are several possibilities to install \Hets.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\begin{enumerate}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederThe best support is currently given via Ubuntu packages.
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederFor Ubuntu Lucid Lynx, enter the following into a terminal:
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\begin{lstlisting}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedersudo apt-add-repository ppa:hets/hets
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedersudo apt-add-repository \
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder "deb http://archive.canonical.com/ubuntu lucid partner"
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroedersudo apt-get update
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroedersudo apt-get install hets
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\end{lstlisting}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederFor later Ubuntu versions, replace lucid by maverick, natty or oneiric.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThis will also install quite a couple of tools for proving requiring about
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder800 MB of disk space. For a minimal installation use \texttt{apt-get install
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder hets-core} instead of \texttt{hets}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\item For Mac OS X 10.6 (Snow Leopard) we provide a meta package
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \texttt{Hets.mpkg} based on MacPorts that will be extended by further tools
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder for proving in the future.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThen we have Java based \Hets installer that we may drop in the future.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDownload a \texttt{.jar} file and start it with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{lstlisting}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\end{lstlisting}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederNote that you need Sun/Oracle Java 1.4.2 or later. On a Mac, you can just
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederdouble-click on the \texttt{.jar} file, but you have to install the MacPorts
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{libglade2} package (and all its dependencies) yourself. In order to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederspeed this up we provide a meta package \texttt{libglade2.mpkg}, too.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThe installer will lead you through the installation with
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedera graphical interface. It will download and install further
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersoftware (if not already installed on your computer):
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabularx}{\linewidth}{|l|l|X|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von SchroederTcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDarwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederIf you do not have Sun/Oracle Java, you can just download the hets binary.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederYou have to unpack it with \texttt{bunzip2} and then put it into
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersome place covered by your \texttt{PATH} environment variable. You also have to
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinstall the above mentioned software and set
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederseveral environment variables, as explained on the installation page.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederYou may compile \Hets from the sources (they are licensed under GPL),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederplease follow the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederlink ``Hets: source code and information for developers''
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederon the \Hets web page, download the sources (as tarball or from
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersvn), and follow the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinstructions in the \texttt{INSTALL} file, but be prepared to take some time.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederDepending on your application further tools are supported and may be
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederinstalled in addition:
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\begin{tabularx}{\linewidth}{|l|l|X|}\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederzChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederminisat & SAT solver & \url{http://minisat.se/} \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederPellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederE-KRHyper & theorem prover
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederReduce & computer algebra system
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder & \url{http://www.reduce-algebra.com/} \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederVSE & theorem prover & (non-public) \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederTwelf & & \url{http://twelf.plparty.org/} \\\hline
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\section{Analysis of Specifications}
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederConsider the following Common Logic text written in CLIF:
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\begin{lstlisting}[language=clif]
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder(and (P x) (Q y))
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder(or (Cat x) (Mat y))
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder(if (P x) (Q x))
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder(exists (z) (and (Pet x) (Happy z) (Attr x z)))
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder\end{lstlisting}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Hets can be used for parsing and
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederchecking static well-formedness of specifications.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \index{parsing}%
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \index{static!analysis}%
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder \index{analysis, static}%
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederLet us assume that the example is in a file named
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederThen you can check the well-formedness of the
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederspecification by typing (into some shell):
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\Hets checks both the correctness of this specification
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder with respect to the CLIF syntax, as
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederwell as its correctness with respect to the static semantics.
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von SchroederThe following flags are available in this context:
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder\begin{description}
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder\item[\texttt{-p}, \texttt{-{}-just-parse}] Just do the parsing
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder -- the static analysis is skipped and no development graph is created.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\item[\texttt{-s}, \texttt{-{}-just-structured}] Do the parsing and the
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder static analysis of (heterogeneous) structured specifications, but
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder leave out the analysis of basic specifications. This can be used
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder for prototyping issues, namely to quickly produce a development graph
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder showing the dependencies among the specifications (cf.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder Sect.~\ref{sec:DevGraph}) even if the individual specifications are
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder not correct yet.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\item[\texttt{-L DIR}, \texttt{-{}-hets-libdir=DIR}]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederUse \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{description}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederThere are more flags which can be used with \Hets, see \cite{HetsUserGuide}.
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\section{Heterogeneous Specification} \label{sec:HetSpec}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\Hets accepts plain text input files (for the
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroederpresented logics) with the following endings:
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\begin{tabular}{|l|c|c|}\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederfilename extension & default logic & structuring language\\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{.casl} & \CASL & \CASL \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder\texttt{.het} & \CASL & \CASL \\\hline
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder\texttt{.owl} & OWL2 & OWL2 \\\hline
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder\texttt{.clf} or \texttt{.clif} & CommonLogic & custom, see Sect.~\ref{relationsInCL} \\\hline
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von SchroederAlthough the endings \texttt{.casl} and \texttt{.het} are
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederinterchangeable, the former should be used for libraries of
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederhomogeneous \CASL specifications and the latter for \HetCASL libraries
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederof heterogeneous specifications (that use the \CASL structuring
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederconstructs). Within a \HetCASL library, the current logic can be changed, e.g.,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederto Common Logic in the following way:
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\begin{lstlisting}[morekeywords=logic]
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederlogic CommonLogic
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\end{lstlisting}
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von SchroederThe subsequent specifications are then parsed and analysed as
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von SchroederCommon Logic specifications. Within such specifications,
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederit is possible to use references to named \CASL specifications;
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederthese are then automatically translated along the default
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederembedding of \CASL into Common Logic (cf.\ Fig.~\ref{fig:LogicGraph}).
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder(There are also heterogeneous constructs
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroederfor explicit translations between logics, see \cite{Mossakowski04}.)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von SchroederThe endings \texttt{.clf} and \texttt{.clif} are available for directly reading in
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederCommon Logic CLIF texts, as in the example of \texttt{Cat.clif}.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederthe logic Common Logic has to be chosen explicitly, and the \CASL structuring
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroedersyntax needs to be used:
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{lstlisting}[language=clif,morekeywords={library,logic,spec,then}]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederlogic CommonLogic
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (and (P x) (Q y))
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder. (or (Cat x) (Mat y))
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (if (P x) (Q x))
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederPred and Cat then
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder. (exists (z) (and (Pet x) (Happy z) (Attr x z)))
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\end{lstlisting}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederNote that the dot at the beginning of a line indicates that a new text begins.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederHence, it is possible to have multiple texts in a \CASL specification.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederThis specification is the \HetCASL-structured equivalent to the following three
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederCLIF 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.}\\
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{lstlisting}[language=clif]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (and (P x) (Q y))
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\end{lstlisting}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{lstlisting}[language=clif]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (or (Cat x) (Mat y))
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (if (P x) (Q x))
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\end{lstlisting}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\begin{lstlisting}[language=clif]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder(cl:text PetHappy
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (cl:imports Pred) (cl:imports Cat)
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder (exists (z) (and (Pet x) (Happy z) (Attr x z)))
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\end{lstlisting}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von SchroederBoth can be directly used with \Hets, where the former content would be in a
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederfile with the extension \texttt{.het} and the latter in a file with one of the extensions
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\texttt{.clf} or \texttt{.clif}. This specification is divided into three
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederparts, which are linked to each other. These links and some more information can
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederbe seen in the development graph of the file.
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder\section{Development Graphs}\label{sec:DevGraph}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederDevelopment graphs are a simple kernel formalism for (heterogeneous)
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederstructured theorem proving and proof management.
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von SchroederA development graph consists of a set of nodes (corresponding to whole
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederstructured specifications or parts thereof), and a set of edges
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedercalled \emph{definition links}, indicating the dependency of each
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederinvolved structured specification on its subparts. Each node is
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederassociated with a signature and some set of local axioms. The axioms
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederof other nodes are inherited via definition links. Definition links
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederare usually drawn as black solid arrows, denoting an import of another
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederComplementary to definition links, which \emph{define} the theories of
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederrelated nodes, \emph{theorem links} serve for \emph{postulating}
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederrelations between different theories. Theorem links are the central
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederdata structure to represent proof obligations arising in formal
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederTheorem links can be \emph{global} (drawn as solid arrows) or
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\emph{local} (drawn as dashed arrows): a global theorem link
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederpostulates that all axioms of the source node (including the inherited
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederones) hold in the target node, while a local theorem link only postulates
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederthat the local axioms of the source node hold in the target node.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederBoth definition and theorem links can be \emph{homogeneous},
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederi.e.\ stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederthe logic changes along the arrow.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederTheorem links are initially displayed in red.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe \emph{proof calculus} for development graphs
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\cite{MossakowskiEtAl05,Habil} is given by rules
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederthat allow for proving global theorem links by decomposing them
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederinto simpler (local and global) ones. Theorem links that have been
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederproved with this calculus are drawn in green by {\Hets}. Local theorem links can
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederbe proved by turning them into \emph{local proof goals}. The latter
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedercan be discharged using a logic-specific calculus as given by an
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederentailment system for a specific institution. Open local
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederproof goals are indicated by marking the corresponding node in the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederdevelopment graph as red; if all local implications are proved, the
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroedernode is turned into green. This implementation ultimately is based
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederon a theorem \cite{Habil} stating soundness and relative completeness
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederof the proof calculus for heterogeneous development graphs.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe following options let \Hets display the development graph of
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedera specification library:
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{description}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[\texttt{-g}, \texttt{-{}-gui}] shows the development graph in a GUI window
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[\texttt{-u}, \texttt{-{}-uncolored}] no colours in shown graphs
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\end{description}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe following additional options also apply typical rules from the development
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedergraph calculus to the final graph and save applying these rules via the GUI.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{description}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item[\texttt{-A}, \texttt{-{}-apply-automatic-rule}] apply the automatic
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder strategy to the development graph. This is what you usually want in order to
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder get goals within nodes for proving.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item[\texttt{-N}, \texttt{-{}-normal-form}] compute all normal forms for nodes
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder with incoming hiding links. (This may take long and may not be implemented
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder for all logics.)
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\end{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederFor a summary of the types of nodes and links occurring in
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederdevelopment graphs, see the \Hets user guide \cite{HetsUserGuide}.\\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederMost of the pull-down menus of the development graph window are
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederuDraw(Graph)-specific layout menus; their function can be looked up in
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederthe uDraw(Graph) documentation\footnote{see
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe Edit menu is the only exception.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederWith choosing Edit→Proofs→Auto-DG prover, you can can prove red theorem
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroederlinks (which may be generated by relative interpretations of theories).
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederActually, this will generate new proof obligations at some node,
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederwhich then can be discharged there.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederMoreover, the nodes and links of the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedergraph have attached pop-up menus, which appear when clicking (and
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederholding) the right mouse button.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe node menus ``Prove'' and ``Check consistency'' are the most
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederimportant ones. With ``Add sentence'', you can add axioms and
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederproof goals on the fly.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederFor a detailed explanation of the menus
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedersee the \Hets User Guide \cite{HetsUserGuide}.
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder\subsection{Relations between Common Logic Texts}
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder\label{relationsInCL}
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder\Hets supports several relations between Common Logic Texts. However only one of
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroederthem is defined in ISO/IEC 24707:2007 \cite{iso24a}. All the other relations are
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroederunofficial extensions used e.g.\ by the Common Logic Repository COLORE \cite{Colore}.
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder\begin{description}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder\item[Importation] \label{descr:link_import}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder is defined in ISO/IEC 24707:2007 \cite{iso24a} as virtual copying of a
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder resource. In \Hets a whole file is ``copied'' into the importing
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder specification. Hets cannot currently handle cyclic imports. If you really need
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder them, send us a message at \href{mailto:hets@informatik.uni-bremen.de}{hets@informatik.uni-bremen.de}, and we will fix it.
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder Using CLIF, you can import \texttt{someFile.clif} via
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder \begin{lstlisting}[language=clif]
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder \end{lstlisting}
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder Omitting the file extension will also succeed. In this case \Hets will look
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder for a file called \texttt{someFile.clif} in first place and then for
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder \texttt{someFile.clf} in the current directory and then in the library paths.
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder \Hets also supports URIs for importing resources. The allowed URI schemes are
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder \texttt{file:}, \texttt{http:} and \texttt{https:}.
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder \begin{lstlisting}[language=clif]
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder(cl:imports file:///absolute/path/to/someFile.clif)
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder(cl:imports http://someDomain.com/path/to/someFile.clif)
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder(cl:imports https://someDomain.com/path/to/someFile.clif)
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder \end{lstlisting}
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder The importation is indicated by a global definition link (black arrow) in the
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder development graph.
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder\item[Relative interpretation]
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder is described in \cite{colore-fois}. It is represented by a theorem link
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder (red arrow) in the development graph. In a Common Logic file it is specified
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder inside of a comment on text-level, that is a comment in the uppermost level
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder of the (optionally named) Common Logic text instead of a comment in a sentence or
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder \begin{lstlisting}[language=clif]
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder(cl:text someText
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder (cl:comment '(relative-interprets someTranslationFile someTargetFile)')
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder \end{lstlisting}
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder Just as with imports (\ref{descr:link_import}), \Hets supports different types
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder of references to resources here, such as URIs.
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder Alternatively, the \HetCASL syntax for relative interpretations is
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder\textbf{view} \textit{v} : \textit{sp1} \textbf{to} \textit{sp2} \textbf{end}
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder Views are declared outside of specifications, as can be seen from List.~\ref{fig:lang}.
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder\item[Nonconservative extension]
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder is represented by a theorem link (red arrow) in the development graph. In a
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder Common Logic file it is specified inside of a comment on text-level:
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder \begin{lstlisting}[language=clif]
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder(cl:comment '(nonconservative-extension someTargetFile)')
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder \end{lstlisting}
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder Just as with imports (\ref{descr:link_import}), \Hets supports different types
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder of references to resources here, as e.g. URIs.
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder%TODO: briefly describe colore-relations.
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder%TODO: include other colore-relations
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder\item[Inclusion]
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder is not a relation between theories. However inclusion can useful. It is used
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder to show other theories in the development graph, without any connection
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder to the current theory. In a Common Logic file inclusion is specified in a
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder text-level comment:
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder \begin{lstlisting}[language=clif]
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder(cl:comment '(include-libs someFile someOtherFile nextFile andSoOn)')
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder \end{lstlisting}
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder The keyword \texttt{include-libs} is followed by a whitespace-separated list
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder of resources to be shown in the development graph. The resource-names can be
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder of different type here, too.
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder\end{description}
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von SchroederExcept for importation and inclusion, you can specify an optional symbol map
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder(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.}
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder Names from the target file are mapped to names from the current
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederfile (including the translation file, if the relation uses one). Note that is is possible to use cyclic relations in \Hets. Only the cyclic
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroederimportation is not supported.
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\subsection{Examples}
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\label{sec:examples}
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\subsubsection{Renaming Symbols with Symbol Maps}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\label{sec:renam-symb-with}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThis example has two almost identical files, \texttt{upper.clif} and
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\texttt{lower.clif}. The only difference in the actual axioms is that
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\texttt{upper.clif} uses uppercase predicates while \texttt{lower.clif}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederuses lowercase predicates. The symbol is added at the end of the relation
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederdefinition in parentheses. Only those names that differ between source
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederand target need to be listed. The other names are implicitly the same.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederA mapping of a single name is defined with
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder``\texttt{nameInTargetFile |-> nameInCurrentFile}''; multiple mappings are
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederseparated by commas. Note that in Common Logic, a comma can be part of a name.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederHence a space must be placed between the separation-comma and a name.\\
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{description}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{lstlisting}[language=clif]
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder (cl:comment '(nonconservative-extension lower
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder (forall (x y) (iff (A x y)
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder\end{lstlisting}
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder\begin{lstlisting}[language=clif]
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder (cl:comment '(nonconservative-extension upper (A |-> a , B |-> b))')
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder (forall (x y) (iff (a x y)
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder\end{lstlisting}
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder\end{description}
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder\subsubsection{Ontology-based Ambient Assisted Living Services and Devices}
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder\label{sec:aal-example}
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder\section{Proofs with \Hets}\label{sec:Proofs}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von SchroederThe proof calculus for development graphs (Sect.~\ref{sec:DevGraph}) reduces
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroederglobal theorem links to local proof goals. You can do this reduction by clicking
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroederon the Edit-menu in the development graph window and selecting
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von SchroederProofs/Auto-DG-Prover. Local proof goals (indicated by red
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroedernodes in the development graph) can be eventually discharged using a theorem
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroederprover, i.e.\ by using the ``Prove'' menu of a red node.
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von SchroederThe graphical user interface (GUI) for calling a prover is shown in
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von SchroederFig.~\ref{fig:proof_window} --- we call it ``Proof Management GUI''.
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von SchroederThe top list on the left shows all goal names prefixed with their proof
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroederstatus in square brackets. A proved goal is indicated by a `+', a `–'
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroederindicates a disproved goal, a space denotes an open goal, and a
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder`$\times$' denotes an inconsistent specification (aka a fallen `+';
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroedersee below for details).
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\begin{figure}[ht]
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder \includegraphics[width=0.5\linewidth,keepaspectratio=true]{UserGuideCL_Prove_devGraph}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder \caption{Prove local proof obligation\label{fig:Prove_devGraph}}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\begin{figure}[ht]
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder\begin{minipage}[b]{0.5\linewidth}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Prove_Prove}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder \caption{\Hets Goal and Prover Interface\label{fig:proof_window}}
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder\hspace{0.1\linewidth}
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder\begin{minipage}[b]{0.5\linewidth}
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Prove_Vampire}
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder \caption{Interface of Vampire Prover\label{fig:Vampire}}
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von SchroederIf you open this GUI when processing the goals of one node for the
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroederfirst time, it will show all goals as open. Within this list you can
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroederselect those goals that should be inspected or proved. The GUI elements are the following:
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\item The button `Display' shows the selected goals in the ASCII syntax of
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder this theory's logic in a separate window.
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder\item By pressing the `Proof details' button a window is opened where for each
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder proved goal the used axioms, its proof script, and its proof are shown ---
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder the level of detail depends on the used theorem prover.
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder\item With the `Prove' button the actual prover is launched. The provers are described
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder in more detail in the \Hets user guide \cite{HetsUserGuide}.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\item The list `Pick Theorem Prover:' lets you choose one of the connected
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder provers (among them \Isabelle, MathServe Broker, \SPASS, Vampire, and
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder zChaff, described below). By pressing `Prove' the selected prover is
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder launched and the theory along with the selected goals is translated via the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder shortest possible path of comorphisms into the prover's logic.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item The pop-up choice box below `Selected comorphism path:' lets you pick a
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder (composed) comorphism to be used for the chosen prover. If the specification
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder does not contain any sequence markers, it is possible to use the comorphism
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \texttt{CommonLogic2CASLCompact} which results in a simpler
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \CASL specification. We recommend using this comorphism whenever possible.
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder\item Since the amount and kind of sentences sent to an ATP system is a major
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder factor for the performance of the ATP system, it is possible to select in
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder the bottom lists the axioms and proven theorems that will comprise the
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder theory of the next proof attempt. Based on this selection the sublogic may
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder vary \ednote{CL: From here, my brain can't parse this sentence.}and also the available provers and comorphisms to provers. Former
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder theorems that are imported from other specifications are marked with the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder prefix `(Th)'. Since former theorems do not add additional logical content,
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder they may be safely removed from the theory.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item If you press the bottom-right `Close' button the window is closed and
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder the status of the goals' list is integrated into the development graph. If
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder all goals have been proved, the selected node turns from red into green.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\item All other buttons control selecting list entries.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederIn order to prove or disprove a theorem, it needs to be declared as proof
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederobligation. This is done by the keyword \texttt{\%implied} at the end of a text:
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder\begin{lstlisting}[morekeywords={logic,spec,and,implied,end}]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroederlogic CommonLogic
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder (and (P x) (Q y))
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder. (Q y) %implied %(correct)%
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder. (P y) %implied %(incorrect)%
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\end{lstlisting}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von SchroederIn this specification the theorems, annotated (named) by \texttt{correct} and
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder\texttt{incorrect} are the ones, that can be proven or disproven.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederNote that they are separate texts inside the specification \texttt{ToProve}.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederThe annotations are optional. For proving, they are the names shown in the
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder``Axioms to include'' section of the prover interface
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder(Fig.~\ref{fig:proof_window}).
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe same specification can be written down in CLIF:
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\begin{lstlisting}[language=clif,morekeywords={implied}]
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder (and (P x) (Q y))
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder(cl:text correct
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder(cl:text incorrect (P y)) %implied
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder\end{lstlisting}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von SchroederIn CLIF, there is no notion of proof obligation. Hence the \texttt{\%implied}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroederkeyword of \Hets must be used, and thus the specification is not pure CLIF. Because the texts have
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroedernames, these are also used in the prover interface. Otherwise, \Hets invents
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder\subsection{Consistency Checker}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von SchroederSince proofs are void if specifications are inconsistent, the consistency
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroedershould be checked (if possible for the given logic) by the ``Consistency
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroederchecker'' shown in Fig.~\ref{fig:cons_window}. This GUI is invoked from
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroederthe `Edit' menu as it operates on all nodes.
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von SchroederThe list on the left shows all node names prefixed with a consistency status
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederin square brackets that is initially empty. A consistent node is indicated by
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedera `+', a `–' indicates an inconsistent node, a `t' denotes a timeout of the last
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederchecking attempt.
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder\begin{figure}[ht]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\begin{minipage}[b]{0.5\linewidth}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Consistency_devGraph}
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder \caption{Selection of consistency checker\label{fig:cons_devGraph}}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder\hspace{0.1\linewidth}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder\begin{minipage}[b]{0.5\linewidth}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder \includegraphics[width=\linewidth,keepaspectratio=true]{UserGuideCL_Consistency_Interface}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder \caption{\Hets Consistency Checker Interface\label{fig:cons_window}}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederFor some selection of nodes (of a common logic) a model finder should be
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederselectable from the `Pick Model finder:' list. Currently only for ``darwin''
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroedersome \CASL models can be re-constructed. When pressing `Check', possibly after
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder`Select comorphism path:', all selected nodes will be checked, spending at
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedermost the number of seconds given under `Timeout:' on each node. Pressing
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroeder`Stop' allows to terminate this process if too many nodes have been chosen.
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von SchroederEither by `View results' or automatically the `Results of consistency check'
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder(Fig.~\ref{fig:cons_res}) will pop up and allow you to inspect the models for
61d26ef772466529400bc460e7c69f67c1173b56Jonathan von Schroedernodes, if they could be constructed.
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder\begin{figure}[ht]
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \includegraphics[width=0.75\linewidth,keepaspectratio=true]{UserGuideCL_Consistency_Result}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder \caption{Consistency checker results\label{fig:cons_res}}
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder\subsection[Automated Theorem Proving Systems]
93e4ae9221332f59e762fd04392096af1511f6b8Jonathan von Schroeder{Automated Theorem Proving Systems\\(Logic SoftFOL)}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder\includegraphics[width=\textwidth]{spassGUI1}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder\caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von SchroederAll ATPs integrated into \Hets share the same GUI, with only a slight
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroedermodification for the MathServe Broker: the input field for extra options is
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroederinactive. Fig.~\ref{fig:SPASS_GUI} shows the instantiation for \SPASS, where
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroederin the top right part of the window the batch mode can be controlled. The
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroederleft side shows the list of goals (with status indicators). If goals are
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroedertimed out (indicated by `t') it may help to activate the check box `Include
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroederpreceding proven theorems in next proof attempt' and pressing `Prove all'
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederOn the bottom right the result of the last proof
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroederattempt is displayed. The `Status:' indicates `Open', `Proved', `Disproved',
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder`Open (Time is up!)', or `Proved (Theory inconsistent!)'. The list of `Used
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von SchroederAxioms:' is filled by \SPASS. The button `Show Details' shows the whole output
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederof the ATP system. The `Save' buttons allow you to save the input and
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederconfiguration of each proof for documentation. By `Close' the results for all
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroedergoals are transferred back to the Proof Management GUI.
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederThe MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederZimmer provides a unified interface to a range of different ATP
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroedersystems; the most important systems are listed in
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von SchroederTab.~\ref{tab:MathServe}, along with their capabilities. These
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedercapabilities are derived from the \emph{Specialist Problem Classes}
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder(SPCs) defined upon the basis of logical, language and syntactical
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederproperties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von SchroederOnly two of the Web services provided by the MathServe system are used
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederby \Hets currently: Vampire and the brokering system. The ATP systems
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroederare offered as Web Services using standardised protocols and formats
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroedersuch as SOAP, HTTP and XML. Currently, the ATP system Vampire may be
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederaccessed from \Hets via MathServe; the other systems are only reached
ca8f01a2b83fbb929aaf29629f71b10fd867956aJonathan von Schroederafter brokering.
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder\begin{table}[t]
| graph.(exp.dot|dot)
The \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
When the \texttt{comptable.xml} format is selected, \Hets will extract
algebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
available from \url{http://www.cofi.info/Libraries}.
\LaTeX\ version of \texttt{Cat.clif} by typing:
This will generate a file \texttt{Cat.pp.tex}. It can be included
into \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
coming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
The format \texttt{pp.xml} represents just a parsed library in XML.
The \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
\item[\texttt{-x}, \texttt{-{}-xml}] use XML-PGIP\footnote{Proof General Interface Protocol} packets to communicate with
(i.e.\ \texttt{-d LogicGraph} lists the logics and comorphisms)
\url{http://pollux.informatik.uni-bremen.de:8000/}. It allows to browse the
\item[\texttt{-l LOGIC}, \texttt{-{}-logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
\item[\texttt{-e ENCODING}, \texttt{-{}-encoding=ENCODING}] Read input files using latin1 or utf8 encoding. The default is still latin1.
\item[\texttt{-{}-relative-positions}] Just uses the relative library name in positions of warning or errors.
\item[\texttt{-U FILE}, \texttt{-{}-xupdate=FILE}] update a development graph according to special XML update information (still experimental).