/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Literal.sml | 12 (* A type for storing first order logic literals. *)
|
H A D | Proof.sml | 12 (* A type of first order logic proofs. *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | HOL.tex | 2 \index{higher-order logic|(} 101 higher-order logic. Note that $a$\verb|~=|$b$ is translated to 282 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In 283 fact, the $\varepsilon$-operator already makes the logic classical, as 309 HOL follows standard practice in higher-order logic: only a few connectives 314 logic may equate formulae and even functions over formulae. But theory~HOL, 355 \subcaption{Propositional logic} 398 \subcaption{Classical logic} 548 Historically, higher-order logic gives a foundation for Russell and 893 simplification set for higher-order logic i [all...] |
H A D | CTT.tex | 586 intuitionistic logic. However, Constructive Type Theory is not just another 587 syntax for first-order logic. There are fundamental differences. 592 In first-order logic, $\disj$-elimination with the assumption $P\disj Q$ 832 Our example expresses a theorem about quantifiers in a sorted logic:
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
H A D | HOL.tex | 2 \index{higher-order logic|(} 101 higher-order logic. Note that $a$\verb|~=|$b$ is translated to 282 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In 283 fact, the $\varepsilon$-operator already makes the logic classical, as 309 HOL follows standard practice in higher-order logic: only a few connectives 314 logic may equate formulae and even functions over formulae. But theory~HOL, 355 \subcaption{Propositional logic} 398 \subcaption{Classical logic} 548 Historically, higher-order logic gives a foundation for Russell and 893 simplification set for higher-order logic i [all...] |
H A D | CTT.tex | 586 intuitionistic logic. However, Constructive Type Theory is not just another 587 syntax for first-order logic. There are fundamental differences. 592 In first-order logic, $\disj$-elimination with the assumption $P\disj Q$ 832 Our example expresses a theorem about quantifiers in a sorted logic:
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | thy_resources.scala | 50 logic = session_name, dirs = session_dirs, modes = print_mode)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/ |
H A D | thy_resources.scala | 50 logic = session_name, dirs = session_dirs, modes = print_mode)
|
/seL4-l4v-10.1.1/HOL4/src/quotient/Manual/ |
H A D | quotient.tex | 206 new types in the HOL logic, 462 including algebra and logic. 511 %%including algebra and logic. 517 %whose logic is a type theory, rather than a set theory. 589 %in the HOL logic 965 This relationship is defined in the HOL logic as a new predicate: 1049 %To define a new type in higher order logic, we must 1078 %in the HOL logic 1821 %are simple type variables in the HOL logic. 2222 Some theorem provers are based on classical logic, [all...] |
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | metisTools.sml | 265 val lmap = timed_fn "logic map build" build_map (interface,cs,ths)
|
/seL4-l4v-10.1.1/HOL4/src/num/theories/ |
H A D | whileScript.sml | 106 The while rule from Hoare logic, total correctness version.
|
/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | HolQbf.tex | 117 \paragraph{Supported subset of higher-order logic}
|
H A D | misc.tex | 856 \index{inferences, in HOL logic@inferences, in \HOL{} logic!counting of|(} 939 \index{inferences, in HOL logic@inferences, in \HOL{} logic!counting of|)} 1112 \index{combinators, in HOL logic@combinators, in \HOL{} logic}% 1150 \index{ dollar sign, in HOL logic parser@\ml{\$} (dollar sign, in \HOL{} logic parser)!as escape character}% 1259 \index{parsing, of HOL logic@parsing, of \HOL{} logic!overloadin [all...] |
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | HolQbf.tex | 114 \paragraph{Supported subset of higher-order logic}
|
H A D | misc.tex | 787 \index{inferences, in HOL logic@inferences, in \HOL{} logic!counting of|(} 870 \index{inferences, in HOL logic@inferences, in \HOL{} logic!counting of|)} 1037 \index{combinators, in HOL logic@combinators, in \HOL{} logic} 1056 \index{ escape, in HOL logic parser@\ml{\$} (escape, in \HOL{} logic parser)}% 1146 \index{parsing, of HOL logic@parsing, of \HOL{} logic!overloadin [all...] |
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/ |
H A D | MiniTLHexSolitaireScript.sml | 6 (* Next two versions of a mini temporal logic are defined. *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | sets.tex | 18 temporal logic CTL\@. Most of the other examples are simple. The 245 to predicate variables, which are allowed in higher-order logic. The main 503 given set. This refinement is useful in higher-order logic, where
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | sets.tex | 18 temporal logic CTL\@. Most of the other examples are simple. The 245 to predicate variables, which are allowed in higher-order logic. The main 503 given set. This refinement is useful in higher-order logic, where
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
H A D | finite_setScript.sml | 7 (* Representing finite sets as a new datatype in the HOL logic. *)
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/ |
H A D | termScript.sml | 13 (* Representing the lambda calculus as a new datatype in the HOL logic. *)
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/examples/ |
H A D | holScript.sml | 11 (* a theory of higher order logic terms, as modelled in systems such as
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 177 in \S\ref{propositional-logic}. 207 \label{propositional-logic} 209 Let's start with a trivial example from propositional logic: 437 Internally, undefined values lead to a three-valued logic. 517 Because numbers are infinite and are approximated using a three-valued logic, 558 Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value, 614 Because datatypes are approximated using a three-valued logic, there is usually 2233 \url{http://tools.computational-logic.org/content/riss3g.php}. 2534 Because of its internal three-valued logic, Nitpick tends to lose a
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Nitpick/document/ |
H A D | root.tex | 177 in \S\ref{propositional-logic}. 207 \label{propositional-logic} 209 Let's start with a trivial example from propositional logic: 437 Internally, undefined values lead to a three-valued logic. 517 Because numbers are infinite and are approximated using a three-valued logic, 558 Since $\mathit{hd}~[]$ is undefined in the logic, it may be given any value, 614 Because datatypes are approximated using a three-valued logic, there is usually 2233 \url{http://tools.computational-logic.org/content/riss3g.php}. 2534 Because of its internal three-valued logic, Nitpick tends to lose a
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Proof.sml | 12 (* A type of first order logic proofs. *)
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | selftest.sml | 159 (* propositional logic *) 621 (* higher-order logic *)
|