Lines Matching defs:of
97 %%%%% end of Klaus macros
149 The central idea of the Heterogeneous Tool Set (\protect\Hets) is to
151 integration and proof management. One can think of \Hets acting like a
158 a number of expansion cards (e.g., the theorem provers Isabelle, SPASS
159 and more, as well as model finders). Hence, a variety of tools is
169 \Hets supports a number of input languages directly, such as \CASL,
173 constructs of
177 combination of specification written in different logics.
179 Fig.~\ref{fig:lang} for a simple subset of the
181 specifications or modules written in a specific logic. The graph of
184 degree of support by \Hets in Fig.~\ref{fig:Languages}.
204 \caption{Syntax of a simple subset of the heterogeneous
207 specific syntax, while \texttt{ID} stands for some form of
215 prescribe the structure of implementations. \emph{Specification
216 libraries} are collections of named structured and architectural
219 \Hets consists of logic-specific tools for the parsing and static
220 analysis of the different involved logics, as well as a
222 architectural specifications and libraries. The latter of course needs
226 \Hets is based on the theory of institutions \cite{GoguenBurstall92},
227 which formalize the notion of a logic. The theory behind \Hets is laid
228 out in \cite{Habil}. A short overview of \Hets is given in
234 The following list of logics (formalized as so-called institutions
241 \caption{Graph of logics currently supported by \Hets. The more an
242 ellipse is filled with green, the more stable is the implementation of the logic. Blue indicates a prover-supported logic.}
287 \caption{Current degree of \Hets support for the different languages. Languages without prover can still ``borrow'' provers
295 expressing the (free) generation of datatypes.
297 %specification of requirements for software systems. But it is also
298 %used for the specification of \Dolce (Descriptive Ontology for
304 We have implemented the \CASL logic in such a way that much of the
308 integration of \CASL extensions and keeps the effort of integrating
311 \item[CoCASL] \cite{MossakowskiEA04} is a coalgebraic extension of \CASL,
312 suited for the specification of process types and reactive systems.
316 is an extension of \CASL with multi-modalities and
317 term modalities. It allows the specification of modal systems with
319 certain forms of dynamic logic.
326 \item[HasCASL] is a higher order extension of \CASL allowing
330 An overview of \HasCASL is given in \cite{Schroeder:2002:HIS};
336 implementation language of \Hets. As a logic we only supports the older
341 \item[CspCASL] \cite{Roggenbach06} is a combination of \CASL
347 of qualitative constraint calculi.
360 structuring of the OWL imports is displayed as Development Graph.
363 is an extension of a restriction of \CASL, realizing
364 a strongly typed variant of OWL in \CASL syntax.
366 \CASL with cardinality restrictions for the description of sorts and
370 of the topsort Thing) are allowed. It is used to bring OWL and
392 classification of the FOL problem} \cite{ZimmerAutexier06}.
394 These together comprise some of the most advanced theorem provers
414 \item[DMU] is a dummy logic to read output of ``Computer Aided
417 \item[FreeCAD] is a logic to read design files of the CAD system
426 \item[DFOL] is an extension of first-order logic with dependent types \cite{rabe:dfol:06}.
428 \item [LF] is the dependent type theory of Twelf \url{http://twelf.plparty.org/}. Hets
432 Logic definitions in LF are based in the logic atlas of the Latin project \cite{project:latin}
439 designed for requirements engineering of business rules
442 \item[Fpl] is a ``logic for functional programs'' as an extension of a
443 restriction of \CASL (predicates are disabled) \cite{Sannella12}.
446 order theory of real numbers with some predefined binders
447 \cite{logic:EnCL}. It allows the formulation of executable
448 specifications of engineering calculation methods. For the execution
449 of these specifications Hets provides connections to the computer
452 the characteristic features of hybrid logic, both at the level of syntax and semantics. A comorphism from HybridCASL
455 The method of hybridisation of arbitrary institutions documented in \cite{DBLP:conf/calco/MartinsMDB11}, providing a method to automatically
456 combine the standard properties of hybrid logics with any logic already integrated in Hets.
457 Some manual intervention is still required: a parser and a semantics analyser for the sentences of the base
459 Currently, the hybridised versions of the following logics may be used in a fully automatic way:
471 explain both the \CASL logic and language of basic specifications as
477 Some of \HetCASL's heterogeneous constructs will be illustrated
488 each source sublogic, the corresponding sublogic of the target
490 A graph of the most important logics and sublogics, together with their
497 \caption{Graph of most important sublogics currently supported by \Hets,
502 In more detail, the following list of logic translations is currently
511 (translation $(7)$ of \cite{Mossakowski02}) \\\hline
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
516 CASL2Propositional & translation of propositional FOL \\\hline
517 CASL2SoftFOL & coding of CASL.SuleCFOL=E to SoftFOL \cite{LuettichEA06a},
519 CASL2SoftFOLInduction & same as CASL2SoftFOL but with instances of induction
522 CASL2SubCFOL & coding of partial functions by error elements
523 (translation $(4a')$ of \cite{Mossakowski02}, but extended to subsorting, i.e. sublogic SubPCFOL=) \\\hline
526 CASL2VSERefine & refining translation of CASL.CFOL= to VSE \\\hline
528 CoCASL2CoPCFOL & coding of subsorting by injections, similar to CASL2PCFOL \\\hline
529 CoCASL2CoSubCFOL & coding of partial functions by error supersorts, similar to CASL2SubCFOL \\\hline
534 Compact Common Logic is a sublogic of Common Logic
551 HasCASL2HasCASLPrograms & coding of \HasCASL axiomatic recursive definitions
553 HasCASL2Haskell & translation of \HasCASL recursive program definitions to Haskell \\\hline
554 HasCASL2IsabelleOption & coding of HasCASL to Isabelle/HOL \cite{Groening05} \\\hline
555 Haskell2Isabelle & coding of Haskell to Isabelle/HOL \cite{TorriniEtAl07} \\\hline
556 Haskell2IsabelleHOLCF & coding of Haskell to Isabelle/HOLCF \cite{TorriniEtAl07} \\\hline
557 HolLight2Isabelle & coding of HolLight to Isabelle/HOL \\\hline
558 Maude2CASL & encoding of rewrites as predicates \\\hline
559 Modal2CASL & the standard translation of modal logic
591 This will also install quite a couple of tools for proving requiring about
592 800 MB of disk space. For a minimal installation \texttt{apt-get install
593 hets-core} instead of \texttt{hets}.
609 A daily snapshot of \texttt{hets} can be installed by:
651 \section{Analysis of Specifications}
677 checking static well-formedness of specifications.
686 Then you can check the well-formedness of the
692 \Hets checks both the correctness of this specification
696 whether operators are applied to arguments of the correct sorts,
697 whether the use of overloaded symbols is unambiguous, and so on).
703 static analysis of (heterogeneous) structured specifications, but
704 leave out the analysis of basic specifications. This can be used
710 Use \texttt{DIR} as a colon separated list of directories for specification libraries (equivalently, you can set the variable \texttt{HETS\_LIB} before
713 For the analysis of architectural specification (a quite advanced
714 feature of \CASL), the \texttt{ANALYSIS} argument specifies the options for
716 algorithm for \CASL logic; it is a comma-separated list of zero or
717 more of the following options:
728 of certain specifications.
757 command line option of \Hets. In all other cases \texttt{.xml} files are
761 interchangeable, the former should be used for libraries of
763 of heterogeneous specifications (that use the \CASL structuring
775 embedding of \CASL into \HasCASL (cf.\ Fig.~\ref{fig:LogicGraph}).
780 A \CspCASL specification consists of a \CASL specification
835 declarations and definitions need to start with the first column of
846 A development graph consists of a set of nodes (corresponding to whole
847 structured specifications or parts thereof), and a set of arrows
848 called \emph{definition links}, indicating the dependency of each
850 associated with a signature and some set of local axioms. The axioms
851 of other nodes are inherited via definition links. Definition links
852 are usually drawn as black solid arrows, denoting an import of another
855 Complementary to definition links, which \emph{define} the theories of
862 postulates that all axioms of the source node (including the inherited
864 that the local axioms of the source node hold in the target node.
885 of the proof calculus for heterogeneous development graphs.
890 The following options let \Hets show the development graph of
909 Let us extend the above library \texttt{Order.casl}. One use of the
957 of the specifications in the library), see Fig.~\ref{fig:dg0}.
971 The black arrow denotes an ordinary import of
978 of a sorting function, taken from the \CASL User Manual
1004 The following specification of sorting by insertion also is taken from
1051 In the above-mentioned development graph, we have two types of nodes.
1054 specifications like the declaration of the $insert$ operation in
1058 Again, the black arrows denote an ordinary import of specifications
1081 Here is a summary of the types of nodes and links occurring in
1093 links in the sense of \cite[IV:4]{CASL/RefManual}).
1099 \item[Violett links] correspond to a mixture of links becoming visible after
1102 links in the sense of \cite[IV:4]{CASL/RefManual}.
1103 \item[Dashed links] correspond to local (theorem) links in the sense of
1113 We now explain the menus of the development graph window.
1114 Most of the pull-down menus of the window are uDraw(Graph)-specific
1119 of the graph have attached pop-up menus, which appear when
1130 you can switch on or off the display of node names, unnamed nodes or
1138 Initially, the complexity of the graph is reduced by hiding all these nodes;
1152 which does not fit on a single screen. The list of all nodes is displayed:
1158 This menu allows to select the type of links that are displayed in the
1166 Checks whether the theories of the nodes of the graph are consistent
1170 \item[Proofs] This menu allows to apply some of the deduction rules
1171 for development graphs, see Sect. IV:4.4 of the \CASL Reference
1172 Manual \cite{CASL/RefManual} or one of
1183 computing normal forms of all nodes (needed when dealing with hiding).
1184 Also, a \CASL-specific normalisation of free links has been
1189 of the development graph.
1205 Here, the number of submenus depends on the type of the node:
1208 \item[Show node info] Shows the local informations of the node: the internal
1209 node name and node number, the xpath that denotes the location of the node
1210 within an XML representation, information about consistency of the node,
1211 origin of the node and the local theory i.e. axioms declared locally.
1213 \item[Show theory] Shows the theory of the node (including axioms
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
1219 \item[Translate theory] Translates the theory of a node to another logic.
1223 of the signature of the node.
1244 \item[Check conservativity] Checks conservativity of the inclusion
1245 morphism from the empty theory to the theory of the node (see
1253 the development graph of the external library from which the specification has
1257 Again, the number of submenus depends on the type of the link:
1261 signature morphism of the link. The latter consists
1262 of two components: a logic translation and a signature morphism in the
1263 target logic of the logic translation.
1265 of an intra-logic signature morphism, the logic translation component is
1268 theory of the target node of the link
1269 is a conservative extension of the theory of the source node.
1293 \item[Show Logic Graph] Shows the graph of logics and logic comorphisms
1294 currently supported by \Hets. The Edit menu of a logic graph window has the
1306 \Hets provides several options controlling the types of files
1310 as explicit type of the input file. By default \texttt{env}, \texttt{casl},
1312 contains a shared ATerm of a development graph, whereas \texttt{casl} or
1319 ATerms) to be applied on top of an underlying development graph created from
1322 proof scripts. The contents of a \texttt{hpf} file must be valid input for
1349 \texttt{OTYPES} is a comma separated list of output types:
1372 Manchester Syntax for each specification of a structured OWL library.
1380 The \texttt{xml} option will produce an XML-version of the development graph
1404 the composition and inverse table of a Tarskian relation algebra from
1408 in the \CASL logic. A sample specification of a relation
1411 The output format is XML, the URL of the DTD is included in the
1421 \LaTeX\ version of \texttt{Order.casl} by typing:
1450 without blanks of one or more comorphism names (see Sect.~\ref{comorphisms})
1453 chooses a list of named specifications for processing
1456 chooses a list of named views for processing
1482 Large parts of \Hets are now also available via a web interface. A running
1493 and the slash of the URL, i.e.\
1495 created it can be accessed via a (fairly unique) session id (consisting of
1499 mark and consists of \emph{entries} (usually field-value pairs) separated by
1504 Usually, query string are made up of \texttt{field=value} pairs, but in some
1516 be used to perform commands (of the development graph calculus) that
1523 would try to prove the goals of the node \texttt{Nat\_\_E1} using the prover
1524 \texttt{SPASS} with a timeout of 5 seconds for the development graph that
1529 shorter by \texttt{?translations=0} and \texttt{?provers=0}, where instead of
1543 \texttt{Int} megabytes (needed in case of a stack overflow).
1549 \item[\texttt{--relative-positions}] Just uses the relative library name in positions of warning or errors.
1559 prover, i.e. by using the ``Prove'' menu of a red node.
1575 If you open this GUI when processing the goals of one node for the
1580 \item The button `Display' shows the selected goals in the ASCII syntax of
1584 the level of detail depends on the used theorem prover.
1587 \item The list `Pick Theorem Prover:' lets you choose one of the connected
1591 shortest possible path of comorphisms into the provers logic.
1594 \item Since the amount and kind of sentences sent to an ATP system is a major
1595 factor for the performance of the ATP system, it is possible to select in
1597 theory of the next proof attempt. Based on this selection the sublogic may
1603 the status of the goals' list is integrated into the development graph. If
1617 a `+', a `-' indicates an inconsistent node, a `t' denotes a timeout of the last
1626 For some selection of nodes (of a common logic) a model finder should be
1630 most the number of seconds given under `Timeout:' on each node. Pressing
1632 Either by `View results' or automatically the `Results of consistency check'
1649 \caption{Interface of the \SPASS prover\label{fig:SPASS_GUI}}
1655 in the top right part of the window the batch mode can be controlled. The
1656 left side shows the list of goals (with status indicators). If goals are
1661 On the bottom right the result of the last proof
1663 `Open (Time is up!)', or `Proved (Theory inconsistent!)'. The list of `Used
1665 of the ATP system. The `Save' buttons allow you to save the input and
1666 configuration of each proof for documentation. By `Close' the results for all
1670 Zimmer provides a unified interface to a range of different ATP
1674 (SPCs) defined upon the basis of logical, language and syntactical
1676 Only two of the Web services provided by the MathServe system are used
1705 {The list of problem classes for each ATP system is not
1726 The ATP system Vampire is the winner of the last 5 CADE ATP System
1729 of ordered binary resolution and superposition for handling equality.
1733 using an Web service of the MathServe system.
1739 % of the Herbrand universe; an effectively propositional problem has
1745 library Thousands of Problems for Theorem Provers (TPTP)
1759 like the simplifier or the tableaux prover, are built on top of this
1760 core. Furthermore, there is over fifteen years of experience with it,
1769 variety of logics within \Isabelle; one of them being \HOL (higher-order
1775 It is essential to be aware of the fact that the \Isabelle/\HOL logic
1777 Therefore, the formulas appearing in subgoals of proofs with \Isabelle
1778 will not conform to the syntax of the original input logic. They may
1779 even use features of \Isabelle/\HOL such as higher-order functions
1787 comorphism), followed by a list of theorems. Initially, all the
1804 for specification and verification of imperative programs.
1807 This logic is an extension of first-order logic with two additional
1808 kinds of formulas
1809 that allow for reasoning about programs. One of them is the
1812 The meaning of $[\alpha]\varphi$ can be roughly put as
1813 ``After every terminating execution of $\alpha$, $\varphi$ holds.''.
1815 of formulas is the diamond formula $\langle\alpha\rangle\varphi$, which is the dual counter part
1816 of a box formula. The meaning of $\langle\alpha\rangle\varphi$
1817 can be described as ``After some terminating execution of $\alpha$,
1821 \CASL) can be sent to the VSE prover via the node menu of development graph
1840 zChaff is a solver for satisfiabily problems of boolean formulas
1845 using the property, that a conjecture under the assumption of a set of axioms is
1846 true, if the variables of axioms together with the negation of the conjecture
1851 current integration of zChaff into \Hets has been tested with zChaff 2004.11.15.
1871 \verb+PELLET_PATH+ has to be set to the root-directory of the Pellet installation.
1905 is an extension of
1907 handling of equality. E-KRHyper is an automatic first order theorem
1911 The options of E-KRHyper are written in a Prolog-like syntax as in
1915 the ``.'' at the end of each option is mandatory. To get an overview of
1924 at the prompt of E-KRHyper, to display its help information, which is basically
1925 a long list of all available parameters. You can exit E-KRHyper by the command
1935 Calculus\cite{Baumgartner:2003}. The integration of Darwin as a consistency checker
1936 supports the display of models (if they can be constructed) in \CASL-syntax.
1938 Darwin uses Eprover for clausification of first-order formulae.
1940 Darwin supports a wide range of options, to get an overview of them run the command
1954 \section{Limits of Hets}
1963 \item Version numbers of libraries are not considered properly.
1969 \section{Architecture of Hets}
1971 The architecture of \Hets is shown in Fig.~\ref{fig:hets}.
1973 This is depicted in the left column of Fig.~\ref{fig:hets}.
2017 \caption{The basic ingredients of logics and logic comorphisms}
2023 \cite{PeytonJones03} by a set of types and functions, see
2027 which is a singleton type the only purpose of which is to determine
2028 all other type components of the given logic. In Haskell jargon, the
2035 of Fig.~\ref{fig:hets}. These modules comprise roughly one third of
2036 \Hets' 100.000 lines of Haskell code.
2045 of the logic is given, or if a logic translation is encountered (in
2046 the latter case, the state is set to the target logic of the
2048 by just using the logic-specific parser of the current logic as
2052 The static analysis is based on the static analysis of basic
2056 the static analysis of basic specifications) and/or translates (along
2072 and in the overview of modules provided in the developers section
2073 of the \Hets home page at \url{http://www.dfki.de/sks/hets}.
2081 \caption{Architecture of the heterogeneous tool set.
2104 with integration of more logics and proof tools into \Hets is also welcome.
2110 in the implementation of \Hets:
2172 of Mark van den Brand, Kolyang, Bartek Klin, Pascal Schmidt and