/seL4-l4v-master/HOL4/src/proofman/ |
H A D | Manager.sig | 5 datatype proof type 9 datatype proofs = PRFS of proof list 12 (* Starting a proof *) 13 val new_goalstack : goal -> (thm->thm) -> proof 14 val new_goaltree : goal -> proof 15 val set_goal : goal -> proof 16 val add : proof -> proofs -> proofs 19 val backup : proof -> proof 20 val set_backup : int -> proof [all...] |
H A D | proofManagerLib.sig | 4 type proof = Manager.proof type 9 (* Starting a proof *) 17 val add : proof -> proofs 21 val b : unit -> proof 25 val restart : unit -> proof 26 val backup : unit -> proof 27 val restore : unit -> proof 28 val save : unit -> proof 34 val e : tactic -> proof [all...] |
/seL4-l4v-master/l4v/misc/pysymbols/isasymbols/ |
H A D | __init__.py | 11 from .proof import Proof
|
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | satConfig.sml | 27 proof : string option, 28 (* proof trace file in HolSatLib format; overrides solver if SOME*) 34 {pterm = boolSyntax.T, solver = minisatp, infile = NONE, proof = NONE, 46 (* if SOME, then valOf is name of proof file (HolSat format) on disk that is 48 fun get_proof (c:sat_config) = (#proof c) 58 {pterm = tm, solver = #solver c, infile = #infile c, proof = #proof c, 62 {pterm = #pterm c, solver = ss, infile = #infile c, proof = #proof c, 66 {pterm = #pterm c, solver = #solver c, infile = SOME nm, proof [all...] |
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Proof.sig | 21 type proof = (Thm.thm * inference) list type 39 val proof : Thm.thm -> proof value 45 val freeIn : Term.var -> proof -> bool 47 val freeVars : proof -> NameSet.set 57 val pp : proof Print.pp 59 val toString : proof -> string
|
H A D | Resolution.sig | 10 (* A type of resolution proof procedures. *) 36 (* The main proof loop. *)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Proof.sig | 21 type proof = (Thm.thm * inference) list type 39 val proof : Thm.thm -> proof value 45 val freeIn : Term.var -> proof -> bool 47 val freeVars : proof -> NameSet.set 57 val pp : proof Print.pp 59 val toString : proof -> string
|
H A D | Resolution.sig | 10 (* A type of resolution proof procedures. *) 36 (* The main proof loop. *)
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Main.C | 103 // Simplistic proof-checker -- just to illustrate the use of 'ProofTraverser': 170 void checkProof(Proof* proof, ClauseId goal = ClauseId_NULL) argument 174 proof->traverse(trav, res_count, goal); 195 " -p <proof trace> Write the trace to this file.\n" 196 " -c Check the trace by simple (read \"slow\") proof checker.\n" 197 " -x Extract proof from trace.\n" 204 char* proof = NULL; local 223 proof = argv[i]; 243 if (proof != NULL || check) S.proof [all...] |
H A D | Solver.C | 57 | id - If logging proof, learnt clauses should be given an ID by caller. 78 if (proof != NULL) proof->incRootCount(); 82 if (proof != NULL) proof->incRootCount(); 88 if (proof != NULL) proof->beginChain(proof->addRoot(qs)); 94 if (proof != NULL) proof [all...] |
/seL4-l4v-master/HOL4/src/AI/proof_search/ |
H A D | psMinimize.sml | 51 Pretty proof steps 59 fun pretty_allstac tim proof = case proof of 86 fun unsafe_prettify_proof proof = 89 fun loop proof = case proof of 106 val body = loop proof 115 fun safe_prettify_proof proof = case proof of 173 Minimizing lists in all tactics of a proof [all...] |
/seL4-l4v-master/l4v/tools/autocorres/ |
H A D | Makefile | 17 PROOF_TESTS_C := $(wildcard tests/proof-tests/*.c) 18 PROOF_TESTS_THY := $(wildcard tests/proof-tests/*.thy) 29 -i tests/parse-tests -i tests/proof-tests -i tests/examples --quick-and-dirty --dir parse-tests --dir proof-tests --dir examples 34 -i tests/parse-tests -i tests/proof-tests -i tests/examples 58 make -C ../../proof CBaseRefine
|
/seL4-l4v-master/isabelle/src/Pure/Thy/ |
H A D | thy_element.scala | 4 Theory elements: statements with optional proof. 18 sealed case class Element[A](head: A, proof: Option[Proof[A]]) 23 (prf, qed) <- proof.iterator 28 proof match { 34 proof match { 41 proof match { 86 category(Keyword.theory_goal, false) ~ proof ^^ { case a ~ b => element(a, b) } 88 category(Keyword.proof_goal, false) ~ proof ^^ { case a ~ b => element(a, b) } | 90 def proof: Parser[Proof[Command]] =
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/ |
H A D | thy_element.scala | 4 Theory elements: statements with optional proof. 18 sealed case class Element[A](head: A, proof: Option[Proof[A]]) 23 (prf, qed) <- proof.iterator 28 proof match { 34 proof match { 41 proof match { 86 category(Keyword.theory_goal, false) ~ proof ^^ { case a ~ b => element(a, b) } 88 category(Keyword.proof_goal, false) ~ proof ^^ { case a ~ b => element(a, b) } | 90 def proof: Parser[Proof[Command]] =
|
/seL4-l4v-master/HOL4/examples/AI_tasks/TPTP/ |
H A D | vampire.sh | 9 timeout 60 ./vampire_v4.2.2_noz3 --time_limit 60 --proof tptp --output_axiom_names on $1 | grep "file[(]'\| SZS" > $OUT1
|
H A D | vampire_casc.sh | 9 timeout 60 ./vampire_v4.2.2_noz3 --mode casc --time_limit 60 --proof tptp --output_axiom_names on $1 | grep "file[(]'\| SZS" > $OUT1
|
/seL4-l4v-master/HOL4/src/tactictoe/src/ |
H A D | tttRecord.sig | 17 (* Wrapping proof *) 20 (* Executing the wrapped proof *)
|
/seL4-l4v-master/graph-refine/ |
H A D | check.py | 7 # proof scripts and check process 176 assert not 'proof node kind understood', kind 213 assert not 'proof node kind understood' 214 for proof in self.subproofs: 215 proof.serialise (p, ss) 218 return [self] + [proof for proof1 in self.subproofs 219 for proof in proof1.all_subproofs ()] 226 for ((restrs2, hyps2, name2), proof) in subproofs 227 for problem in proof.all_subproblems (p, restrs2, 309 assert not 'proof nod [all...] |
/seL4-l4v-master/HOL4/examples/ind_def/ |
H A D | milScript.sml | 3 (* DESCRIPTION : Defines a proof system for minimal intuitionistic *) 52 (* inductively by the proof rules for the logic. *) 70 (* to prove the conclusion. The proof is completely straightforward. *) 78 (* The proof for the other direction proceeds by induction over the *)
|
/seL4-l4v-master/HOL4/src/holyhammer/provers/ |
H A D | vampire.sh | 11 timeout $1 ./vampire --time_limit $1 --proof tptp --output_axiom_names on $IN 2> $ERROR \
|
/seL4-l4v-master/HOL4/src/real/ |
H A D | realLib.sml | 4 (* is also included. plus some other proof procedures. *)
|
/seL4-l4v-master/isabelle/src/Pure/ |
H A D | term_xml.scala | 88 def proof: T[Proof] = 92 { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) }, 93 { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) }, 94 { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) }, 95 { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) }, 101 proof 104 val proof: T[Proof] = proof_env(Map.empty)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/ |
H A D | term_xml.scala | 88 def proof: T[Proof] = 92 { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) }, 93 { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) }, 94 { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) }, 95 { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) }, 101 proof 104 val proof: T[Proof] = proof_env(Map.empty)
|
/seL4-l4v-master/HOL4/Manual/Tutorial/ |
H A D | preface.tex | 37 \item Goal directed proof, tactics, and tacticals. 42 proof of the infinitude of primes---to illustrate how \HOL{} is used 49 \HOL{} system for a tricky proof. Chapter~\ref{chap:combin} is a more 50 extensive example: the proof of confluence for combinatory 54 Chapter~\ref{chap:proof-tools} gives an example of implementing a 55 proof tool of one's own. This demonstrates the programmability of 63 %\item Chapter~\ref{tool} shows how a special purpose proof tool (a 65 % illustrates methods for `tuning' proof generating programs and 68 %\item Chapter~\ref{binomial} is a proof of the Binomial Theorem in a 73 % notation is expressed in \HOL{}, and the structure of the proof i [all...] |
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | Z3_ProofParser.sml | 61 I am hoping that the Z3 proof format will eventually be changed 116 (* FIXME: I am hoping that the Z3 proof format will eventually be 305 (* returns an extended proof; 't' must encode a proofterm *) 306 fun extend_proof proof (id, t) = 309 Option.isSome (Redblackmap.peek (proof, id)) then 314 Redblackmap.insert (proof, id, proofterm_of_term t) 318 definition; returns a (possibly extended) dictionary and proof *) 319 fun parse_definition get_token (tydict, tmdict, proof) = 333 val proof = extend_proof proof (proofterm_i value 393 val proof = parse_proof get_token value [all...] |