Searched defs:the (Results 1 - 6 of 6) sorted by relevance

/hets/doc/
H A DLibraries.tex36 % - prints and marks TEXT for the main index
40 % - marks TEXT,SUBTEXT and SUBTEXT,TEXT for the main index
48 % - prints \emph{TEXT} and marks TEXT for the main index
53 % - marks \Gram{TEXT} for the Symbol Index, sorted as TEXT
72 \title{CASL libraries on the web}
78 \section{What the \CASL summary says}
81 A library may be located at a particular \emphindex{site} on the
84 the location and perhaps identifies a particular version of the
92 independently of their registration in the globa
[all...]
H A DUserGuideCommonLogic.tex51 %% 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 us
[all...]
H A Dhs2isa.tex25 been implemented as part of the Heterogeneous Tool Set. The the target logic
26 is Isabelle/HOLCF, and the translation is based on a shallow embedding
37 Automating translation from programming languages to the language of a generic
38 prover may provide useful support for the formal development and the
40 make the task of proving assertions about programs written in them easier,
41 owing to the relative simplicity of their semantics
43 to us, more specifically, from an interest in the use of functional languages
44 for the specificatio
[all...]
/hets/CASL/doc/
H A DCASLParserOverview.tex16 see the documentation for HetCATS and Common
18 \section{Compiling the CASL parser}
22 \texttt{gmake capa} in the top directory.
25 print) ``Basic Specification with Subsorts'' of the CASL Summary
28 Structured specifications (see \texttt{Static/hetpa.hs}) must be parsed by the
44 given as \texttt{*.casl} files in the \texttt{test} subdirectory. Calling
45 \texttt{./runcheck.sh ../capa} performs many tests and compares the results
48 Alternatively a test can be run using \texttt{runhugs}. For this the
49 file \texttt{capa.lhs} is executable and the test can be run
55 with the expecte
[all...]
/hets/Maude/doc/
H A Ddg.tex8 \subsection{Creating the development graph}
14 Each Maude module generates two nodes in the development
15 graph. The first one contains the theory equipped with the usual
17 to the first one with a free definition link (whose signature morphism
18 is detailed in Section \ref{sec:free}), contains the same signature but
19 no local axioms and stands for the free models of the theory.
24 consists of free extensions of the models of their parameters, that are
33 Maude module expressions allow to combine and modify the informatio
[all...]
/hets/CASL_DL/doc/
H A DCASL_DL-Notes.tex13 \title{Design and Notes for the \CASLDL Node in Hets}
17 \textbf{Note:} The following issues very often mention the not jet
18 complete OWL DL logic (node) of Hets. Clearly the development of
24 the named spec is put into a file/CASL library that contains
25 only this named spec? Till] [No, if you parse an OWL DL file the
27 specifications. This makes the handling of parsing and analysis
32 food.owl. If you parse wine.owl the parser reads first wine.owl and
34 hence it skips the import in food.owl. This development graph has
41 [Although it seems to be the only way, it sounds a bit complicated.
42 Perhaps you could leave out the ``splittin
[all...]

Completed in 13 milliseconds