UserGuideCommonLogic.tex revision f8b3526c0e58902c94ea3ae921409828925e1115
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\documentclass{article}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\setlength{\textwidth}{16cm}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\setlength{\topmargin}{-1cm}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\setlength{\evensidemargin}{0cm}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\setlength{\oddsidemargin}{0cm}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\setlength{\textheight}{22.5cm}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\usepackage[utf8]{inputenc}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage[T1]{fontenc}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{charter} % very clean and readable font
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{courier}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage[show]{ed} % set to hide for producing a released version
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{alltt}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{casl}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{color}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{url}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{threeparttable,hhline}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{tabularx}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{paralist}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage{listings}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\lstset{basicstyle=\ttfamily,columns=fixed}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\usepackage[pdfborder=0 0 0,bookmarks,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipdfauthor={Till Mossakowski, Christian Maeder, Mihai Codescu, Eugen Kuksa, Christoph Lange},
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipdftitle={Hets for Common Logic Users}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski{hyperref} %% do not load more packages after this line!!
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\QUERY}[1]%{}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski{\marginpar{\raggedright\hspace{0pt}\small #1\\~}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\eat}[1]{}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{EXAMPLE}[1][] {\par#1\begin{EXAMPLEFORMAT}\begin{ITEMS}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski {\end{ITEMS}\end{EXAMPLEFORMAT}\par}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\IEXT}[1] {\\#1\I}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\IEND} {\I\END}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{EXAMPLEFORMAT} {}{}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Added by MB to have some extra vertical space after the ``main'' examples
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% following the points (and some others in the text):
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{BIGEXAMPLE} {\begin{EXAMPLE}} {\end{EXAMPLE}\medskip}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{DETAILS}[1][] {#1\begin{DETAILSFORMAT}}{\end{DETAILSFORMAT}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{DETAILSFORMAT} {}{}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newenvironment{META}[1][] {#1\begin{METAFORMAT}}{\end{METAFORMAT}}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newenvironment{METAFORMAT} {\medskip\vrule\hspace{1ex}\vrule\hspace{1ex}%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{minipage}{0.9\textwidth}\it}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski {\end{minipage}\par\medskip}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SLIDESMALL} {}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SLIDESONLY}[1] {}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski% SIMULATING SMALL-CAPS FOR BOLD, EMPH
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\normalTEXTSC}[2]{{#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% NOT \newcommand{\normalTEXTSC}[2]{{\normalsize#1\scriptsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeTEXTSC} [2]{{\large #1\small #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeTEXTSC} [2]{{\Large #1\normalsize#2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGETEXTSC} [2]{{\LARGE #1\large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\hugeTEXTSC} [2]{{\huge #1\Large #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HugeTEXTSC} [2]{{\Huge #1\LARGE #2}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\newcommand {\CASL}{\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCASL} {\largeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LargeCASL} {\LargeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGECASL} {\LARGETEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\hugeCASL} {\hugeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HugeCASL} {\HugeTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%\newcommand {\CoFI}{CoFI\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\MAYA}{\normalTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeMAYA} {\largeTEXTSC{M}{AYA}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHets} {\largeTEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LARGEHets} {\LARGETEXTSC{H}{ETS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Cats}{\normalTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeCats} {\largeTEXTSC{C}{ATS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\ELAN}{\normalTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeELAN} {\largeTEXTSC{E}{LAN}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\HOL}{\normalTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHOL} {\largeTEXTSC{H}{OL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Isabelle}{\normalTEXTSC{I}{SABELLE}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeIsabelle} {\largeTEXTSC{I}{SABELLE}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\SPASS}{\normalTEXTSC{S}{PASS}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand {\Horn}{\normalTEXTSC{H}{ORN}}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%% Klaus macros
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLDL}{\textmd{\textsc{Casl-DL}}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\Dolce}{\textmd{\textsc{Dolce}}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SHOIN}{$\mathcal{SHOIN}$(\textbf{D})\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SROIQ}{$\mathcal{SROIQ}$(\textbf{D})\xspace}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\newcommand{\DL}{DL\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%%%% end of Klaus macros
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%% Use \ELAN-\CASL, \HOL-\CASL, \Isabelle/\HOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\LCF}{LCF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\ASF}{ASF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\ASF}{\normalTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeASF} {\largeTEXTSC{A}{SF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SDF}{SDF\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand {\SDF}{\normalTEXTSC{S}{DF}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski%%\newcommand{\largeSDF} {\largeTEXTSC{S}{DF}\xspace}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\newcommand {\ASFSDF}{\normalTEXTSC{A}{SF}+\normalTEXTSC{S}{DF}\xspace}
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski\newcommand{\largeASFSDF} {\largeTEXTSC{A}{SF}+\largeTEXTSC{S}{DF}\xspace}
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski\newcommand {\HasCASL}{\normalTEXTSC{H}{AS}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\largeHasCASL} {\largeTEXTSC{H}{AS}\largeTEXTSC{C}{ASL}\xspace}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski%% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\newcommand{\CCC}{CCC\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CoCASL}{\normalTEXTSC{C}{O}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CspCASL}{\normalTEXTSC{C}{SP}-\normalTEXTSC{C}{ASL}\xspace}
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski\newcommand{\Csp}{\normalTEXTSC{C}{SP}\xspace}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\newcommand{\CcsCASL}{CCS-\normalTEXTSC{C}{ASL}\xspace}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\newcommand{\CASLLtl}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{L}{TL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\CASLChart}{\normalTEXTSC{C}{ASL}-\normalTEXTSC{C}{HART}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\SBCASL}{\normalTEXTSC{S}{B}-\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\HetCASL}{\normalTEXTSC{H}{ET}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\newcommand{\ModalCASL}{\normalTEXTSC{M}{odal}\normalTEXTSC{C}{ASL}\xspace}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{document}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\title{{\bf \protect{\LARGEHets} for Common Logic Users}\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski-- Version 0.99 --}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\author{Till Mossakowski, Christian Maeder,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Mihai Codescu, Eugen Kuksa, Christoph Lange\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDFKI GmbH, Bremen, Germany.\\[1em]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiComments to: \href{mailto:hets-users@informatik.uni-bremen.de}{hets-users@informatik.uni-bremen.de} \\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(the latter needs subscription to the mailing list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Introduction}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCommon Logic (CL) is an ISO standard published as ``ISO/IEC 24707:2007
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski--- Information technology — Common Logic (CL): a framework for a family
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof logic-based languages'' \cite{CommonLogic:oldfashioned}. CL is based on untyped first-order
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilogic, but extends first-order logic in two ways: \begin{inparaenum}[(1)]\item any term can be
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiused as function or predicate, and \item sequence markers allow
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifor talking about sequences of individuals directly\end{inparaenum}.\footnote
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski{Strictly speaking, only the second feature goes beyond first-order
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe Heterogeneous Tool Set (\Hets) is an open source software providing
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiseveral kinds of tool support for Common Logic:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{itemize}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item a parser for the Common Logic Interchange Format (CLIF) --- CLIF
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski is a Lisp-like syntax for CL;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item a connection of CL to well-known first-order theorem provers
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilike SPASS, darwin and Vampire, such that logical consequences
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof CL theories can be proved;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item a connection of CL to the higher-order provers Isabelle/HOL
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiand Leo-II in order to perform induction proofs in theories
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinvolving sequence markers;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item a connection to first-order model finders like darwin that
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiallow one to find models for CL theories;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item support for proving interpretations between CL theories to be correct;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item a translation that eliminates the use of CL modules\footnote{Actually, we are using a revised semantics for modules, as proposed
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskirecently in~\cite{NH:CommonLogicHoratio}.}. Since the semantics of CL modules
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiis special to CL, this elimination of modules is necessary before
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisending CL theories to a standard first-order prover;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item a translation of the Web Ontology Language OWL to CL;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item a translation of propositional logic to CL.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis guide will introduce you to these functionalities of \Hets.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor the full functionalities of \Hets, see the \Hets user guide
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{HetsUserGuide}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{The Heterogeneous Tool Set and Its Input Languages}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe central idea of the Heterogeneous Tool Set (\protect\Hets) is to
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprovide a general framework for formal methods integration and proof
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskimanagement. One can think of \Hets acting like a motherboard where
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidifferent expansion cards can be plugged in, the expansion cards here
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskibeing individual logics (with their analysis and proof tools) as well
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskias logic translations. The \Hets motherboard already has plugged in
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskia number of expansion cards (e.g., the theorem provers Isabelle, SPASS
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiand more, as well as model finders). Hence, a variety of tools is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiavailable, without the need to hard-wire each tool to the logic at
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{center}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \includegraphics[width=0.45\textwidth]{hets-motherboard}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\caption{The \Hets motherboard and some expansion cards}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets consists of logic-specific tools for the parsing and static
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskianalysis of the different involved logics, as well as a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic-independent parsing and static analysis tool for structured and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiarchitectural specifications and libraries. The latter of course needs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito call the logic-specific tools whenever a basic specification is
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets is based on the theory of institutions \cite{GoguenBurstall92},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhich formalise the notion of a logic. The theory behind \Hets is laid
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiout in \cite{Habil}. A short overview of \Hets is given in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{MossakowskiEA06,MossakowskiEtAl07b}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets supports a number of input languages directly, such as Common
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLogic and OWL2 and \HetCASL. They will be described in the next
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\subsection{Common Logic and the Common Logic Interchange Format (CLIF)}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCLIF is specified in Annex A of the Common Logic standard
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{CommonLogic:oldfashioned}. \Hets can directly read in files in
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCLIF syntax, and also recursively reads in any imported files (cf.\ section~\ref{relationsInCL} for the syntax).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCommon Logic itself does not support the specification of logical
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiconsequences, nor relative theory interpretations, nor other
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifeatures that speak about structuring and comparing logical
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitheories. Michael Gr\"uninger has suggested certain special annotations comments for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithis purpose, which are supported by \Hets, see
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisection~\ref{relationsInCL}. Alternatively, CLIF syntax can be used
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifor specifications within \HetCASL files, or CLIF files can be referred to within \HetCASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifiles. \HetCASL is a structuring language supporting relative theory
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinterpretations and other things, see section~\ref{HetCASL} below.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{OWL2}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiOWL2 is a W3C standard \cite{w3c:owl2-overview}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets can directly read in OWL2 files in various syntaxes (called ``serialisations''), including
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe native OWL XML syntax \cite{w3c:owl2-xml}, the RDF/XML syntax \cite{w3c:owl2-RDF-mapping,w3c04:rdf-xml}\ednote{CL: This was previously ``the RDF syntax''; however RDF is just a data model, which has many possible syntaxes itself. I presume that Hets supports at least RDF/XML, but does it also supports further RDF serialisations, e.g.\ Turtle?}, and the human-readable
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiManchester syntax \cite{w3c:owl2-manchester}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSince OWL2 does not support relative theory interpretations and other
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructuring features, such things can only be expressed in \HetCASL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifiles. For this purpose, OWL2 Manchester syntax can be used within
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\HetCASL files, or OWL2 files can be referred to within \HetCASL files.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{HetCASL}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{HetCASL}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor heterogeneous specification, \Hets offers the Heterogeneous
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilanguage \HetCASL. \HetCASL is not so much a logic, but a meta
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilanguage that can express relations of theories written in different
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogics, like logical consequences, relative interpretations of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitheories, conservative extensions, translations of theories
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskialong logic translations, etc.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \HetCASL generalises the structuring
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\CASL (Common Algebraic Specification Language \cite{CASL-UM,CASL/RefManual}) to arbitrary logics
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(if they are formalised as institutions and plugged into
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe \Hets motherboard), as well as to heterogeneous
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicombinations of specifications written in different logics.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFig.~\ref{fig:lang} for a simple subset of the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\HetCASL syntax, where \emph{basic specifications} are unstructured
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications or modules written in a specific logic. The graph of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicurrently supported logics and logic translations (the latter are also
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskicalled comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidegree of support by \Hets in Fig.~\ref{fig:Languages}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{figure}[ht]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{lstlisting}[basicstyle=\ttfamily\small,morekeywords={then,with,logic,spec,end,view,to},escapeinside={<>}]
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSPEC ::= BASIC-SPEC %% <logic-specific syntax, e.g CLIF, Manchester syntax>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | SPEC then SPEC %% <extension of a spec with new symbols and axioms>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | SPEC then %implies SPEC %% <annotation: extension is logically implied>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | SPEC with SYMBOL-MAP %% <renaming of SPEC along SYMBOL-MAP>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | SPEC with logic ID %% <translation of SPEC to a different logic>
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiDEFINITION ::= logic ID %% <select a new logic for subsequent items>
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski | spec ID = SPEC end %% <give the name ID to SPEC>
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski | view ID : SPEC to SPEC = SYMBOL-MAP end %% <interpretation of theories>
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski | view ID : SPEC to SPEC = logic ID end %% <dto., but across different logics>
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiLIBRARY = DEFINITION*
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{lstlisting}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\caption{Syntax of a simple subset of the heterogeneous
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification language.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecific syntax, while \texttt{ID} stands for some form of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiidentifiers.\label{fig:lang}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiWith \emph{heterogeneous structured specifications}, it is possible to
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicombine and rename specifications, hide parts thereof, and also
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskitranslate them to other logics. \emph{Architectural specifications}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiprescribe the structure of implementations. \emph{Specification
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski libraries} are collections of named structured and architectural
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecifications. \emph{Refinements} express the fact the a specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiis becoming more specific. All this is supported by \HetCASL.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiFor details, see \cite{Mossakowski04,Habil,CASL/RefManual}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\section{Logics supported by Hets}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets supports a variety of different logics. The following are most important for use with Common Logic:
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{figure}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{center}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \includegraphics[width=\textwidth]{LogicGraph-CL}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\caption{Graph of logics related to Common Logic that are currently supported by \Hets. The more an
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiellipse is filled with green, the more stable is the implementation of the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilogic. Blue indicates a prover-supported logic.}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\label{fig:LogicGraph}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{figure}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{center}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{tabular}{|l|c|c|c|}\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiLanguage & Parser & Static Analysis & Prover \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\CASL & x & x & -- \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiCommon Logic & x (CLIF) & x & -- \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiOWL2 & x & x & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiPropositional & x & x & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiSoftFOL & x & -- & x \\\hline
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\caption{Current degree of \Hets support for some of the languages.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLanguages without prover can still ``borrow'' provers
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskivia logic translations.\label{fig:Languages}}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Common Logic] is an ISO standard published as ``ISO/IEC 24707:2007 - Information technology — Common Logic (CL): a framework for a family of logic-based languages'' \cite{CommonLogic:oldfashioned}. It is based on first-order logic, but extends first-order
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskilogic in several ways. The Common Logic
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Interchange Format (CLIF) provides a Lisp-like syntax for Common
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Logic. \Hets currently only supports parsing CLIF. If you need
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski other dialects, send us a message and we will add them.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[OWL2] is the Web Ontology Language recommended by the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski World Wide Web Consortium (W3C, \url{http://www.w3c.org}); see \cite{w3c:owl2-overview}. It is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski used for knowledge representation on the Semantic Web
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \cite{berners:2001:SWeb}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiHets calls an external OWL2 parser
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski written in Java to obtain the abstract syntax for an OWL file and its
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski imports. The Java parser also does a first analysis classifying
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski the OWL ontology into the sublanguages OWL Full (all of OWL, under the RDF semantics, undecidable \cite{w3c:owl2-rdf-based-semantics}), OWL DL (all of OWL, under the direct semantics \cite{w3c:owl2-direct-semantics}), and the so-called OWL Profiles (i.e.\ proper sublanguages) OWL EL, OWL QL, and OWL RL \cite{w3c:owl2-profiles}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Hets supports all except OWL Full.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski structuring of the OWL imports is displayed as a Development Graph.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Propositional] is classical propositional logic, with
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe zChaff SAT solver \cite{Herbstritt03} connected to it.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[SoftFOL] \cite{LuettichEA06a} offers several automated theorem
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski proving (ATP) systems for first-order logic with equality: \begin{inparaenum}[(1)]\item \SPASS
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \cite{WeidenbachEtAl02}, see \url{http://www.spass-prover.org};
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item Vampire \cite{RiazanovV02} see \url{http://www.vprover.org};
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item Eprover \cite{Schulz:AICOM-2002}, see \url{http://www.eprover.org};
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item E-KRHyper \cite{DBLP:conf/cade/PelzerW07}, see \url{http://www.uni-koblenz.de/~bpelzer/ekrhyper}, and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski MathServe Broker\footnote{which chooses an appropriate ATP upon a
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski classification of the FOL problem} \cite{ZimmerAutexier06}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\end{inparaenum}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski These together comprise some of the most advanced theorem provers
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski for first-order logic. SoftFOL is essentially the first-order
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski interchange language TPTP \cite{DBLP:conf/lpar/Sutcliffe10},
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[CASL] extends many sorted first-order logic with partial
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski functions and subsorting. It also provides induction sentences,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski expressing the (free) generation of datatypes.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor more details on \CASL see \cite{CASL/RefManual,CASL-UM}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiFor Common Logic, \CASL can be seen as kind of transitional hub, linking
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCommon Logic to other logics, most importantly SoftFOL.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\Isabelle] \cite{NipPauWen02} is the logic of the interactive
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski theorem prover Isabelle for higher-order logic.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[THF] is an interchange language for higher-order logic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \cite{DBLP:conf/cade/BenzmullerRS08}, similar to what TPTP
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski is for first-order logic. \Hets connects THF to the automated
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski higher-order prover Leo-II.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[HasCASL] is a higher order extension of \CASL allowing
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski polymorphic datatypes and functions. It is closely related to the
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski programming language Haskell and allows program constructs being
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski embedded in the specification. For Common Logic, \HasCASL
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski is mainly interesting as a transitional hub for paths
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski to the provers Isabelle and Leo-II.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[RelScheme] is a logic for relational databases \cite{DBLP:journals/ao/SchorlemmerK08}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiVarious logics are supported with proof tools. Proof support for the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiother logics can be obtained by using logic translations to a
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiprover-supported logic. For Common Logic, the paths to SoftFOL
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiare particularly interesting, because this offers an interface
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskito standard first-order provers. Moreover, the paths to THF
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand Isabelle offer interfaces to higher-order provers, which
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis essential if you want to prove inductive theorems about
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiAn introduction to \CASL can be found in the \CASL User Manual
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{CASL-UM}; the detailed language reference is given in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe \CASL Reference Manual \cite{CASL/RefManual}. These documents
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiexplain both the \CASL logic and language of basic specifications as
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwell as the logic-independent constructs for structured and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiarchitectural specifications. The corresponding document explaining the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\HetCASL language constructs for \emph{heterogeneous} structured specifications
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis the \HetCASL language summary \cite{Mossakowski04}; a formal
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisemantics as well as a user manual with more examples are in preparation.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSome of \HetCASL's heterogeneous constructs will be illustrated
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiin Sect.~\ref{sec:HetSpec} below.\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor further information on logics supported by \Hets, see the \Hets user guide
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{HetsUserGuide}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Logic translations supported by Hets}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\label{comorphisms}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiLogic translations (formalised as institution comorphisms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\cite{GoguenRosu02}) translate from a given source logic to a given
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskitarget logic. More precisely, one and the same logic translation
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimay have several source and target \emph{sub}logics: for
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskieach source sublogic, the corresponding sublogic of the target
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilogic is indicated.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIn more detail, the following list of logic translations involving Common Logic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiis currently supported by \Hets:\\
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\noindent\begin{tabularx}{\textwidth}{|l|X|}\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCommonLogic2CASL & Coding Common Logic to \CASL. Module elimination
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski is applied before translating to \CASL. \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCommonLogic2CASLCompact & Coding compact Common Logic to \CASL.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Compact Common Logic is a sublogic of Common Logic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski where no sequence markers occur. Module elimination
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski is applied before translating to \CASL. We recommend
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski using this comorphism whenever possible because it
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski results in simpler specifications.\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCommonLogicModuleElimination & Eliminating modules from a Common Logic theory
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski resulting in an equivalent specification without
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski modules. \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiOWL22CommonLogic & Inclusion of OWL2 description logic \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiProp2CommonLogic & Inclusion of propositional logic \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiSoftFOL2CommonLogic & Inclusion of first order logic \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCASL2SoftFOL & Coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskimapping types to soft types \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCASL2SoftFOLInduction & Same as CASL2SoftFOL but with instances of induction
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiaxioms for all proof goals \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCASL2SoftFOLInduction2 & Similar to CASL2SoftFOLInduction but replaces goals with induction premises \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCASL2Propositional & Translation of propositional FOL \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{tabularx}\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThose comorphisms can be chained, e.g., for theorem proving, you can translate
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiCommon Logic to SoftFOL with \texttt{CommonLogic2CASLCompact;CASL2SoftFOLInduction}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisince there is no prover for Common Logic or \CASL.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor further information on logic translations supported by \Hets, see the \Hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiuser guide \cite{HetsUserGuide}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Getting started}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe latest \Hets version can be obtained from the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets tools home page
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Since \Hets is being
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimproved constantly, it is recommended always to use the latest version.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Hets is currently available (on Intel architectures only) for Linux
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThere are several possibilities to install \Hets.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{enumerate}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe best support is currently given via Ubuntu packages.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor Ubuntu Lucid Lynx, enter the following into a terminal:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-add-repository ppa:hets/hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-add-repository \
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski "deb http://archive.canonical.com/ubuntu lucid partner"
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-get update
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisudo apt-get install hets
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor later Ubuntu versions, replace lucid by maverick, natty or oneiric.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThis will also install quite a couple of tools for proving requiring about
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski800 MB of disk space. For a minimal installation use \texttt{apt-get install
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski hets-core} instead of \texttt{hets}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item For Mac OS X 10.6 (Snow Leopard) we provide a meta package
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{Hets.mpkg} based on MacPorts that will be extended by further tools
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for proving in the future.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThen we have Java based \Hets installer that we may drop in the future.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDownload a \texttt{.jar} file and start it with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{lstlisting}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiNote that you need Sun/Oracle Java 1.4.2 or later. On a Mac, you can just
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidouble-click on the \texttt{.jar} file, but you have to install the MacPorts
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{libglade2} package (and all its dependencies) yourself. In order to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskispeed this up we provide a meta package \texttt{libglade2.mpkg}, too.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe installer will lead you through the installation with
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia graphical interface. It will download and install further
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisoftware (if not already installed on your computer):
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{tabularx}{\linewidth}{|l|l|X|}\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiHets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiuDraw(Graph) & graph drawing & \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTcl/Tk & graphics widget system & (version 8.4 or 8.5 must be installed before)\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\SPASS & theorem prover & \url{http://spass.mpi-sb.mpg.de/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDarwin & theorem prover & should be installed manually from \url{http://combination.cs.uiowa.edu/Darwin/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\Isabelle & theorem prover & \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(X)Emacs & editor (for Isabelle) & (must be installed manually)\\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{tabularx}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiIf you do not have Sun/Oracle Java, you can just download the hets binary.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiYou have to unpack it with \texttt{bunzip2} and then put it into
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisome place covered by your \texttt{PATH} environment variable. You also have to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinstall the above mentioned software and set
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiseveral environment variables, as explained on the installation page.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiYou may compile \Hets from the sources (they are licensed under GPL),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiplease follow the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilink ``Hets: source code and information for developers''
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskion the \Hets web page, download the sources (as tarball or from
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisvn), and follow the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiinstructions in the \texttt{INSTALL} file, but be prepared to take some time.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{enumerate}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDepending on your application further tools are supported and may be
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinstalled in addition:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{tabularx}{\linewidth}{|l|l|X|}\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskizChaff & SAT solver & \url{http://www.princeton.edu/~chaff/zchaff.html} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiminisat & SAT solver & \url{http://minisat.se/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiPellet & OWL reasoner & \url{http://clarkparsia.com/pellet/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiE-KRHyper & theorem prover
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \url{http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiReduce & computer algebra system
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski & \url{http://www.reduce-algebra.com/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMaude & rewrite system & \url{http://maude.cs.uiuc.edu/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiVSE & theorem prover & (non-public) \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiTwelf & & \url{http://twelf.plparty.org/} \\\hline
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{tabularx}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\section{Analysis of Specifications}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiConsider the following Common Logic text written in CLIF:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{lstlisting}[language=clif]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(and (P x) (Q y))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(or (Cat x) (Mat y))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(not (On x y))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(if (P x) (Q x))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(exists (z) (and (Pet x) (Happy z) (Attr x z)))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{lstlisting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets can be used for parsing and
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskichecking static well-formedness of specifications.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \index{parsing}%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \index{static!analysis}%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \index{analysis, static}%
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiLet us assume that the example is in a file named
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThen you can check the well-formedness of the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispecification by typing (into some shell):
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets checks both the correctness of this specification
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski with respect to the CLIF syntax, as
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiwell as its correctness with respect to the static semantics.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe following flags are available in this context:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-p}, \texttt{-{}-just-parse}] Just do the parsing
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- the static analysis is skipped and no development graph is created.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-s}, \texttt{-{}-just-structured}] Do the parsing and the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski static analysis of (heterogeneous) structured specifications, but
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski leave out the analysis of basic specifications. This can be used
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski for prototyping issues, namely to quickly produce a development graph
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski showing the dependencies among the specifications (cf.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Sect.~\ref{sec:DevGraph}) even if the individual specifications are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski not correct yet.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\item[\texttt{-L DIR}, \texttt{-{}-hets-libdir=DIR}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiUse \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicalling \Hets).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{description}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThere are more flags which can be used with \Hets, see \cite{HetsUserGuide}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\section{Heterogeneous Specification} \label{sec:HetSpec}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\Hets accepts plain text input files (for the
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskipresented logics) with the following endings:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{tabular}{|l|c|c|}\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifilename extension & default logic & structuring language\\\hline
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\texttt{.casl} & \CASL & \CASL \\\hline
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\texttt{.het} & \CASL & \CASL \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{.owl} & OWL2 & OWL2 \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\texttt{.clf} or \texttt{.clif} & CommonLogic & custom, see Chapter \ref{relationsInCL} \\\hline
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiAlthough the endings \texttt{.casl} and \texttt{.het} are
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinterchangeable, the former should be used for libraries of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskihomogeneous \CASL specifications and the latter for \HetCASL libraries
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiof heterogeneous specifications (that use the \CASL structuring
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiconstructs). Within a \HetCASL library, the current logic can be changed, e.g.,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskito Common Logic in the following way:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{lstlisting}[morekeywords=logic]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilogic CommonLogic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{lstlisting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe subsequent specifications are then parsed and analysed as
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCommon Logic specifications. Within such specifications,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiit is possible to use references to named \CASL specifications;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithese are then automatically translated along the default
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiembedding of \CASL into Common Logic (cf.\ Fig.~\ref{fig:LogicGraph}).
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(There are also heterogeneous constructs
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifor explicit translations between logics, see \cite{Mossakowski04}.)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThe endings \texttt{.clf} and \texttt{.clif} are available for directly reading in
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCommon Logic CLIF texts, as in the example of \texttt{Cat.clif}.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBy contrast, in \HetCASL libraries (ending with \texttt{.het}),
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskithe logic Common Logic has to be chosen explicitly, and the \CASL structuring
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskisyntax needs to be used:
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{lstlisting}[language=clif,morekeywords={library,logic,spec,then}]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskilogic CommonLogic
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (and (P x) (Q y))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski. (or (Cat x) (Mat y))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (not (On x y))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if (P x) (Q x))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskispec PetHappy =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPred and Cat then
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski. (exists (z) (and (Pet x) (Happy z) (Attr x z)))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{lstlisting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiNote that the dot at the beginning of a line indicates that a new text begins.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiHence, it is possible to have multiple texts in a \CASL specification.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiThis specification is the \HetCASL-structured equivalent to the following three
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCLIF files:\footnote{Note that where the Common Logic specification requires ``cl:text'', some samples available on the Web use ``cl-text''. Therefore, \Hets also supports the latter.}\\
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{lstlisting}[language=clif]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (and (P x) (Q y))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{lstlisting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{lstlisting}[language=clif]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (or (Cat x) (Mat y))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (not (On x y))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if (P x) (Q x))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{lstlisting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\begin{lstlisting}[language=clif]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(cl:text PetHappy
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (cl:imports Pred) (cl:imports Cat)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (exists (z) (and (Pet x) (Happy z) (Attr x z)))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski\end{lstlisting}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiBoth can be directly used with \Hets, where the former content would be in a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifile with the extension \texttt{.het} and the latter in a file with one of the extensions
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\texttt{.clf} or \texttt{.clif}. This specification is divided into three
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskiparts, which are linked to each other. These links and some more information can
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskibe seen in the development graph of the file.
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski\section{Development Graphs}\label{sec:DevGraph}
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiDevelopment graphs are a simple kernel formalism for (heterogeneous)
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskistructured theorem proving and proof management.
47af295501ed5f407848f61b9943d58ccb43be29Till MossakowskiA development graph consists of a set of nodes (corresponding to whole
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskistructured specifications or parts thereof), and a set of edges
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskicalled \emph{definition links}, indicating the dependency of each
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinvolved structured specification on its subparts. Each node is
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiassociated with a signature and some set of local axioms. The axioms
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiof other nodes are inherited via definition links. Definition links
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiare usually drawn as black solid arrows, denoting an import of another
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskispecification.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiComplementary to definition links, which \emph{define} the theories of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskirelated nodes, \emph{theorem links} serve for \emph{postulating}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskirelations between different theories. Theorem links are the central
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskidata structure to represent proof obligations arising in formal
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiTheorem links can be \emph{global} (drawn as solid arrows) or
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\emph{local} (drawn as dashed arrows): a global theorem link
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskipostulates that all axioms of the source node (including the inherited
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiones) hold in the target node, while a local theorem link only postulates
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithat the local axioms of the source node hold in the target node.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiBoth definition and theorem links can be \emph{homogeneous},
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskii.e. stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithe logic changes along the arrow.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiTheorem links are initially displayed in red.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill MossakowskiThe \emph{proof calculus} for development graphs
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\cite{MossakowskiEtAl05,Habil} is given by rules
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithat allow for proving global theorem links by decomposing them
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiinto simpler (local and global) ones. Theorem links that have been
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiproved with this calculus are drawn in green. Local theorem links can
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskibe proved by turning them into \emph{local proof goals}. The latter
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskican be discharged using a logic-specific calculus as given by an
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskientailment system for a specific institution. Open local
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiproof goals are indicated by marking the corresponding node in the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidevelopment graph as red; if all local implications are proved, the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskinode is turned into green. This implementation ultimately is based
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskion a theorem \cite{Habil} stating soundness and relative completeness
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiof the proof calculus for heterogeneous development graphs.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiDetails can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiand in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following options let \Hets show the development graph of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskia specification library:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-g}, \texttt{-{}-gui}] Shows the development graph in a GUI window
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-u}, \texttt{-{}-uncolored}] no colours in shown graphs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe following additional options also apply typical rules from the development
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskigraph calculus to the final graph and save applying these rule via the GUI.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\begin{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-A}, \texttt{-{}-apply-automatic-rule}] apply the automatic
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski strategy to the development graph. This is what you usually want in order to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski get goals within nodes for proving.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\item[\texttt{-N}, \texttt{-{}-normal-form}] compute all normal forms for nodes
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski with incoming hiding links. (This may take long and may not be implemented
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for all logics.)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\end{description}
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor a summary of the types of nodes and links occurring in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskidevelopment graphs, see the \Hets user guide \cite{HetsUserGuide}.\\
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMost of the pull-down menus of the development graph window are
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiuDraw(Graph)-specific layout menus; their function can be looked up in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskithe uDraw(Graph) documentation\footnote{see
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \url{http://www.informatik.uni-bremen.de/uDrawGraph/en/service/uDG31\_doc/}.}.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe exception is the Edit menu.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiWith choosing Edit, Proofs, Auto-DG prover, you can can prove red theorem
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskilinks (which may be generated by relative interpretations of theories).
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiActually, this will generate new proof obligations at some node,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiwhich then can be discharged there.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiMoreover, the nodes and links of the
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowskigraph have attached pop-up menus, which appear when clicking (and
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiholding) with the right mouse button.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiThe node menus ``Prove'' and ``Check consistency'' are the most
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskiimportant ones. With ``Add sentence'', you can add axioms and
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiproof goals on the fly.
5277e290ad70afdf97f359019afd8fb5816f4102Till MossakowskiFor a detailed explanation of the menus
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisee the \Hets User Guide \Hets user guide \cite{HetsUserGuide}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski\subsection{Relations between Common Logic Texts}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\label{relationsInCL}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\Hets supports several relations between Common Logic Texts. However only one of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskithem is defined in ISO/IEC 24707:2007 \cite{iso24a}. All the other relations are
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiunofficial extensions used e.g.\ by the Common Logic Repository COLORE \cite{Colore}.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\begin{description}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski\item[Importation] \label{descr:link_import}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski is defined in ISO/IEC 24707:2007 \cite{iso24a} as virtual copying of a
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski resource. In \Hets a whole file is ``copied'' into the importing
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski specification. Hets currently cannot handle cyclic imports. If you really need
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski them, send us a message at hets@informatik.uni-bremen.de, and we will fix it.
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Using CLIF, you can import \texttt{someFile.clif} via
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \begin{lstlisting}[language=clif]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski \end{lstlisting}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Omitting the file extension will also succeed. In this case \Hets will look
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski for a file called \texttt{someFile.clif} in first place and then for
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski \texttt{someFile.clf} in the current directory and then in the library paths.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \Hets also supports URIs for importing resources. The allowed URI schemes are
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \texttt{file:}, \texttt{http:} and \texttt{https:}.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \begin{lstlisting}[language=clif]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(cl:imports file:///absolute/path/to/someFile.clif)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(cl:imports http://someDomain.com/path/to/someFile.clif)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(cl:imports https://someDomain.com/path/to/someFile.clif)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski \end{lstlisting}
of references to resources here, as e.g. URIs.
of references to resources here, as e.g. URIs.
The example has two almost identical files, \texttt{upper.clif} and
\texttt{lower.clif}. The only difference in the actual axioms is that
\textbf{upper.clif}:
\textbf{lower.clif}:
Proofs/Auto-DG-Prover. Local proof goals (indicated by red
prover, i.e. by using the ``Prove'' menu of a red node.
| graph.(exp.dot|dot)
The \texttt{omn} option \cite{books/sp/Kohlhase06} will produce OWL files in
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 \texttt{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
(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).