Searched refs:proof (Results 1 - 25 of 518) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/proofman/
H A DManager.sig5 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 DproofManagerLib.sig4 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__.py11 from .proof import Proof
/seL4-l4v-master/HOL4/src/HolSat/
H A DsatConfig.sml27 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 DProof.sig21 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 DResolution.sig10 (* A type of resolution proof procedures. *)
36 (* The main proof loop. *)
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DProof.sig21 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 DResolution.sig10 (* A type of resolution proof procedures. *)
36 (* The main proof loop. *)
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DMain.C103 // 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 DSolver.C57 | 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 DpsMinimize.sml51 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 DMakefile17 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 Dthy_element.scala4 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 Dthy_element.scala4 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 Dvampire.sh9 timeout 60 ./vampire_v4.2.2_noz3 --time_limit 60 --proof tptp --output_axiom_names on $1 | grep "file[(]'\| SZS" > $OUT1
H A Dvampire_casc.sh9 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 DtttRecord.sig17 (* Wrapping proof *)
20 (* Executing the wrapped proof *)
/seL4-l4v-master/graph-refine/
H A Dcheck.py7 # 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 DmilScript.sml3 (* 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 Dvampire.sh11 timeout $1 ./vampire --time_limit $1 --proof tptp --output_axiom_names on $IN 2> $ERROR \
/seL4-l4v-master/HOL4/src/real/
H A DrealLib.sml4 (* is also included. plus some other proof procedures. *)
/seL4-l4v-master/isabelle/src/Pure/
H A Dterm_xml.scala88 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 Dterm_xml.scala88 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 Dpreface.tex37 \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 DZ3_ProofParser.sml61 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...]

Completed in 203 milliseconds

1234567891011>>