33 %% Added by MB to have some extra vertical space after the ``main'' examples
184 degree of support by \Hets in Fig.~\ref{fig:Languages}.
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
349 \item[OWL 2] is the Web Ontology Language (OWL 2) recommended by the
430       \verb+TWELF_LIB+ must be set) and reads in the OMDoc generated by Twelf.
451 \item[Hybrid] HybridCASL \cite{DBLP:conf/calco/NevesMMB13} extends ModalCASL by implementing
464 other logics can be obtained by using logic translations to a
481 by Hets}
497 \caption{Graph of most important sublogics currently supported by \Hets,
503 supported by \Hets:
513 CASL2PCFOL & coding of subsorting (SubPCFOL=) by injections, see Chap.\ III:3.1 of the CASL Reference Manual \cite{CASL/RefManual} \\\hline
514 CASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
522 CASL2SubCFOL & coding of partial functions by error elements
528 CoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
529 CoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to  CASL2SubCFOL \\\hline
609 A daily snapshot of \texttt{hets} can be installed by:
614 In case the binary (under \texttt{/usr/lib/hets/hets}) is broken it can be replaced manually or by reverting an update:
687 specification by typing (into some shell):
756 logic is set to DMU before a library import or by the ``\texttt{-l DMU}''
758 assumed to be development graph files as produced by ``\texttt{-o xml}''.
874 \cite{MossakowskiEtAl05,Habil} is given by rules
875 that allow for proving global theorem links by decomposing them
878 be proved by turning them into \emph{local proof goals}.  The latter
879 can be discharged using a logic-specific calculus as given by an
881 proof goals are indicated by marking the corresponding node in the
944 by a strict partial ordering relation. Checking this requires theorem
968 Arrows show how specifications are related by the structuring
972 specifications (generated by the extension), while the red arrow
1004 The following specification of sorting by insertion also is taken from
1138 Initially, the complexity of the graph is reduced by hiding all these nodes;
1153 the nodes are identified by the internal node number and the internal node name.
1196  which can be later read by uDrawGraph.
1199  to the current development graph in a .hpf file which can be later read by
1215 are not part of the theory; they can be made visible only by re-adding
1216 the hidden symbols, using the normal form of the node, by calling
1294   currently supported by \Hets. The Edit menu of a logic graph window has the
1407 generated by basic relations, and that the specification is written
1421 \LaTeX\ version of \texttt{Order.casl} by typing:
1435 The \texttt{dfg} format is used by the \SPASS theorem prover
1442 consistency checks by SPASS or Darwin respectively.
1445 level 2 (by using the option \texttt{-v2}) to get feedback which files are
1487 where the \texttt{svg} format is supposed to look like the graphs displayed by
1488 uDrawGraph. Besides browsing, the web server is supposed to be accessed by
1492 A development graph is addressed by the \emph{path} following the port number
1498 A \emph{path} may be followed by a query string that begins with a question
1499 mark and consists of \emph{entries} (usually field-value pairs) separated by
1501 development graph given by the \emph{path} or they allow to perform commands
1509 \texttt{pdf}, etc., do not need to be preceded by \texttt{format=}.  Some
1514 session id for a development graph that is given by a file name, i.e.\
1519 Given a graph, nodes and edges can be addressed by numbers via entries like
1520 \texttt{node=0} or \texttt{edge=0}. (Nodes can also be given by name.)  For
1521 nodes, prover actions are possible by further
1526 goals can be given via a \texttt{theorems} field and special translations by a
1528 queried by \texttt{?node=0\&translations} and \texttt{?node=0\&provers} or
1529 shorter by \texttt{?translations=0} and \texttt{?provers=0}, where instead of
1557 global theorem links to local proof goals. Local proof goals (indicated by red
1559 prover, i.e. by using the ``Prove'' menu of a red node.
1564 status in square brackets. A proved goal is indicated by a `+', a `-'
1611 should be checked (if possible for the given logic) by the ``Consistency
1616 in square brackets that is initially empty.  A consistent node is indicated by
1632 Either by `View results' or automatically the `Results of consistency check'
1657 timed out (indicated by `t') it may help to activate the check box `Include
1664 Axioms:' is filled by \SPASS. The button `Show Details' shows the whole output
1669 The MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
1675 properties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
1676 Only two of the Web services provided by the MathServe system are used
1677 by \Hets currently: Vampire and the brokering system.  The ATP systems
1707         named according to benchmark tests made with MathServe by
1711   \caption{ATP systems provided as Web services by MathServe}
1732 for detailed information. The connection to Vampire is achieved by
1738 % apply to first-order problems that are distinguished by the finiteness
1740 % only constants (generated by finitely many terms) whereas a real
1747 has been introduced by Sutcliffe and Suttner for the annual
1787  comorphism), followed by a list of theorems. Initially, all the
1795  by saving your file (using the Emacs file menu, or the Ctrl-x Ctrl-s
1796  key sequence), and by exiting Emacs (Ctrl-x Ctrl-c).
1834 The state created by VSE will be stored in a \texttt{.tar} file (within the
1906 KRHyper\footnote{\url{http://www.uni-koblenz.de/~wernhard/krhyper/}} by
1910 implementation we use a default tactics script, that can be influenced by the user.
1925 a long list of all available parameters. You can exit E-KRHyper by the command
2023 \cite{PeytonJones03} by a set of types and functions, see
2048 by just using the logic-specific parser of the current logic as
2087 \Hets is mainly maintained by
2171 It has been developed by the first author with help
2178 developed by Serge Autexier and Dieter Hutter.

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