34 pdftitle={Hets for Common Logic Users}]
152 \title{{\bf \protect{\LARGEHets} for Common Logic Users}\\
168 Common Logic (CL) is an ISO standard published as ``ISO/IEC 24707:2007
169 --- Information technology — Common Logic (CL): a framework for a family
178 several kinds of tool support for Common Logic:
180 \item a parser for the Common Logic Interchange Format (CLIF) --- CLIF
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
245 Common Logic itself does not support the specification of logical
320 \Hets supports a variety of different logics.   The following are most important for use with Common Logic:
327 \caption{Graph of logics related to Common Logic that are currently supported by \Hets.}
334 \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
335 logic in several ways.   The Common Logic
337   Logic.  \Hets currently only supports parsing CLIF. If you need
375 For Common Logic, \CASL can be seen as kind of transitional hub, linking
376 Common Logic to other logics, most importantly SoftFOL.
389   embedded in the specification. For Common Logic, \HasCASL
399 prover-supported logic. For Common Logic, the paths to SoftFOL
422 \section{Logic translations supported by Hets}
425 Logic translations (formalised as institution comorphisms
432 In more detail, the following list of logic translations involving Common Logic 
436 CommonLogic2CASL & Coding Common Logic to \CASL. Module elimination
438 CommonLogic2CASLCompact & Coding compact Common Logic to \CASL. 
439 			  Compact Common Logic is a sublogic of Common Logic
444 CommonLogicModuleElimination & Eliminating modules from a Common Logic theory 
459 Common Logic to SoftFOL with \texttt{CommonLogic2CASLCompact;CASL2SoftFOLInduction} 
460 since there is no prover for Common Logic or \CASL.
563 Consider the following Common Logic text written in CLIF:
632 to Common Logic in the following way:
639 Common Logic specifications. Within such specifications,
642 embedding of \CASL into Common Logic (cf.\ Fig.~\ref{fig:LogicGraph}).
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
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.}\\
796 \subsection{Relations between Common Logic Texts}
798 \Hets supports several relations between Common Logic Texts. However only one of
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}.
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.}
881 This section introduces several typical examples of using Common Logic ontologies with \Hets.
886 This example has two almost identical Common Logic texts, \texttt{upper.clif} and 
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:
924 separated by commas. Note that in Common Logic, a comma can be part of a name.
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:
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.
1114 \subsubsection{Heterogeneous Views from OWL to Common Logic}
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.
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:
1311 {Automated Theorem Proving Systems\\(Logic SoftFOL)}
1392 Common Logic theories involving sequence markers.
1502 The \texttt{clif} option will produce Common Logic files in
1503 CLIF dialect for each specification of a Common Logic library.
1509 state, Common Logic theories can be exported to and imported from OMDoc.

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