34 %% following the points (and some others in the text):
151 integration and proof management. One can think of \Hets acting like a
153 expansion cards here being individual logics (with their analysis and
154 proof tools) as well as logic translations.  Individual logics and
155 their analysis and proof tools can be plugged into the \Hets
159 and more, as well as model finders). Hence, a variety of tools is
166 \caption{The \Hets motherboard and some expansion cards}
170 Common Logic, OWL 2, LF, THF, HOL, Haskell, and Maude. For heterogeneous
175 (if they are formalised as institutions and plugged into
182 currently supported logics and logic translations (the latter are also
183 called comorphisms) is shown in Fig.~\ref{fig:LogicGraph}, and the
206 \texttt{BASIC-SPEC} and \texttt{SYMBOL-MAP} have a logic
213 combine and rename specifications, hide parts thereof, and also
216   libraries} are collections of named structured and architectural
219 \Hets consists of logic-specific tools for the parsing and static
221 logic-independent parsing and static analysis tool for structured and
222 architectural specifications and libraries. The latter of course needs
294   functions and subsorting.  It also provides induction sentences,
296 %It is mainly designed and used for the
299 %Linguistic and Cognitive Engineering), an Upper Ontology for knowledge
301 %specify calculi for time and space.
308 integration of \CASL extensions and keeps the effort of integrating
312 suited for the specification of process types and reactive systems.
316  is an extension of \CASL with multi-modalities and
321 \item[ExtModal] is an extended modal logic, subsuming and replacing ModalCASL.
322   It features -- apart from multiple modalities and dynamic logic -- also time
323   (and term) modalities, grading, hybrid modal logic, and the $\mu$-calculus
324   \cite{Codruta10}. Comorphisms to CASL and THF have been implemented.
327   polymorphic datatypes and functions. It is closely related to the
328   programming language Haskell and allows program constructs being
334 \item[Haskell] is a modern, pure and strongly typed functional programming
351   used for knowledge representation and the Semantic Web
354   written in JAVA to obtain the abstract syntax for an OWL file and its
356   the OWL ontology into the sublanguages OWL Full, OWL DL and OWL
366   \CASL with cardinality restrictions for the description of sorts and
368   between \CASLDL, OWL and \SHOIN. Compared to \CASL only unary
369   and binary predicates, predefined datatypes and concepts (subsorts
370   of the topsort Thing) are allowed. It is used to bring OWL and
389 \item E-KRHyper \cite{DBLP:conf/cade/PelzerW07}, see \url{http://www.uni-koblenz.de/~bpelzer/ekrhyper}, and
402   automated higher-order provers Leo-II, Satallax and Isabelle's nitpick,
403   refute and sledgehammer.
423   \verb+full-maude.maude+, \verb+hets.prj+, \verb+maude2haskell.maude+ and
430       \verb+TWELF_LIB+ must be set) and reads in the OMDoc generated by Twelf.
433       and therefore the environment variable \verb+LATIN_LIB+ must be set to the
450   algebra systems Mathematica, Maple and Reduce.
452 the characteristic features of hybrid logic, both at the level of syntax and semantics. A comorphism from HybridCASL
457 Some manual intervention is still required: a parser and a semantics analyser for the sentences of the base
460 Propositional, CASL, CoCASL, and any other logic already hybridised.
471 explain both the \CASL logic and language of basic specifications as
472 well as the logic-independent constructs for structured and
486 target logic. More precisely, one and the same logic translation
487 may have several source and target \emph{sub}logics: for
490 A graph of the most important logics and sublogics, together with their
514 CASL2PCFOLTopSort & coding of subsorting (SulPeCFOL=) by a top sort and unary
580 and with limited functionality for Mac OSX.
624 link ``Hets: source code and information for developers''
626 svn), and follow the
630 Depending on your application further tools are supported and may be
676 \Hets can be used for parsing and
697 whether the use of overloaded symbols is unambiguous, and so on).
701  -- the static analysis is skipped and no development is created.
702 \item[\texttt{-s}, \texttt{--just-structured}] Do the parsing and the
720     operations and predicates.
726     complete and usually takes longer than the full cell condition
760 Although the endings \texttt{.casl} and \texttt{.het} are
762 homogeneous \CASL specifications and the latter for \HetCASL libraries
771 The subsequent specifications are then parsed and analysed as
781 for the data part and a \Csp process built over this data part.
815 Haskell programs % and HasSLe specifications,
816 and hence supports the Haskell module system.
818 the logic Haskell has to be chosen explicitly, and the \CASL structuring
835 declarations and definitions need to start with the first column of
844 structured theorem proving and proof management.
847 structured specifications or parts thereof), and a set of arrows
850 associated with a signature and some set of local axioms.  The axioms
866 Both definition and theorem links can be \emph{homogeneous},
876 into simpler (local and global) ones. Theorem links that have been
884 on a theorem \cite{Habil} stating soundness and relative completeness
888 and in \cite{Habil,MossakowskiEtAl05,MossakowskiEtAl07b}.
898 graph calculus to the final graph and save applying these rule via the GUI.
904   with incoming hiding links. (This may take long and may not be implemented
941 only checks syntactic and static semantic well-formedness -- it is
952 (assuming that the above two specifications and the view
1059 (corresponding to the extensions and unions in the
1064 In this way, we can see that both  \NAMEREF{List\_Order\_Sorted}  and
1076 proof obligation between \NAMEREF{List\_Order\_Sorted}  and
1081 Here is a summary of the types of nodes and links occurring in
1108   one and the same logic).
1118 The exception is the Edit menu. Moreover, the nodes and links
1153 the nodes are identified by the internal node number and the internal node name.
1160 three categories: definition links, proven theorem links and unproven
1168   Isabelle-refute, darwin and E-KRHyper, with best support for darwin.
1174   local and global (definition or theorem) links is stable, support
1175   for hiding links and checking conservativity is still experimental.
1179   proof goals, that is, they become green, and instead, some target nodes
1182   a colimit approximation for the development graph and for
1200  \Hets and thus the action performed on the graph are saved.
1209   node name and node number, the xpath that denotes the location of the node
1211   origin of the node and the local theory i.e. axioms declared locally.
1225 \item[Show proof status] Show open and proven local proof goals.
1233 \item[Disprove] Negates selected goals and tries to disprove them using
1239   (possibly named) sentence will be parsed and analysed using the underlying logic.
1251 Show proof status} and {\bf Prove} and moroever, the option {\bf Show
1259 \item[Show info] Shows informations about the edge: internal number and
1260 internal nodes it links, the link type and origin and the
1262 of two components: a logic translation and a signature morphism in the
1271 nodes which are not displayed and it expands the path to the links forming it.
1282   and restarting the application after sources have changed. However, all
1291   original state and proof steps will be lost, therefore you have to confirm
1293 \item[Show Logic Graph] Shows the graph of logics and logic comorphisms
1297 \item[Show detailed logic graph] Shows the important sublogics and comorphims
1298   between them, i.e. translation (blue links) and inclusion (black links).
1304 \section{Reading, Writing and Formatting}
1307 that are read and written.
1314   always be read if it exists and is consistent (aka newer) than the
1367 The \texttt{env} and \texttt{prf} formats are for subsequent reading,
1375 markup format and data model for Open Mathematical Documents. It
1376 serves as semantics-oriented representation format and ontology
1389 \texttt{--database-config=FILEPATH} and \texttt{--database-subconfig=KEY}
1400 each specification in the library to \Isabelle, and write one \Isabelle
1404 the composition and inverse table of a Tarskian relation algebra from
1407 generated by basic relations, and that the specification is written
1477   (i.e.\ \texttt{-d LogicGraph} lists the logics and comorphisms)
1493 and the slash of the URL, i.e.\
1499 mark and consists of \emph{entries} (usually field-value pairs) separated by
1505 cases the field name or the value may be omitted and in that case the equal
1510 formats, like \texttt{pdf}, only pretty print specification and
1519 Given a graph, nodes and edges can be addressed by numbers via entries like
1526 goals can be given via a \texttt{theorems} field and special translations by a
1527 \texttt{translation} field. The available provers and translations can be
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
1539 \item[\texttt{-V}, \texttt{--version}] Print version number and exit.
1541 Print usage information and exit.
1565 indicates a disproved goal, a space denotes an open goal, and a
1572 \caption{Hets Goal and Prover Interface\label{fig:proof_window}}
1583   proved goal the used axioms, its proof script, and its proof are shown ---
1588   provers (among them \Isabelle, MathServe Broker, \SPASS, Vampire, and
1590   launched and the theory along with the selected goals is translated via the
1594 \item Since the amount and kind of sentences sent to an ATP system is a major
1596   the bottom lists the axioms and proven theorems that will comprise the
1598   vary and also the available provers and comorphisms to provers. Former
1602 \item If you press the bottom-right `Close' button the window is closed and
1633 (Fig. \ref{fig:cons_res}) will pop up and allow you to inspect the models for
1658 preceeding proven theorems in next proof attempt' and pressing `Prove all'
1665 of the ATP system. The `Save' buttons allow you to save the input and
1674 (SPCs) defined upon the basis of logical, language and syntactical
1675 properties by Sutcliffe and Suttner \cite{SutcliffeEA:2001:EvalATP}.
1677 by \Hets currently: Vampire and the brokering system.  The ATP systems
1678 are offered as Web Services using standardized protocols and formats
1679 such as SOAP, HTTP and XML.  Currently, the ATP system Vampire may be
1721 predicates. The ATP \SPASS should be installed locally and available
1727 Competitions (CASC) (2002--2006) in the devisions \verb,FOF, and
1729 of ordered binary resolution and superposition for handling equality.
1737 % The classes ``effectively propositional'' and ``real first-order''
1744 upon a classification based on the SPCs, and on a training with the
1747 has been introduced by Sutcliffe and Suttner for the annual
1748 competition CASC \cite{Sutcliffe:2006:CASC} and provides a unified
1758 has a very small core guaranteeing correctness, and its provers,
1761 and several mathematical textbooks have been partially
1793  now can replace the 'oops' commands with real \Isabelle proofs, and
1796  key sequence), and by exiting Emacs (Ctrl-x Ctrl-c).
1804 for specification and verification of imperative programs.
1811 language, and $\varphi$ is a dynamic logic formula.
1829 on'' and ``specification''. Besides the builtin specification ``boolean''
1908 prover and model finder based on the Hyper Tableaux Calculus\cite{Baumgartner:1996}.
1933 Darwin is an automatic first order prover and model finder implementing the Model
1965 support for hiding links and for conservativity.
1981 a static checker and a prover for basic specifications in the logic have
2017 \caption{The basic ingredients of logics and logic comorphisms}
2023 \cite{PeytonJones03} by a set of types and functions, see
2041 \cite{Parsec}.  Logic and translation names are looked up in the logic
2044 the current logic, and which is updated if an explicit specification
2053 specifications, and transforms an abstract syntax tree to a
2056 the static analysis of basic specifications) and/or translates (along
2057 the intra- and inter-logic translations) the theory, while
2058 simultaneously adding nodes and links to the development graph.
2072 and in the overview of modules provided in the developers section
2088 Christian Maeder (Christian.Maeder@dfki.de) and Till Mossakowski
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.
2159 Zicheng Wang, and
2165 \Cats and
2170 provides parsing and static analysis for \CASL.
2172 of Mark van den Brand, Kolyang, Bartek Klin, Pascal Schmidt and
2177 graphs without hiding and without logic translations.  \MAYA has been
2178 developed by Serge Autexier and Dieter Hutter.
2185 Konstantin Tchekine and Stefan W\"olfl
2186 for giving feedback about \Cats, HOL-CASL and \Hets. Finally,
2187 special thanks to Christoph L\"uth and George Russell

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