177 The Heterogeneous Tool Set (\Hets) is an open source software providing
204 \section{The Heterogeneous Tool Set and Its Input Languages}
206 The central idea of the Heterogeneous Tool Set (\protect\Hets) is to
211 as logic translations. The \Hets motherboard already has plugged in
220 \caption{The \Hets motherboard and some expansion cards}
226 architectural specifications and libraries. The latter of course needs
231 which formalise the notion of a logic. The theory behind \Hets is laid
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}.
285 specifications or modules written in a specific logic.  The graph of
320 \Hets supports a variety of different logics.   The following are most important for use with Common Logic:
335 logic in several ways.   The Common Logic
346   imports. The Java parser also does a first analysis classifying
349 The
412 architectural specifications.  The corresponding document explaining the
467 The latest \Hets version can be obtained from the
481 The best support is currently given via Ubuntu packages.
509 The installer will lead you through the installation with
593 The following flags are available in this context:
638 The subsequent specifications are then parsed and analysed as
646 The endings \texttt{.clf} and \texttt{.clif} are available for directly reading in
719 associated with a signature and some set of local axioms.  The axioms
740 The \emph{proof calculus} for development graphs
745 be proved by turning them into \emph{local proof goals}.  The latter
757 The following options let \Hets display the development graph of
764 The following additional options also apply typical rules from the development
782 The Edit menu is the only exception. 
790 The node menus ``Prove'' and ``Check consistency'' are the most
817   \Hets also supports URIs for importing resources. The allowed URI schemes are
825   The importation is indicated by a global definition link (black arrow) in the 
834   The \HetCASL syntax for relative interpretations is
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:
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.
980 The source is available as \texttt{CommonLogic/Examples/Partial\_Orders.het} directory in the \Hets library \cite{hets-library:URL}.
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:
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:
1159 The proof calculus for development graphs (Sect.~\ref{sec:DevGraph}) reduces
1166 The graphical user interface (GUI) for calling a prover is shown in
1168 The top list on the left shows all goal names prefixed with their proof
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
1203 \item With the `Prove' button the actual prover is launched. The provers are described
1205 \item The list `Pick Theorem Prover:' lets you choose one of the connected
1210 \item The pop-up choice box below `Selected comorphism path:' lets you pick a
1246 The annotations are optional. For proving, they are the names shown in the 
1250 The same specification can be written down in CLIF:
1275 The list on the left shows all node names prefixed with a consistency status
1323 in the top right part of the window the batch mode can be controlled.  The
1330 attempt is displayed.  The `Status:' indicates `Open', `Proved', `Disproved',
1331 `Open (Time is up!)', or `Proved (Theory inconsistent!)'. The list of `Used
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
1337 The MathServe system \cite{ZimmerAutexier06} developed by J\"{u}rgen
1345 by \Hets currently: Vampire and the brokering system.  The ATP systems
1373       {The list of problem classes for each ATP system is not
1388 The main interative theorem proving system integrated into \Hets is
1404 The main \Isabelle logic (called Pure) is some weak intuitionistic type
1405 theory with polymorphism. The logic Pure is used to represent a
1422 The \Isabelle theory file conforms to the Isabelle/Isar syntax
1450   proof scripts. The contents of a \texttt{hpf} file must be valid input for
1454 The possible input types are:
1495 The \texttt{env} and \texttt{prf} formats are for subsequent reading,
1499 The \texttt{omn} option \cite{w3c:owl2-manchester} will produce OWL files in
1502 The \texttt{clif} option will produce Common Logic files in
1505 The \texttt{omdoc} format \cite{books/sp/Kohlhase06} is an XML-based
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.
1516 The \texttt{hs} format is used for Haskell modules. Executable \CASL or
1530 The output format is XML, the URL of the DTD is included in the
1533 The \texttt{sig} or \texttt{th} option will create \HetCASL signature or
1534 theory files for each development graph node. (The \texttt{.delta} extension
1537 The \texttt{pp} format is for pretty printing, either as plain text
1550 The format \texttt{pp.xml} represents just a parsed library in XML.
1554 The \texttt{dfg} format is used by the \SPASS theorem prover
1557 The \texttt{tptp} format (\url{http://www.tptp.org}) is a standard
1608 other programs using queries. The possible queries are described at
1627 declaration. The default is \CASL.
1628 \item[\texttt{-e ENCODING}, \texttt{-{}-encoding=ENCODING}] Read input files using latin1 or utf8 encoding. The default is still latin1.

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