51 %% Added by MB to have some extra vertical space after the ``main'' examples
52 %% following the points (and some others in the text):
135 %% Do NOT use \ASF+\SDF (it gives a superfluous space in the middle)
158 (the latter needs subscription to the mailing list)
174 {Strictly speaking, only the second feature goes beyond first-order
180 \item a parser for the Common Logic Interchange Format (CLIF) --- CLIF
185 \item a connection of CL to the higher-order provers Isabelle/HOL
191 \item a translation that eliminates the use of CL modules\footnote{Actually, we are using a revised semantics for modules, as proposed
192 recently in~\cite{NH:CommonLogicHoratio}.}. Since the semantics of CL modules
195 \item a translation of the Web Ontology Language OWL to CL;
200 For the full functionalities of \Hets, see the \Hets user guide  
206 The central idea of the Heterogeneous Tool Set (\protect\Hets) is to
209 different expansion cards can be plugged in, the expansion cards here
212 a number of expansion cards (e.g., the theorem provers Isabelle, SPASS
214 available, without the need to hard-wire each tool to the logic at
223 \Hets consists of logic-specific tools for the parsing and static
224 analysis of the different involved logics, as well as a
227 to call the logic-specific tools whenever a basic specification is
230 \Hets is based on the theory of institutions \cite{GoguenBurstall92},
231 which formalise the notion of a logic. The theory behind \Hets is laid
236 Logic and OWL2 and \HetCASL. They will be described in the next
239 \subsection{Common Logic and the Common Logic Interchange Format (CLIF)}
241 CLIF is specified in Annex A of the Common Logic standard
243 CLIF syntax, and also recursively reads in any imported files (cf.\ Sect.~\ref{relationsInCL} for the syntax).
245 Common Logic itself does not support the specification of logical
258 \Hets can directly read in OWL2 files in all syntaxes (called ``serialisations'') that the OWL API supports \cite{OWLAPI:URL}, including
259 the native OWL XML syntax \cite{w3c:owl2-xml},  the human-readable
260 Manchester 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}.
269 For heterogeneous specification, \Hets offers the Heterogeneous
276  \HetCASL generalises the structuring
280 the \Hets motherboard), as well as to heterogeneous
283 Fig.~\ref{fig:lang} for a simple subset of the
286 currently supported logics and logic translations (the latter are also
287 called comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
291 \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={<>}]
299              | spec ID = SPEC end  %% give the name ID to SPEC
311 prescribe the structure of implementations.  \emph{Specification
313 specifications. \emph{Refinements} express the fact the a specification
340 \item[OWL2] is the Web Ontology Language recommended by the
342   used for knowledge representation on the Semantic Web
345   written in Java to obtain the abstract syntax for an OWL file and its
347   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}.
350   structuring of the OWL imports is displayed as a Development Graph.
353 the zChaff SAT solver \cite{Herbstritt03} connected to it.
364     classification of the FOL problem} \cite{ZimmerAutexier06}.
366   These together comprise some of the most advanced theorem provers
367   for first-order logic. SoftFOL is essentially the first-order
373   expressing the (free) generation of datatypes.
378 \item[\Isabelle] \cite{NipPauWen02} is the logic of the interactive
383   is for first-order logic. \Hets connects THF to the automated
387   polymorphic datatypes and functions. It is closely related to the
389   embedded in the specification. For Common Logic, \HasCASL
391   to the provers Isabelle and Leo-II.
397 Various logics are supported with proof tools. Proof support for the
399 prover-supported logic. For Common Logic, the paths to SoftFOL
401 to standard first-order provers. Moreover, the paths to THF
407 An introduction to \CASL can be found in the \CASL User Manual
408 \cite{CASL-UM}; the detailed language reference is given in
409 the \CASL Reference Manual \cite{CASL/RefManual}.  These documents
410 explain both the \CASL logic and language of basic specifications as
411 well as the logic-independent constructs for structured and
412 architectural specifications.  The corresponding document explaining the
414 is the \HetCASL language summary \cite{Mossakowski04}; a formal
419 For further information on logics supported by \Hets, see the \Hets user guide  
427 target logic. More precisely, one and the same logic translation
429 each source sublogic, the corresponding sublogic of the target
432 In more detail, the following list of logic translations involving Common Logic 
462 For further information on logic translations supported by \Hets, see the \Hets 
467 The latest \Hets version can be obtained from the
473 improved constantly, it is recommended always to use the latest version.
482 For Ubuntu Lucid Lynx, enter the following into a terminal:
497   for proving in the future.
499 Then we have Java based \Hets installer that we may drop in the future.
505 double-click on the \texttt{.jar} file, but you have to install the MacPorts
509 The installer will lead you through the installation with
528 If you do not have Sun/Oracle Java, you can just download the hets binary.
531 install the above mentioned software and set
532 several environment variables, as explained on the installation page.
535 You may compile \Hets from the sources (they are licensed under GPL), 
536 please follow the
538 on the \Hets web page, download the sources (as tarball or from
539 svn), and follow the
540 instructions in the \texttt{INSTALL} file, but be prepared to take some time.
563 Consider the following Common Logic text written in CLIF:
582 Let us assume that the example is in a file named
583 \texttt{Cat-AllInOne.clif}.\footnote{This file can be found in the \texttt{CommonLogic/Examples} directory in the \Hets library \cite{hets-library:URL}.}
584 Then you can check the well-formedness of the
590 \Hets checks both the correctness of this specification
591  with respect to the CLIF syntax, as
592 well as its correctness with respect to the static semantics.
595 \item[\texttt{-p}, \texttt{-{}-just-parse}] Just do the parsing
596  -- the static analysis is skipped and no development graph is created.
597 \item[\texttt{-s}, \texttt{-{}-just-structured}] Do the parsing and the
599   leave out the analysis of basic specifications.  This can be used
601   showing the dependencies among the specifications (cf.
602   Sect.~\ref{sec:DevGraph}) even if the individual specifications are
605 Use \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
613 \Hets accepts plain text input files (for the 
614 presented logics) with the following endings:
627 Although the endings \texttt{.casl} and \texttt{.het} are
628 interchangeable, the former should be used for libraries of
629 homogeneous \CASL specifications and the latter for \HetCASL libraries
630 of heterogeneous specifications (that use the \CASL structuring
631 constructs). Within a \HetCASL library, the current logic can be changed, e.g.,
632 to Common Logic in the following way:
641 these are then automatically translated along the default
647 Common Logic CLIF texts, as in the example of \texttt{Cat-AllInOne.clif}.
649 the logic Common Logic has to be chosen explicitly, and the \CASL structuring
672 Note that the dot at the beginning of a line indicates that a new text begins.
675 This specification is the \HetCASL-structured equivalent to the following three
676 CLIF files:\footnote{Note that the ``cl:text'' syntax specified in the Common Logic standard \cite{CommonLogic:oldfashioned} has subsequently been recorded as a defect \cite{CommonLogicDefects:oldfashioned}, in favor of ``cl-text''.  \Hets supports both.}\\
703 Both can be directly used with \Hets, where the former content would be in a 
704 file with the extension \texttt{.het} and the latter in a file with one of the extensions 
705 \texttt{.clf} or \texttt{.clif}.\footnote{These files can be found in the \texttt{CommonLogic/Examples} directory in the \Hets library \cite{hets-library:URL}.} This specification is divided into three 
707 be seen in the development graph of the file.
717 called \emph{definition links}, indicating the dependency of each
724 Complementary to definition links, which \emph{define} the theories of
726 relations between different theories. Theorem links are the central
731 postulates that all axioms of the source node (including the inherited
732 ones) hold in the target node, while a local theorem link only postulates
733 that the local axioms of the source node hold in the target node.
736 i.e.\ stay within the same logic, or \emph{heterogeneous}, i.e.\ %% such that
737 the logic changes along the arrow. 
748 proof goals are indicated by marking the corresponding node in the
749 development graph as red; if all local implications are proved, the
752 of the proof calculus for heterogeneous development graphs.
754 Details can be found in the \CASL Reference Manual \cite[IV:4]{CASL/RefManual}
757 The following options let \Hets display the development graph of
760 \item[\texttt{-g}, \texttt{-{}-gui}] shows the development graph in a GUI window
764 The following additional options also apply typical rules from the development
765 graph calculus to the final graph and save applying these rules via the GUI.
767 \item[\texttt{-A}, \texttt{-{}-apply-automatic-rule}] apply the automatic
768   strategy to the development graph. This is what you usually want in order to
775 For a summary of the types of nodes and links occurring in
776 development graphs, see the \Hets user guide \cite{HetsUserGuide}.\\
778 Most of the pull-down menus of the development graph window are
780 the uDraw(Graph) documentation\footnote{see
782 The Edit menu is the only exception. 
787 Moreover, the nodes and links of the
789 holding) the right mouse button. 
790 The node menus ``Prove'' and ``Check consistency'' are the most
792 proof goals on the fly.
793 For a detailed explanation of the menus
794 see the \Hets User Guide \cite{HetsUserGuide}.
799 them, the importation, is defined in ISO/IEC 24707:2007 \cite{CommonLogic:oldfashioned}, and has a syntax within Common Logic. All the other relations are 
800 unofficial extensions used e.g.\ by the Common Logic Repository COLORE \cite{Colore}, and represented externally of Common Logic texts.  COLORE currently represents them in external XML documents, and any required symbol maps in external CLIF files.  \Hets, in contrast, allows for declaring them as \emph{views} within \HetCASL files, outside of specifications, as can be seen from the syntax specification in List.~\ref{fig:lang}.
805   resource. In \Hets a whole file is ``copied'' into the importing  
813   Omitting the file extension will also succeed. In this case \Hets will look 
815   \texttt{someFile.clf} in the current directory and then in the library paths.
825   The importation is indicated by a global definition link (black arrow) in the 
829   is formally defined in \cite{colore-fois}.  Informally, one module relatively interprets those “modules whose theorems are preserved within the current module through [a] mapping. There exists a mapping between modules such that all theorems of the other module hold in the current module after the mapping is applied.” \cite{Colore-metadata}
832   (red arrow) in the development graph.
851 \item[Non-conservative extension] is informally defined as follows:  One module non-conservatively extends other modules, if its “axioms entail new facts for the shared lexicon of the [other] module(s). [That is, the] shared lexicon between the current module and a [non-conservatively extended] module are not logically equivalent with respect to their modules.” \cite{Colore-metadata}.
853   \Hets represents non-conservative extension by a theorem link (red arrow) in the development graph.\ednote{CL: show the Hets view syntax}
863   to show other theories in the development graph, without any connection 
864   to the current theory.
866   For loading such theories, \HetCASL employs the same syntax as for loading theories that are connected to other theories, i.e.\ on loading theories, \Hets does not care about their relations:
873 (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.}
874  Names from the target file are mapped to names from the current 
875 file (including the translation file, if the relation uses one).  Note that is is possible to use cyclic relations in \Hets. Only the cyclic 
887 \texttt{lower.clif}; these can be found in the \texttt{CommonLogic/Examples} directory in the \Hets library \cite{hets-library:URL}. The only difference in the actual axioms is that 
907 The heterogeneous library \texttt{CommonLogic/Examples/SymbolMap.het} in the \Hets library \cite{hets-library:URL} establishes a mapping (actually: a relative interpretation) between these two Common Logic texts:
921 A symbol map only needs to list those names that differ between the source
922 and the target ontology; the other names (none in this concrete case) are implicitly the same.  A mapping of a single name is defined with 
925 Hence a space must be placed between the separation-comma and a name.
931 The COLORE \cite{Colore} module \texttt{Region\-Boolean\-Contact\-Algebra} relatively interprets the module \texttt{Atomless\-Boolean\-Lattice}.  These two modules specify axioms about booleans; thus, they have the same signature.  In the graph of imports, they have several common imported modules (e.g.\ \texttt{Bounded\-Distributive\-Lattice}), but no common importing module, as can be seen from Fig.~\ref{fig:colore-graph}.
941 For use with \Hets, we have made a dump of the COLORE contents available in \texttt{CommonLogic/colore} in the \Hets library \cite{hets-library:URL}.  The \HetCASL variant of expressing the relative interpretation can be found in \texttt{CommonLogic/Examples/COLORE-RelativeInterpretation}.  Here, it is not necessary to rename symbols, as both modules have the same signature.
943 For easier understanding, the \HetCASL implementation includes literal copies of the \texttt{Region\-Boolean\-Contact\-Algebra} and \texttt{Atomless\-Boolean\-Lattice} modules; actually, they could as well have been included from their respective files using \texttt{from ... get ...}.
978 This example defines a partial order twice: once as an extension of a strict partial order, and once directly.  Then, we connect both definitions by a view that expresses the relative interpretation.
980 The source is available as \texttt{CommonLogic/Examples/Partial\_Orders.het} directory in the \Hets library \cite{hets-library:URL}.
1033 Consider the following ambient assisted living (AAL) scenario:
1035   Clara instructs her \textbf{wheelchair} to get her to the \textbf{kitchen} (\textbf{\underline{next door}} to the \textbf{living room}.  For \textbf{dinner}, she would like to take a pizza from the \textbf{freezer} and bake it in the \textbf{oven}.  (Her diet is vegetarian.)  \textbf{\underline{Afterwards}} she needs to rest in \textbf{bed}.
1037 Existing ontologies for ambient assisted living (e.g.\ the OpenAAL\footnote{\url{http://openaal.org}} OWL ontology) cover the \emph{core} of these  concepts; they provide at least classes (or generic superclasses) corresponding to the concepts highlighted in \textbf{bold}.  However, that does not cover the scenario completely.  In particular, there are relevant concepts (here: space and time, \underline{underlined}), which are not covered at the required level of complexity.  OpenAAL says that appointments have a date and that rooms can be connected to each other, but not what exactly that means.  Foundational ontologies and spatial calculi, often formalized in first-order logic, cover space and time at the level of complexity required by a central controller of an apartment and by an autonomously navigating wheelchair.
1039 More concretely, Common Logic is useful in this scenario for expressing knowledge on the arrangement of rooms, e.g.\ as follows in a first-order formalization of an RCC-style spatial calculus:
1045 (“Two areas in a house (e.g.\ a working area in a room) are either the same, or intersecting, or bordering, or separated, or one is a proper part of the other.”)
1047 The following listing shows a relevant excerpt of the heterogeneous specification, which can be found 
1048 under \texttt{Ontology/Examples/AAL.het} in the \Hets library \cite{hets-library:URL}.  The key features include:
1051 \item Heterogeneous specification allows for reusing the OpenAAL OWL ontology, but at the same time formalizing a first-order spatial calculus.
1052 \item In particular, the compact representation of mutual disjointness chosen here makes use of Common Logic's sequence markers.
1053 \item As Common Logic module extends the previously imported OWL ontology, it has access to all entities of the OWL ontology by name; in particular, we can specify that two rooms are connected (in terms of the OpenAAL terminology) if certain conditions in terms of our Common Logic module, or certain conditions in terms of OpenAAL hold.
1062 %% this is the default name that Hets assigns to unnamed ontologies,
1066   %% Import the OpenAAL OWL ontology.
1092     %% make the above "or" exclusive
1097     %% (the latter would only work in OWL if we used an explicit subproperty
1099     %% and "is-door-of", but otherwise we wouldn't be able to restrict the
1117 In the previous example, we established a link between an OWL ontology and a Common Logic ontology by reusing elements of the signature of the OWL ontology (concretely: OpenAAL's \texttt{is-in-room} predicate) in the Common Logic ontology.
1119 \HetCASL's view mechanism offers an alternative to that.  A view from one ontology to another ontology in the same logic has been shown in Sect.~\ref{sec:relat-interpr}, but it is also possible to have views across logics, as long as there is a translation between these logics that is known to \Hets (cf.\ Sect.~\ref{comorphisms}).
1121 The following example, which is available as \texttt{Ontology/Examples/TimeInOWLandCL.het} in the \Hets library \cite{hets-library:URL}, establishes a view between the OWL Time ontology and its reimplementation in Common Logic, \ednote{CL: There is no way to make that explicit in \HetCASL, is there?\\ TM: you mean the datatype stuff that the OWL to CL translation generates? We should modify the translation to generate this only if really needed.\\ CL: No, I just thought (and was wrong) that \HetCASL had no way of explicitly choosing a logic translation.  But not I don't understand what \emph{you} mean.  Maybe it's related to the error that I get when loading the file; see my ticket.}using the ``OWL22CommonLogic'' translation:
1153 %% As OWL22CommonLogic is the default translation,
1161 on the Edit-menu in the development graph window and selecting 
1163 nodes in the development graph) can be eventually discharged using a theorem
1164 prover, i.e.\ by using the ``Prove'' menu of a red node.
1168 The top list on the left shows all goal names prefixed with their proof
1193 If you open this GUI when processing the goals of one node for the
1195 select those goals that should be inspected or proved. The GUI elements are the following:
1198 \item The button `Display' shows the selected goals in the ASCII syntax of
1200 \item By pressing the `Proof details' button a window is opened where for each
1201   proved goal the used axioms, its proof script, and its proof are shown ---
1202   the level of detail depends on the used theorem prover.
1203 \item With the `Prove' button the actual prover is launched. The provers are described
1204   in more detail in the \Hets user guide \cite{HetsUserGuide}.
1205 \item The list `Pick Theorem Prover:' lets you choose one of the connected
1207   zChaff, described below). By pressing `Prove' the selected prover is
1208   launched and the theory along with the selected goals is translated via the
1209   shortest possible path of comorphisms into the prover's logic.
1211   (composed) comorphism to be used for the chosen prover. If the specification
1212   does not contain any sequence markers, it is possible to use the comorphism
1215 \item Since the amount and kind of sentences sent to an ATP system is a major
1216   factor for the performance of the ATP system, it is possible to select in
1217   the bottom lists the axioms and proven theorems that will comprise the
1218   theory of the next proof attempt. Based on this selection the sublogic may
1219   vary and so do the available provers and the comorphism paths leading to provers. Former
1220   theorems that are imported from other specifications are marked with the
1222   they may be safely removed from the theory.
1223 \item If you press the bottom-right `Close' button the window is closed and
1224   the status of the goals' list is integrated into the development graph. If
1225   all goals have been proved, the selected node turns from red into green.
1230 obligation. This is done by the keyword \texttt{\%implied} at the end of a text:
1243 In this specification\footnote{\texttt{HelloWorldExamples/ToProve.het} in the \Hets library \cite{hets-library:URL}} the theorems, annotated (named) by \texttt{correct} and 
1244 \texttt{incorrect} are the ones, that can be proven or disproven.
1245 Note that they are separate texts inside the specification \texttt{ToProve}.
1246 The annotations are optional. For proving, they are the names shown in the 
1247 ``Axioms to include'' section of the prover interface 
1263 In CLIF, there is no notion of proof obligation. Hence the \texttt{\%implied} 
1264 keyword of \Hets must be used, and thus the specification is not pure CLIF. Because the texts have 
1265 names, these are also used in the prover interface. Otherwise, \Hets invents 
1270 Since proofs are void if specifications are inconsistent, the consistency
1271 should be checked (if possible for the given logic) by the ``Consistency
1273 the `Edit' menu as it operates on all nodes.
1275 The list on the left shows all node names prefixed with a consistency status
1277 a `+', a `–' indicates an inconsistent node, a `t' denotes a timeout of the last
1295 selectable from the `Pick Model finder:' list. Currently only for ``darwin''
1298 most the number of seconds given under `Timeout:' on each node. Pressing
1300 Either by `View results' or automatically the `Results of consistency check'
1301 (Fig.~\ref{fig:cons_res}) will pop up and allow you to inspect the models for
1317 \caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
1320 All ATPs integrated into \Hets share the same GUI, with only a slight
1321 modification for the MathServe Broker: the input field for extra options is
1322 inactive. Fig.~\ref{fig:SPASS_GUI} shows the instantiation for \SPASS, where
1323 in the top right part of the window the batch mode can be controlled.  The
1324 left side shows the list of goals (with status indicators).  If goals are
1325 timed out (indicated by `t') it may help to activate the check box `Include
1329 On the bottom right the result of the last proof
1332 Axioms:' is filled by \SPASS. The button `Show Details' shows the whole output
1333 of the ATP system. The `Save' buttons allow you to save the input and
1334 configuration of each proof for documentation. By `Close' the results for all
1335 goals are transferred back to the Proof Management GUI.
1339 systems; the most important systems are listed in
1341 capabilities are derived from the \emph{Specialist Problem Classes}
1342 (SPCs) defined upon the basis of logical, language and syntactical
1344 Only two of the Web services provided by the MathServe system are used
1345 by \Hets currently: Vampire and the brokering system.  The ATP systems
1347 such as SOAP, HTTP and XML.  Currently, the ATP system Vampire may be
1348 accessed from \Hets via MathServe; the other systems are only reached
1374         exhaustive, but only the most appropriate problem classes are
1384 For details on the ATPs supported, see the \Hets user guide \cite{HetsUserGuide}.
1396 like the simplifier or the tableaux prover, are built on top of this
1412 It is essential to be aware of the fact that the \Isabelle/\HOL logic
1413 is different from the logics that are encoded into it via comorphisms.
1414 Therefore, the formulas appearing in subgoals of proofs with \Isabelle
1415 will not conform to the syntax of the original input logic.  They may
1422 The \Isabelle theory file conforms to the Isabelle/Isar syntax
1423 \cite{NipPauWen02}. It starts with the theory (encoded along the selected
1424  comorphism), followed by a list of theorems. Initially, all the
1425  theorems have trivial proofs, using the `oops` command. However, if
1427  the generated \Isabelle theory file, ensuring that your previous work
1430  now can replace the 'oops' commands with real \Isabelle proofs, and
1431  use Proof General to step through the proofs. You finish your session
1432  by saving your file (using the Emacs file menu, or the Ctrl-x Ctrl-s
1439 \Hets provides several options controlling the types of files
1443   as explicit type of the input file. 
1496 avoiding the need to re-analyse downloaded libraries. \texttt{prf} files
1497 can also be stored or loaded via the GUI's File menu.
1511 The \texttt{xml} option will produce an XML-version of the development graph
1514 The \texttt{exp} format is the new experimental omdoc format.
1519 When the \texttt{thy} format is selected, \Hets will try to translate
1520 each specification in the library to \Isabelle, and write one \Isabelle
1523 When the \texttt{comptable.xml} format is selected, \Hets will extract
1524 the composition and inverse table of a Tarskian relation algebra from
1525 specification(s) (selected with the \texttt{-n} or \texttt{-{}-spec}
1526 option). It is assumed that the relation algebra is
1527 generated by basic relations, and that the specification is written
1528 in the \CASL logic. A sample specification of a relation
1529 algebra can be found under \texttt{Calculi/Space/RCC8.het} in the \Hets library \cite{hets-library:URL}.
1530 The output format is XML, the URL of the DTD is included in the
1547 into \LaTeX\ documents, provided that the style \texttt{hetcasl.sty}
1548 coming with the \Hets distribution (\texttt{LaTeX/hetcasl.sty}) is used.
1554 The \texttt{dfg} format is used by the \SPASS theorem prover
1563 For all output formats it is recommended to increase the verbosity to at least
1564 level 2 (by using the option \texttt{-v2}) to get feedback which files are
1588   with \Hets in interactive mode by listening to the port \texttt{PORT}
1591   with \Hets in interactive mode via connecting to the port on host
1596   (i.e.\ \texttt{-d LogicGraph} lists the logics and comorphisms)
1603 \url{http://pollux.informatik.uni-bremen.de:8000/}. It allows to browse the
1606 where the \texttt{svg} format is supposed to look like the graphs displayed by
1607 uDrawGraph. Besides browsing, the web server is supposed to be accessed by
1611 For details on this topic, see the \Hets user guide \cite{HetsUserGuide}.
1617 Set the verbosity level according to \texttt{Int}. Default is 1.
1623 \item[\texttt{+RTS -KIntM -RTS}] Increase the stack size to
1625 This must be the first option.
1626 \item[\texttt{-l LOGIC}, \texttt{-{}-logic=LOGIC}] chooses the initial logic, which is used for processing the specifications before the first \textbf{logic L}
1630 \item[\texttt{-{}-relative-positions}] Just uses the relative library name in positions of warning or errors.

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