| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | holCheck.tex | 35 This is a brief description of the \hc{}\index{holCheckLib!\hc{}} model checker, version 1.0. It assumes the reader is familiar with symbolic model checking, with \HOL{}, and, ideally, with \texttt{HolBddLib}, the \HOL{} interface to BDDs. It should be read with a working \HOL{} installation at hand.
39 \hc{} is a BDD-based model checker embedded in the \HOL{} theorem prover, interfaced to an external BDD engine for efficiency. It currently has the following features:
42 \item All steps of the algorithm are proved in \HOL{}, with BDD operations considered atomic.
43 \item Results are returned as \HOL{} theorems.
59 See \S\ref{sec:models} for details. The user is required to supply only \( S_0 \) and \( T \) as the remaining components can be calculated from these. Properties are input as \HOL{} terms of type \(\mathtt{mu}\) or \(\mathtt{ctl}\), \HOL{} datatypes for which have been defined (see \S\ref{sec:prop} for details). A property is satisfied by a model if the set of initial states of the model is a subset of the set of states satisfying the property.
183 For our running example, we use \texttt{ttt.sml} from \texttt{src/HolCheck/examples}. Build this (and others\footnote{The AMBA examples are large and take a while to build. To skip them, see the README file in the same folder.}) by typing \texttt{Holmake} in \texttt{src/HolCheck/examples}. Now start \HOL{} from this directory (or use the -I command-line parameter).
185 The first step after loading \HOL{} i
[all...] |
| H A D | version2.tex | 6 This appendix summarizes the differences between \HOL 88 Version 2.0
17 The top-level directory of the \HOL\ distribution sources has been
19 Installing \HOL'). An important addition is a directory
20 {\small\verb%contrib%} containing contributions from the \HOL\ user
48 Four libraries from Version 1.11 of HOL have been temporarily withdrawn,
110 of methodologies for embedding application-specific languages in \HOL\
114 quotation typecheckers for the \HOL\ logic. This enables more type
128 The top-level of the \HOL\ distribution directory now contains:
151 the \HOL\ distribution directory (`\ml{hol}') resides.
180 \noindent returns the internal pathname used by \HOL\ t
[all...] |
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | holCheck.tex | 35 This is a brief description of the \hc{}\index{holCheckLib!\hc{}} model checker, version 1.0. It assumes the reader is familiar with symbolic model checking, with \HOL{}, and, ideally, with \texttt{HolBddLib}, the \HOL{} interface to BDDs. It should be read with a working \HOL{} installation at hand.
39 \hc{} is a BDD-based model checker embedded in the \HOL{} theorem prover, interfaced to an external BDD engine for efficiency. It currently has the following features:
42 \item All steps of the algorithm are proved in \HOL{}, with BDD operations considered atomic.
43 \item Results are returned as \HOL{} theorems.
59 See \S\ref{sec:models} for details. The user is required to supply only \( S_0 \) and \( T \) as the remaining components can be calculated from these. Properties are input as \HOL{} terms of type \(\mathtt{mu}\) or \(\mathtt{ctl}\), \HOL{} datatypes for which have been defined (see \S\ref{sec:prop} for details). A property is satisfied by a model if the set of initial states of the model is a subset of the set of states satisfying the property.
183 For our running example, we use \texttt{ttt.sml} from \texttt{src/HolCheck/examples}. Build this (and others\footnote{The AMBA examples are large and take a while to build. To skip them, see the README file in the same folder.}) by typing \texttt{Holmake} in \texttt{src/HolCheck/examples}. Now start \HOL{} from this directory (or use the -I command-line parameter).
185 The first step after loading \HOL{} i
[all...] |
| H A D | version2.tex | 6 This appendix summarizes the differences between \HOL 88 Version 2.0
17 The top-level directory of the \HOL\ distribution sources has been
19 Installing \HOL'). An important addition is a directory
20 {\small\verb%contrib%} containing contributions from the \HOL\ user
48 Four libraries from Version 1.11 of HOL have been temporarily withdrawn,
110 of methodologies for embedding application-specific languages in \HOL\
114 quotation typecheckers for the \HOL\ logic. This enables more type
128 The top-level of the \HOL\ distribution directory now contains:
151 the \HOL\ distribution directory (`\ml{hol}') resides.
180 \noindent returns the internal pathname used by \HOL\ t
[all...] |
| H A D | tactics.tex | 7 in \HOL. All three originate with Milner
61 the idea is similarly central to theorem proving in \HOL.
68 %The tactics and tacticals in the \HOL{} system are derived from those in the
80 \index{goals, in HOL system@goals, in \HOL{} system}
110 \index{proofs, in HOL logic@proofs, in \HOL{} logic!as ML function applications@as \ML{} function applications}
112 in \HOL{}, following the \LCF{} usage; it is, as mentioned,
116 \index{proofs, in HOL logic@proofs, in \HOL{} logi
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/IndDef/Manual/ |
| H A D | paper.tex | 16 and Workshop on the HOL Theorem Proving System, 27--30 August 1991,
19 {\Large\bf A Package for Inductive Relation Definitions in HOL}\\
33 derived principle of definition in HOL, namely the introduction of relations
45 The HOL user community has a strong tradition of taking a purely {\it
51 rules of definition in the {\small HOL} logic---namely, constant definition,
60 in the {\small HOL} system and thus provides a facility for automating proofs
63 {\small HOL} logic. But certain recursive type definitions and function
72 principle of definition in {\small HOL} for defining relations inductively by a
235 ${\sf Rtc}\;R$ can be defined in the {\small HOL} logic by the constant
259 defined formally in the {\small HOL} logi
[all...] |
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/poly/ |
| H A D | HM_Cline.sml | 84 wn ("HOL state-file already set; ignoring earlier spec")
116 {help = "specify HOL state", long = ["holstate"], short = "",
122 {help = "use poly rather than a HOL heap", long = ["poly_not_hol"],
|
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
| H A D | elliptic_exampleScript.sml | 62 (* Extensions to HOL theories to define the ex_ constants. *)
71 (* First define the parameters for the example using HOL types. *)
134 (* Converting HOL types to words. *)
334 (* eliminate HOL types that are not just tuples of word32s. *)
477 (* First define the parameters for the example using HOL types. *)
485 (* Converting HOL types to words. *)
|
| /seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
| H A D | QDimacs.sml | 3 (* Translation between (the QBF-in-prenex-form subset of) HOL terms and the
32 (* free variables in HOL theorems, which are (implicitly) universally *)
34 (* theorem in HOL. *)
161 (* read_qdimacs_file: returns a QBF (as a HOL term) that corresponds to the *)
166 (* to HOL variables of type bool. 'varfn' is expected to be injective, *)
272 are implicitly existential) vs. HOL (where they are implicitly
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/Fact32/ |
| H A D | exor32.ml | 16 (* Define the component in HOL *)
52 (* instances) and a function to print a HOL term ``XOR32(in1,in2,out)`` as *)
|
| H A D | Xor32.ml | 66 (* Stop zillions of warning messages that HOL variables of type ``:num`` *)
|
| /seL4-l4v-10.1.1/HOL4/examples/imperative/ |
| H A D | necec2010.sml | 7 \section{HOL Preliminaries}
9 The HOL logic system provides a proof manager which manages the derivation of an proof. It does so using a
20 There are a number of libraries in HOL which make this possible. One library in particular, known as `bossLib',
25 Once the internal features of the bossLib structure are exposed to the HOL session, terms can now consist of expressions on strings, numbers and lists.
26 As per HOL recommendations, other libraries required by the test case should be open at the front of the file befor any other commands.
29 we enable the HOL system to display all assumptions and data types currently in use.
106 For novice users of HOL, the above code demonstrates seven commonly used tactics of the HOL proving system, namely:
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/ |
| H A D | SatSolvers.sml | 3 ** can be invoked from HOL.
12 ** post_run, (* transform SAT solver output before reading into HOL *)
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | OmegaSimple.sig | 20 implementation into HOL kernel proofs. It also performs the initial
21 translation from a HOL formula into a shadow proof state, so that the
|
| /seL4-l4v-10.1.1/HOL4/src/simp/src/ |
| H A D | Opening.sig | 56 * Some examples (where REL is HOL equality)
85 * Optimized implementations of the HOL equality congruence rules using the
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/ |
| H A D | ml.tex | 34 trasferito alla shell e valutato in \HOL{} con un `copia e incolla'. In
48 persistano nei successivi. Per entrare nel sistema \HOL{} si
51 \HOL{} non � nel proprio percorso. Il sistema \HOL{} quindi
64 HOL-4 [\holnsversion (built Fri Apr 12 15:34:35 2002)]
66 For introductory HOL help, type: help "hol";
91 logica \HOL{} che � spiegata nel Capitolo~\ref{HOLlogic}.
256 capitolo, sar� introdotta la logica supportata dal sistema \HOL{} (la logica di
|
| H A D | more-examples.tex | 21 In questa directory, c'� un benchmarck standard di HOL: la dimostrazione della
30 l'automazione di \HOL{} su una dimostrazione classica.
|
| /seL4-l4v-10.1.1/HOL4/Manual/Tutorial/ |
| H A D | more-examples.tex | 21 In this directory, there is a standard HOL benchmark: the proof of
30 automation of \HOL{} on a classic proof.
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Functions/document/ |
| H A D | intro.tex | 14 We assume that you have mastered the fundamentals of Isabelle/HOL
16 with Isabelle in general, consult the Isabelle/HOL tutorial
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
| H A D | preface.tex | 5 in higher-order logic (HOL), using the proof assistant Isabelle.
21 also describes Isabelle/HOL's treatment of sets, functions and
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Functions/document/ |
| H A D | intro.tex | 14 We assume that you have mastered the fundamentals of Isabelle/HOL
16 with Isabelle in general, consult the Isabelle/HOL tutorial
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
| H A D | preface.tex | 5 in higher-order logic (HOL), using the proof assistant Isabelle.
21 also describes Isabelle/HOL's treatment of sets, functions and
|
| /seL4-l4v-10.1.1/l4v/tools/autocorres/ |
| H A D | Makefile | 28 python ../../misc/scripts/gen_isabelle_root.py -o $@ -b AutoCorres -s AutoCorresTest -d HOL-Number_Theory \
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
| H A D | HOL.tex | 3 \index{HOL system@{\sc hol} system}
6 polymorphic version of Church's Simple Theory of Types. HOL can be best
8 \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a
9 gentle introduction on using Isabelle/HOL in practice.
59 \caption{Syntax of \texttt{HOL}} \label{hol-constants}
93 \caption{Full grammar for HOL} \label{hol-grammar}
105 HOL has no if-and-only-if connective; logical equivalence is expressed using
125 HOL allows new types to be declared as subsets of existing types,
127 \texttt{datatype} (see~{\S}\ref{sec:HOL:datatype}).
188 satisfying~$P$, if such exists. Since all terms in HOL denot
[all...] |
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
| H A D | HOL.tex | 3 \index{HOL system@{\sc hol} system}
6 polymorphic version of Church's Simple Theory of Types. HOL can be best
8 \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} provides a
9 gentle introduction on using Isabelle/HOL in practice.
59 \caption{Syntax of \texttt{HOL}} \label{hol-constants}
93 \caption{Full grammar for HOL} \label{hol-grammar}
105 HOL has no if-and-only-if connective; logical equivalence is expressed using
125 HOL allows new types to be declared as subsets of existing types,
127 \texttt{datatype} (see~{\S}\ref{sec:HOL:datatype}).
188 satisfying~$P$, if such exists. Since all terms in HOL denot
[all...] |