Searched refs:Proof (Results 1 - 25 of 138) sorted by relevance

123456

/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttMinimize.sig6 datatype Proof = type
8 | Then of (Proof * Proof)
9 | Thenl of (Proof * Proof list)
13 val minimize_proof : Proof -> Proof
14 val reconstruct : goal -> Proof -> string
H A DtttSearch.sig23 ProofError | ProofSaturated | ProofTimeOut | Proof of string
H A DtacticToe.sml203 | Proof s =>
331 NONE => debug_eproof ("Proof status: Time Out")
342 debug_eproof ("Proof found: " ^ newstac)
354 | ProofSaturated => debug_proof "Proof status: Saturated"
355 | ProofTimeOut => debug_proof "Proof status: Time Out"
356 | Proof s => debug_proof ("Proof found: " ^ s)
H A DtttMinimize.sml154 datatype Proof = type
156 | Then of (Proof * Proof)
157 | Thenl of (Proof * Proof list)
/seL4-l4v-10.1.1/l4v/misc/pysymbols/isasymbols/
H A D__init__.py16 from .proof import Proof namespace
H A Dproof.py19 p = Proof('True \\<and> True')
30 class Proof(object): class in inherits:object
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/
H A DMakefile6 ln -fs ../minisat/Proof.o
9 ln -fs ../minisat/Proof.h
13 g++ -O3 Proof.o File.o zc2hs.cpp -o zc2hs
/seL4-l4v-10.1.1/HOL4/examples/elliptic/
H A DellipticTools.sig17 (* Proof tools. *)
H A DellipticTools.sml23 (* Proof tools. *)
H A DfieldTools.sig35 (* Proof tools. *)
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/
H A DProof.h0 /*****************************************************************************************[Proof.h]
32 // A "listner" for the proof. Proof events will be passed onto (online mode) or replayed to
45 class Proof { class
58 Proof(); // Offline mode -- proof stored to a file, which can be saved, compressed, and/or traversed.
59 Proof(ClauseId goal); // Offline mode -- for pre-initialising c2fp
60 Proof(ProofTraverser& t); // Online mode -- proof will not be stored.
79 void compress (Proof& dst, ClauseId goal = ClauseId_NULL); // 'dst' should be a newly constructed, empty proof.
H A DProof.C0 /*****************************************************************************************[Proof.C]
20 #include "Proof.h"
63 // Proof logging:
65 Proof::Proof() function in class:Proof
75 Proof::Proof(ProofTraverser& t) function in class:Proof
83 ClauseId Proof::addRoot(vec<Lit>& cl, ClauseId orig_root_id)
109 void Proof::beginChain(ClauseId start)
118 void Proof
[all...]
/seL4-l4v-10.1.1/HOL4/src/1/
H A Dholmakebuild.sml13 ("*** Proof of \n " ^ Parse.term_to_string t ^ "\n*** failed (used CHEAT).\n")
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/cantor/
H A DCantor.ml1 % Proof of Cantor's Theorem %
/seL4-l4v-10.1.1/isabelle/src/Doc/Prog_Prove/document/
H A Droot.tex37 \chapter{Logic and Proof Beyond Equality}
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Prog_Prove/document/
H A Droot.tex37 \chapter{Logic and Proof Beyond Equality}
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DProof.sml6 structure Proof :> Proof = structure
139 handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err);
195 raise Bug ("Proof.recontructSubst: shouldn't fail:\n" ^ err);
215 raise Bug ("Proof.recontructResolvant: shouldn't fail:\n" ^ err);
221 val () = Print.trace LiteralSet.pp "Proof.reconstructEquality: cl" cl
272 "Proof.reconstructEquality: candidates" candidates
281 raise Bug ("Proof.recontructEquality: shouldn't fail:\n" ^ err);
309 val () = Print.trace Thm.pp "Proof.thmToInference: th" th
318 val () = Print.trace ppThmInf "Proof
[all...]
H A DProof.sig6 signature Proof = signature
H A DTptp.sml901 {inference : Proof.inference,
927 Proof.Axiom cl => LiteralSet.functions cl
928 | Proof.Assume atm => Atom.functions atm
929 | Proof.Subst (sub,_) => Subst.functions sub
930 | Proof.Resolve (atm,_,_) => Atom.functions atm
931 | Proof.Refl tm => Term.functions tm
932 | Proof.Equality (lit,_,tm) =>
954 Proof.Axiom cl => LiteralSet.relations cl
955 | Proof.Assume atm => NameAritySet.singleton (Atom.relation atm)
956 | Proof
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DProof.sml6 structure Proof :> Proof = structure
139 handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err);
195 raise Bug ("Proof.recontructSubst: shouldn't fail:\n" ^ err);
215 raise Bug ("Proof.recontructResolvant: shouldn't fail:\n" ^ err);
221 val () = Print.trace LiteralSet.pp "Proof.reconstructEquality: cl" cl
272 "Proof.reconstructEquality: candidates" candidates
281 raise Bug ("Proof.recontructEquality: shouldn't fail:\n" ^ err);
309 val () = Print.trace Thm.pp "Proof.thmToInference: th" th
318 val () = Print.trace ppThmInf "Proof
[all...]
H A DProof.sig6 signature Proof = signature
H A DTptp.sml901 {inference : Proof.inference,
927 Proof.Axiom cl => LiteralSet.functions cl
928 | Proof.Assume atm => Atom.functions atm
929 | Proof.Subst (sub,_) => Subst.functions sub
930 | Proof.Resolve (atm,_,_) => Atom.functions atm
931 | Proof.Refl tm => Term.functions tm
932 | Proof.Equality (lit,_,tm) =>
954 Proof.Axiom cl => LiteralSet.relations cl
955 | Proof.Assume atm => NameAritySet.singleton (Atom.relation atm)
956 | Proof
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/dff/
H A DdffScript.sml3 (* DESCRIPTION : Proof that a unit delay is implemented by a simple *)
59 (* Proof that there is no simple SINGLE abstraction from *)
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/Hahn_Banach/document/
H A Droot.tex69 \part {Lemmas for the Proof}
76 \part {The Main Proof}
/seL4-l4v-10.1.1/isabelle/src/HOL/Hahn_Banach/document/
H A Droot.tex69 \part {Lemmas for the Proof}
76 \part {The Main Proof}

Completed in 156 milliseconds

123456