/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Literal.sig | 10 (* A type for storing first order logic literals. *)
|
H A D | Term.sig | 10 (* A type of first order logic terms. *)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | General.sml | 60 (* Exception packets. The first word is the code, a unique id; the second is
|
H A D | ListPair.sml | 100 (* Is it better to check the lengths first? *)
|
/seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 4 The theory~\thydx{LK} implements classical first-order logic through Gentzen's 13 first-order terms is called \cldx{term}. No types of individuals are 440 duplication, we employ best-first search: 574 A \textbf{pack} is a pair whose first component is a list of safe rules and 615 frequently fails to terminate. It is generally unsuitable for depth-first 664 The method is inherently depth-first. 677 applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$. 701 applies {\tt step_tac} using depth-first search to solve subgoal~$i$. 705 applies {\tt step_tac} using best-first search to solve subgoal~$i$. It is
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | preface.tex | 12 The first part, \textbf{Elementary Techniques},
|
/seL4-l4v-master/HOL4/examples/temporal_deep/src/model_check/ |
H A D | modelCheckLib.sig | 35 (*Checks that the given ltl-formulas are equivalent at the first point of time. Since there are past ltl operators this does not mean that they are equivalent for all points of time!*)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Formula.sig | 10 (* A type of first order logic formulas. *)
|
H A D | KeyMap.sig | 84 {first : key * 'a -> 'c option,
|
H A D | Literal.sig | 10 (* A type for storing first order logic literals. *)
|
H A D | Term.sig | 10 (* A type of first order logic terms. *)
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 4 The theory~\thydx{LK} implements classical first-order logic through Gentzen's 13 first-order terms is called \cldx{term}. No types of individuals are 440 duplication, we employ best-first search: 574 A \textbf{pack} is a pair whose first component is a list of safe rules and 615 frequently fails to terminate. It is generally unsuitable for depth-first 664 The method is inherently depth-first. 677 applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$. 701 applies {\tt step_tac} using depth-first search to solve subgoal~$i$. 705 applies {\tt step_tac} using best-first search to solve subgoal~$i$. It is
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | preface.tex | 12 The first part, \textbf{Elementary Techniques},
|
/seL4-l4v-master/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibSimple.sig | 76 both sides of the equation first. For example, to find guesses
|
/seL4-l4v-master/l4v/tools/c-parser/standalone-parser/ |
H A D | GetOpt.sig | 43 * RequireOrder: no option processing after first non-option
|
/seL4-l4v-master/HOL4/examples/fermat/little/ |
H A D | FLTbinomialScript.sml | 23 (k+1)^p = k^p + 1^p (mod p) just first and last terms
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 164 invoked the first time. 213 in \S\ref{first-steps}. If the remote versions of any of these provers is used 233 \label{first-steps} 297 For best results, first simplify your problem by calling \textit{auto} or at 304 is better for first-order problems. Hence, you may get better results if you 305 first simplify the problem to remove higher-order features. 425 proof is too difficult for it. Metis's search is complete for first-order logic 536 the reverse is also true, so do not be discouraged if your first attempts fail. 595 first-order ATP (such as E, SPASS, and Vampire) as opposed to a 635 > Isabelle > General.'' For automatic runs, only the first prove [all...] |
/seL4-l4v-master/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 164 invoked the first time. 213 in \S\ref{first-steps}. If the remote versions of any of these provers is used 233 \label{first-steps} 297 For best results, first simplify your problem by calling \textit{auto} or at 304 is better for first-order problems. Hence, you may get better results if you 305 first simplify the problem to remove higher-order features. 425 proof is too difficult for it. Metis's search is complete for first-order logic 536 the reverse is also true, so do not be discouraged if your first attempts fail. 595 first-order ATP (such as E, SPASS, and Vampire) as opposed to a 635 > Isabelle > General.'' For automatic runs, only the first prove [all...] |
/seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
H A D | foundations.tex | 48 \caption{Intuitionistic first-order logic} \label{fol-fig} 52 \index{first-order logic} 54 Figure~\ref{fol-fig} presents intuitionistic first-order logic, 80 first-order. The latter syntax is used throughout the manual. 144 higher-order logic but not in first-order logic. 301 In our formalization of first-order logic, we declared a type~$o$ of 482 formalizing first-order logic~\cite{paulson-found}. There is a one-to-one 590 \item Equations with no function unknowns are solved using first-order 601 imitation. The first solution is usually the one desired: 646 When resolving two rules, the unknowns in the first rul [all...] |
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
H A D | foundations.tex | 48 \caption{Intuitionistic first-order logic} \label{fol-fig} 52 \index{first-order logic} 54 Figure~\ref{fol-fig} presents intuitionistic first-order logic, 80 first-order. The latter syntax is used throughout the manual. 144 higher-order logic but not in first-order logic. 301 In our formalization of first-order logic, we declared a type~$o$ of 482 formalizing first-order logic~\cite{paulson-found}. There is a one-to-one 590 \item Equations with no function unknowns are solved using first-order 601 imitation. The first solution is usually the one desired: 646 When resolving two rules, the unknowns in the first rul [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | patternMatch.sml | 8 (* the order in which subterms of any term are to be examined to find the first patter n *) 213 (* the choice of tests with low branching factor first. *)
|
/seL4-l4v-master/HOL4/polyml/samplecode/ide/ |
H A D | use.sml | 75 (* If the first part of the path is ".." then it's in some other directory. *) 124 (* use "f" first tries to open "f" but if that fails it tries "f.ML", "f.sml" etc. *)
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | Ho_Rewrite.sml | 4 (* straightforward adaptation of the first order *) 93 ["Multiple rewrites possible (first taken):\n",
|
/seL4-l4v-master/HOL4/src/search/ |
H A D | bftScript.sml | 2 (* Breadth-first traversal of directed graphs that can contain cycles. *) 29 (* Termination proof. In the first recursive call, the fringe list is *)
|
H A D | dftScript.sml | 2 (* Depth first traversal of directed graphs that can contain cycles. *) 29 (* Termination proof. In the first recursive call, the to_visit list is *)
|