16 pdftitle={Hets User Guide}]
71 \newcommand     {\Hets}{\normalTEXTSC{H}{ETS}\xspace}
149 The central idea of the Heterogeneous Tool Set (\protect\Hets) is to
151 integration and proof management. One can think of \Hets acting like a
155 their analysis and proof tools can be plugged into the \Hets
157 \cite{GoguenBurstall92}.  The \Hets motherboard already has plugged in
166 \caption{The \Hets motherboard and some expansion cards}
169 \Hets supports a number of input languages directly, such as \CASL,
171 specification, \Hets offers the language heterogeneous \CASL.
176 the \Hets motherboard), as well as to heterogeneous
184 degree of support by \Hets in Fig.~\ref{fig:Languages}.
219 \Hets consists of logic-specific tools for the parsing and static
226 \Hets is based on the theory of institutions \cite{GoguenBurstall92},
227 which formalize the notion of a logic. The theory behind \Hets is laid
228 out in \cite{Habil}. A short overview of \Hets is given in
232 \section{Logics supported by Hets}
235 \cite{GoguenBurstall92}) is currently supported by \Hets:
241 \caption{Graph of logics currently supported by \Hets. The more an
287 \caption{Current degree of \Hets support for the different languages. Languages without prover can still ``borrow'' provers
336   implementation language of \Hets. As a logic we only supports the older
337   Haskell 98 standard.  Yet, in principle, \Hets might be applied to itself --
353 Hets calls an external OWL 2 parser
358  Hets only supports the last two, more restricted variants.
401   what TPTP is for (untyped) first-order logic. \Hets connects THF to the
428 \item [LF] is the dependent type theory of Twelf \url{http://twelf.plparty.org/}. Hets
431       Moreover, LF can be used as a logical framework to add new logics in Hets \cite{CHK+2011a}.
449   of these specifications Hets provides connections to the computer
456 combine the standard properties of hybrid logics with any logic already integrated in Hets.
481 by Hets}
497 \caption{Graph of most important sublogics currently supported by \Hets,
503 supported by \Hets:
571 The latest \Hets version can be obtained from the
572 \Hets tools home page
576  Since \Hets is being
579 \Hets is currently available (on Intel architectures only) for Linux
582 There are several possibilities to install \Hets.
600 Hets-lib & specification library & \url{http://www.cofi.info/Libraries}\\\hline
619 \item For Mac OSX we provide disk images \texttt{Hets-<date>.dmg} without GTK support.
622 You may compile \Hets from the sources (they are licensed under GPL),
624 link ``Hets: source code and information for developers''
625 on the \Hets web page, download the sources (as tarball or from
676 \Hets can be used for parsing and
685 with the \Hets distribution as \texttt{Hets-lib/UserManual/Chapter3.casl}).
692 \Hets checks both the correctness of this specification
711 calling \Hets).
738 \Hets accepts plain text input files with the following endings:
757 command line option of \Hets. In all other cases \texttt{.xml} files are
890 The following options let \Hets show the development graph of
940 Again, these specifications can be checked with \Hets. However, this
955 \Hets now displays a so-called development graph
1040 \Hets now displays a more complex development graph, see Fig.~\ref{fig:dg1}.
1192   window, if the library graph window has been closed after \Hets has been
1200  \Hets and thus the action performed on the graph are saved.
1294   currently supported by \Hets. The Edit menu of a logic graph window has the
1306 \Hets provides several options controlling the types of files
1323   \Hets in interactive mode.  (\texttt{gen\_trm} formats are currently not
1387 save to. If the file does not yet exist, \Hets will create it.
1392 found at \url{https://github.com/spechub/Hets/blob/master/Persistence/database_postgresql.yml}}
1399 When the \texttt{thy} format is selected, \Hets will try to translate
1403 When the \texttt{comptable.xml} format is selected, \Hets will extract
1409 algebra can be found in the \Hets library \texttt{Calculi/Space/RCC8.het},
1429 coming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
1460 \item[\texttt{-I}, \texttt{--interactive}] run \Hets in interactive mode
1462 \item[\texttt{-X}, \texttt{--server}] run \Hets as web server (see
1466   \Hets in interactive mode
1469   with \Hets in interactive mode vy listining to the port \texttt{PORT}
1472   with \Hets in interactive mode via connecting to the port on host
1480 \section{Hets as a web server}\label{sec:Server}
1482 Large parts of \Hets are now also available via a web interface. A running
1485 \Hets library, upload a file or just a \HetCASL specification. Development
1554 \section{Proofs with \Hets}\label{sec:Proofs}
1572 \caption{Hets Goal and Prover Interface\label{fig:proof_window}}
1623 \caption{Hets Consistency Checker Interface\label{fig:cons_window}}
1652 All ATPs integrated into \Hets share the same GUI, with only a slight
1677 by \Hets currently: Vampire and the brokering system.  The ATP systems
1680 accessed from \Hets via MathServe; the other systems are only reached
1789  you have saved earlier proof attempts, \Hets will patch these into
1842 in CNF. It is connected as a prover for propositional logic to \Hets. The prover
1851 current integration of zChaff into \Hets has been tested with zChaff 2004.11.15.
1870 is needed to run Pellet. For the integration into \Hets the environment variable
1877 C++. Fact++ is integrated into \Hets via the OWL-API, which is written in Java.
1937 Eprover is needed to be in the system-path, if Darwin is used with \Hets, since
1954 \section{Limits of Hets}
1956 \Hets is still intensively under development. In particular, the
1969 \section{Architecture of Hets}
1971 The architecture of \Hets is shown in Fig.~\ref{fig:hets}.
1975 \Hets provides an abstract interface for
2034 The logic-independent modules in \Hets can be found in the right half
2036 \Hets' 100.000 lines of Haskell code.
2065 \Hets can store development graphs, including their proofs.
2066 Therefore, \Hets uses the so-called
2073 of the \Hets home page at \url{http://www.dfki.de/sks/hets}.
2087 \Hets is mainly maintained by
2101 If your favourite logic is missing in \Hets, please tell us
2103 when deciding which logics and proof tools to integrate next into \Hets. Help
2104 with integration of more logics and proof tools into \Hets is also welcome.
2107 The heterogeneous tool set \Hets would not have possible
2110 in the implementation of \Hets:
2162 \Hets has been built based on experiences with its
2186 for giving feedback about \Cats, HOL-CASL and \Hets. Finally,
2188 for help with connecting \Hets to their UniForM workbench.

Indexes created Tue Jul 24 14:28:13 CEST 2018