Foundations For The Management Of Formal Mathematical Knowledge
Foundations for the Management of FormalMathematical KnowledgeRobert L. ConstableCornell UniversitySmall Types WorkshopNijmegen, November 200410/28/2004Nijmegen041
VisionVery large libraries (databases) of formal mathematicalknowledge, created and shared by the theorem provingcommunity, will make interactive theorem provers indispensibletools in parts of mathematics, science, and education as theyalready have become in formal methods and softwarepractice. In turn, the libraries will grow more rapidly andbecome interconnected with the intuitive mathematicalliterature, weaving threads of computational certainty into theoldest rigorous intellectual activity of human kind.10/28/2004Nijmegen042
MetaPRLMizarNuPRLCOQACL2HOLPVSTheorem proving systems as isolated islands,reaching a small community10/28/2004Nijmegen043
MetaPRLMizarNuPRLFormal Digital LibraryCOQACL2HOLPVSThe FDL joins all the small islands into a single big island thatcan accommodate much more than the sum of all individualislands, and allows people to stand on the ground in between.10/28/2004Nijmegen044
Challenges and Problems1. Community using formal proofs is relatively small Market for formal proofs is small– proof technology not widely used in software– proof technology not widely used inscience and math– proof technology not widely used in education Formal proving is still hard work– expansion factor– shallow base of basic mathematical facts– demanding skill set (programming math design)10/28/2004Nijmegen045
Challenges and Problems2. Community is disconnected Each group uses a different system Almost no sharing (logical difficulties, practical ones) Systems change or go extinct10/28/2004Nijmegen046
Digital Library Approach to the Challenges1. Widen the community by library will increase the services provided library will decrease the effort to createproofs (seen from experience)2. Connect the community through a common service– the digital libraries approach10/28/2004Nijmegen047
Outline1.2.3.Relating theories and systemsThe structure of theoriesAids to organization and search10/28/2004Nijmegen048
Type TheoriesThere are at least eleven active important interactiveprovers, some coupled to fully automatic provers such asJProver, Otter, TPS, and Omega.ACL2, Alf, Coq, HOL, Isabelle, MetaPRL, Minlog, Mizar, Nuprl, PVS, TwelfNine of these are based on higher-order typed logic. Why?Will there ever be ONE system? ONE logic? ONEframework? ONE metalogic?Will there ever be one Operating System? OneProgramming Language?10/28/2004Nijmegen049
Central Characters –Higher-Order Logics and Type TheoriesHOL/IsabelNuprl,BA BA BZ, Atomx :A Ba b in A x : A , x : Aa b in A x : A , x : Ax : A BCoq and Nuprl share many features, so Coq will bementioned as well.10/28/2004Nijmegen0410
Comparing Representative Type TheoriesLeast Number Principle (LNP):( P : N B. y : . P ( y ) x : . (P ( x ) & x : . z x P ( z ) )Law of Excluded Middle (LEM): P : Propi . (P P )10/28/2004Nijmegen0411)
Interpretations of LNPIn Nuprl LNP specifies a classof programs that includes:le a st(P , y ) fo r i 0 to y d oif P(i )the n re tu rn(i )e lse i : i 1e nd ; re tu rn(y ) .In HOL and PVS the function P B is ANY function,and it represents any propositional function, includingnoncomputable ones, e.g.:P(x,m) iff a Turing machine with xstates can print the number m andhalt starting with blank tape.10/28/2004Nijmegen0412
Interpretations of LEMIn Nuprl, LEM is not an axiom nor a theorem. There aremodels of Nuprl for which LEM , and LEM is false in thedomain theory of Nuprl.In HOL and PVS, LEM is an axiom.Adding LEM to Nuprl produces a theory we call ClassicalNuprl. Doug Howe proved that this theory is consistent.We will examine that proof.10/28/2004Nijmegen0413
Type Theory as a Specification LanguageInteger square root example10/28/2004–Thm 1.2 n : . ! r : . Root ( n , r )–Cor 1.1 rt :–Cor 1.2ext (Thm 1.1) ε–Cor 1.3 n : . Root ( n , ext (Thm 1.1)( n ) ) . n : . Root ( n , rt ( n ) )Nijmegen04 14
Interpretations of Integer Square RootThese theorems could be true in Coq, HOL, Nuprl, andPVS if HOL and PVS supported extraction of functions from statements according to the Semantics of Evidence; seemy MOD 1982 lecture notes, Assigning Meaning to Proofs;and my Handbook of Proof Theory article [39], “Types inLogic, Mathematics and Programming.”In Coq and Nuprl, the function in Cor 1.1 is computable.10/28/2004Nijmegen0415
The Root Program ExtractThe Working Material, Appendix A, p. 46, shows theextract term for this proof in ML notation:let rec sqrt i if i 0 then 0, pf 0 else let r , pf i 1 sqrt ( i - 1)in if ( r 1) n then r 1, pf i 2else r , pf i ' 10/28/2004Nijmegen0416
Relating theories and systems(early period)CLASSICALCONSTRUCTIVESimple type theory – STT(HOL, Isabelle)Intuitionistic type theory – ITT(Alf)Extended STT – STT (PVS)Computational type theory – CTT(Nuprl, MetaPRL)Calculus of Inductive Constructions – CIC(Coq, MetaPRL)10/28/2004Nijmegen0417
Relating theories and systems(current period)CLASSICALCONSTRUCTIVESimple type theory – STT(HOL, Isabelle)Constructive Simple type theory – CSTT(Berghofer/Nipkow 2002)Extended STT – STT (PVS)Intuitionistic type theory – ITTClassical – CTT (Howe 1997)PolymorphicComputationalincludes sets(Classical – Nuprl)10/28/2004Computational type theory – CTTCalculus of Inductive Constructions – CICNijmegen0418
Semantics of STTAndy Pitts gives a clean semantics of STT in ZF set theory.In that semantics:{} φ , {φ } , {φ , {φ }} ,.λ x : N.b ( x ) {〈 x , b ( x )〉 x 10/28/2004}is the set of functional relations onNijmegen04x.19
Semantics of CTTPer Martin-Lof provided an intuitive axiomatic semanticsbased on his doctrine of canonical forms.Stuart Allen gave a PER (partial equivalence relation)semantics in a neutral theory of inductive definitions.In that semantics: all terms that evaluate to canonical integers{n} { x : Term x n}is z 10/28/2004{ z} zNijmegen0420
Semantics of CTTλ x.b ( x ) is defined by evaluation rulesthink of {3} { f 3} is ({z} {fz})f z:λ x.x is in all A A!10/28/2004Nijmegen0421
Subtyping in CTT versus Set TheoryNotice Even BIn CTT,Even Bconsider λ x.rm(x,2)In Set Theory, any f in Even Bis a subset of a function in B10/28/2004Nijmegen0422
The Cumulative Hierarchy of Sets.ω ω.ωP ( P (φ ) )P (φ )φ p(iφ )i 0Captures the intuition of collecting stages and co-finality unending stages.10/28/2004Nijmegen0423
Zermelo Fraenkel Set Theory (ZF)ZF can be axiomatized in 1st order logic by axioms, 2axiom schemas (separation, replacement). Axiom ofchoice is a 9th axiom.Z0 φThe hierarchy is defined as:Z α Zββ αZ α 1 P ( Z α )Z Zαα OrdEvery ZF set x is in some Zα ; its rank is the least suchordinal α.10/28/2004Nijmegen0424
Semantics for 4ZCCZWernerZFC25
An Intuitionistic Cumulative Hierarchy of Sets.ω.C-STTintoIZFω ωP ( P (φ ) )P (φ )PropφFirst Order Logic (FOL) Base with proof terms (proofs-as-programs.)10/28/2004Nijmegen0426
Review of Set Theoretic Semantics“Structured Sets”Types(HOL, PVS, MML0 )A {αi }ω ωαi - - - - - - - rank (αi )ωThe Cumulative Hierarchy of Sets10/28/2004Nijmegen0427
Goal of Howe’s Approacha1 , a 2 , , ai PureType Theoryf (a )f λ x .b p a , b λ x .b a , b c i (a ) UienlargeType TheorywithSet TermsAf λ x .bλ x .b a10/28/2004α1 , α 2 , , α i a1 , a 2 , , ai bγA( )f (a ) ϕ αf ϕc i (α ) c i (α ) a ,b α , β Nijmegen04c i (a )( )ci α28
Howe’s Meaning FunctionsHowe’s Approach to Set-theoretic Semantics:like Pitts, Dybjer, Troelstra, and others, Doug Howe mapstypes into sets; for A, a type,A is a set.However, he introduces new ideas to handle functionality,polymorphism, subtyping, quotient types, and types as objects(universes). For instance,λ x .xA Ais an element ϕ of A Aand he writes that ϕ10/28/2004Nijmegen04λ x .x .29
Limitations of Set EmbeddingUnlike with PVS and HOL, no embedding can cover allof Nuprl because Recursive types allow T (T B ) B Domains all absolutely unsolvable problemsBut Howe gets a very substantial part and Moranextends to more.10/28/2004Nijmegen0430
Goal of Howe’s Approach Extend the family of “structured sets” Create constants for all “structured sets” Extend evaluation to all terms Define approximation (covering)αi aito relate sets αi to terms ai10/28/2004Nijmegen0431
Howe’s Method1. Encode type terms and types into sets in the cumulativeγhierarchy W ty , γ fn , ϕ c i α1 , , α n ϕc i (α )2.Define a subset of W with a unique meaning property; call it V.3.Define a term model for all V sets; call it T0 .4.Define evaluation and approximation on T0 ; this provides acomputational type theory with set oracles.I present a variant used by Evan Moran to extend Howe’s results.10/28/2004Nijmegen0432
Extending Set Theoretic Semanticsto ML-82, Alf, Nuprl.Can we account for these ideas in set theory?Can we embed CTT into the cumulative hierarchy?Uj.τ i are s33
Howe’s SemanticsWe think of types as collections of equivalence classes of terms:. . . aior.We need to allow sets representing equivalence classesαi into the collection of types.written γ {α1 , α 2 , , α n }α1 , α 2 , , α nwhere αi covers ai10/28/2004(α iapproximates ai ) αiNijmegen04ai34
Disjointness and IncompatibilityThe equivalence classes are disjoint, of course.A a1a2 . . . ai.if ai a j 0 thenai a jThe set elements must also be incompatible:γ A {α1 , α 2 , , αi }con(αi , α j ) implies αi α jFor each ai A there will be a unique αi γ A , such that αi10/28/2004Nijmegen04aj.35
Disjointness and IncompatibilityThe key condition for functions is:ϕϕ' α1 , β1 , α 2 , β 2 , , αi , βi , α'1 , β'1 , α'2 , β'2 , , α'i , β'i , If for all α , β , α ', β ' con ( αi , α'i ) implies con ( βi , β'i )thencon ( ϕ , ϕ' )10/28/2004Nijmegen0436
Compatibility (Consistency) Examples 00 and 11 are compatible (consistent) sinceϕ { 0, 0 } and ϕ { 1,1 } have a non-emptyintersection, ϕ { 0, 0 , 1,1 } . 0(00 ) and 0(11) are compatible,i.e. ϕ { 0, ϕ { 0, 0 } } con ϕ { 0, ϕ { 1, 1 } }since 0 con 0 and ϕ { 0, 0 } con ϕ { 1, 1 } .10/28/2004Nijmegen0437
Membership and ApproximationIf the type A is interpreted as the set γ A , then for eacha A , there is a unique α such thatαa.We will say A γ A and10/28/2004Nijmegen04aA α.38
Uniqueness TheoremFor any term t in T 0 ,1.If γ 12.For all γ V and α1 , α 2 γ ,if α110/28/2004t and γ 2t and α 2Nijmegen04t , then γ 1 γ 2t , then α1 α 239
The Term Language T0Howe defines a term language, T0 , that includes theNuprl terms with binding, such asx : A B , x : A B , λ x .b , x : A B ,less ( n ; m ; a ; b ) , decide ( p ; x .a ; y .b ) , T 0 includes the constructors and constants, such asU i , nat {n } , pair (a ; b ) , inl (a ) , inr ( b ) , ap (f ; a ) , T 0 includes constants for all of the γ , ϕ , ξ , c i (α ) sets.Howe uses γ , ϕ , ξ to denote the set terms.10/28/2004Nijmegen0440
The Term Language T0Howe extends the evaluation relation to all terms,for example:ap ( λ x .b ; a ) c if b a / x cless ( 0;1; a ; b ) c if a c()For instance, ap λ x .x ; ϕ ϕ .10/28/2004Nijmegen0441
Evaluation Rulesf φ (α , β ) φ αf (a ) βγ γ10/28/2004a(apφ )f λ x .b b a / x v( ap λ )f (a ) vλ x .b λ x .bNijmegen04c i (a ) c i (a )42
Approximation Rulese v α vα e j α j(c i α 1 , , α n (α , β ) φφ†βλ x .b)aj(c i a 1 , , a n)b α / x † Howe does not use this rule because it is unproven when thenon-determinism of functions on quotient types is allowed.10/28/2004Nijmegen0443
ExamplesLet ϕ { 0, 4 , 1, 5 } ϕ ' { 0, 2 }ψ { ϕ ,17 , ϕ ',18 }ϕ ( 0 0 ) 4 because 00 0ϕλ x .x 4λ x .x 4 but not ϕ 'ψ ( λ x .x 4 ) 1710/28/2004Nijmegen0444
The Substitution LemmaIf αβa then for any term e ,e α / x implies β e a / x The intuition is that for any dem onstration of βe α / x ,if it does not exam ine α , then it also establishes βIf the derivation depends on α , then since αe a / x .a and a is aterm , there is m o re inform ation in a than in any approxim ationα , and that inform ation w ill establish the facts used about αe α / x using a in place of α .to show β10/28/2004Nijmegen0445
Rationale for the Substitution LemmaAssume αa and βe α / x e α / x means αβ λ x .e . β } , a singleton set, andThus, λ x .e γ {αTo say β(1) λ x .e γ {α } γ { β }(2) From α a we know a γ {α }From (1) and (2) we have ( λ x .e ) a γ {β } ,thus, e a / x γ {β } , and henceβ10/28/2004Nijmegen04e a / x .46
Soundness – the Meaning of x : A Bx :A Bis the set of functions ϕ withdomain A such that for all α , β ϕ ,β B α / x γ α .10/28/2004Nijmegen0447
Soundness of Function Elimination – ConclusionWe need to know thatthere is a β inf ( a ) B [a / x ] is defined, i.e.B [a / x ]βf (a ) .We know that for any α , β ϕ f , β B α / x , by the premise for f .To sayaA α m eans αa . (Recall "M em bershipand A pproxim ation.")10/28/2004Nijmegen0448
Soundness of Function Elimination –ConclusionBy the Substitution Lemma,B α / x , then γ αif γ B a / x ,thus, γ B α / x B a / x . Likewise, if β( ) then βf αf (a ) .But by the Substitution Lemma , we know βsince ϕ ff and βHence f (a )10/28/2004B [a / x ]( )ϕf α . B a / x Nijmegen04( )f α ,as required.49
Review of Set Theoretic Semantics“Structured Sets”Types(HOL, PVS, MML0 )A {αi }ω ωαi - - - - - - - rank (αi )ωCumulative Hierarchy of Sets10/28/2004Nijmegen0450
Issues with Nuprl Type TheoriesSome Nuprl theorems contradict classical set theory andclassical logic.(a) Nuprl can solve this recursion equation on types:T (T B ) Busing µ X . ( X B ) B.(b) Nuprl’s domain theory (bar types) includes this result: h :10/28/2004 B. x : . ( h ( x ) t iff x )Nijmegen0451
Nuprl has Union and IntersectionThe types A B , B x , A B ,x A Bx , x :A Bx Aall violate Howe’s construction as outlined.({0} {0}) ({1} {1})includes 00 and 1α1 but noβcan approximate both.10/28/2004Nijmegen0452
Outline1.2.3.Relating theories and systemsThe structure of theoriesAids to organization and search10/28/2004Nijmegen0453
Theory StructureShould theories be directory-like structures, as in Automathcontexts (a tree of knowledge)?These can be internalized as dependent records.{G:Type, op:GxGG; id:G, ax1: Assoc(G, op);ax2: Identity(G, op, id); }The FDL takes a different approach, more like a databasethan a file system.10/28/2004Nijmegen0454
Information Graph of the FDLobjectslogical dependencytextual linksaccounting linksmetalogical links10/28/2004Nijmegen0455
FDL contains formal objectsrulesdefinitionsalgorithms, ofs, partial proofscertificates10/28/2004Nijmegen0456
InferencesH 1 A G1 by J1 , H 2 A G2 by J 2 ,, H n A Gn by J nH A G by JHi a list of formulas (terms)Gia formula (term)Jia justification (rule, tactic)10/28/2004Nijmegen0457
ProofA proof is a dag of inferencesA G, AH A G, RH A G, RA G, AA G, AH A G, RH A G, RH A G, RH A G, RH A G, R10/28/2004Nijmegen0458
Example of DependenciesRULEDEFDEFTHM name1: T1by external THM name2 : T2 byproof10/28/2004Nijmegen0459
FDL allows sharing among collectionsPVS10/28/2004NuprlNijmegen04MetaPRL60
FDL performs archival functionsAutomath system Auto QE checked the followingformalization of Landau’s Grundlagen (August 17, 2004).Coq 5.0 created the following extract for the FundamentalTheorem of Algebra (June 14, 2003).Nuprl 5 checked that Total Order (TO) protocol satisfies P(June 5, 2003).MetaPRL compiler produced C code from TO, and P ispreserved (October 19, 2003).PVS 2.4 proved Menger’s theorem (September 15, 2003).10/28/2004Nijmegen0461
Formal Digital LibraryEditorEditorNuprl 5WebLibraryEvaluatorTHEORY defs, thms, tacticsrules, structureMaudeEvaluatorMetaPRLEvaluatorSoS (Lisp)EvaluatorTHEORYPRLdefs, thms, tacticsrules, structureTHEORY (HOL)defs, thms, tacticsrules, structureTranslatorJava10/28/2004EditorTHEORY defs, thms, tacticsrules, structureTHEORY(PVS)defs, thms, tacticsrules, structureTHEORY defs, thms, tacticsrules, 2
Prototype FDL – Data (Manual 3.1)Organized to eventually support closed mapsD Term(D)D are object names (abstract)Term(D) are objects with embedded referencesMap is closed under object reference.Working space is the current closed map.Basic data structure is the library table.10/28/2004Nijmegen0463
Closed MapsD Term( D )closed under reference (no dangling pointers)closedopen id , term( ) id , term( ) id , term( ) id , term( ) id , term( ) id , term( ) id , term( ) ? id , term( ) 10/28/2004Nijmegen0464
Abstract Object IdentifiersD D′impliesTerm ( D ) Term ( D′ )i.e. d d′ impliesdef ( d ) def ( d′ )thm ( d ) thm ( d′ )()(pf thm ( d ) pf thm ( d′ )10/28/2004Nijmegen04)65
Concepts for FDL Design FDL supports large-scale operations on collectionstheory translation, e.g. CZF to Type Theorycross linking via formal thesaurustransplanting theoremsclassical to constructive translations10/28/2004Nijmegen0466
Concepts for FDL Design FDL provides an experimental publication mediumCan solicit exemplary contributionshybrid articles – formal and informalelegant formalizationschallenging formalizationsexpository articleshypothetical formalizationsArticles directly include shared material10/28/2004Nijmegen0467
Outline1. Relating theories and systems2. The structure of theories3. Aids to organization and search10/28/2004Nijmegen0468
Objective Organize digital formal math by automated andadaptable means Exploratory analysis of formal structure10/28/2004Nijmegen0469
Motivation Collections are growing large; need for better automation,search, visualization, personalization very broad Can we exploit it in the same was as is done with thestructure of the web? Formal Mathematics is rich with structure; can we exploitthis as some kind of metadata?10/28/2004Nijmegen0470
Method Graph-based approach to exploit meta-information from thestructure– relationships between theories are hidden, mass of objects, orderedby humans Internet search engines seems really smart; they exploit structure– Rank results according to “authority,” Google’s Page Rank– Teoma (www.teoma.com) allows you to “refine” search based onclusters Equate hyperlinks with dependencies, use “HITS”10/28/2004Nijmegen0471
Kleinberg’s “HITS” Algorithm HUBS10/28/2004AUTHORITIESNijmegen04Hubs point to good authorities &authorities point to good hubsSparse adjacency matrix, A– Hub vector 1steigenvector of AAT– Authority vector 1steigenvector of ATACommunities– Strongest hubs andauthorities from respectivenon-principle eigenvectors– Currently there areimproved techniques relyingon the same graph72
Iterative Algorithm Define x n , y n authority, hub weight for node n in graph Gwith edges E. x n y q q:(q,n)єE y n x q q:(n,q)єE Iterate 20 times, normalizing after each.10/28/2004Nijmegen0473
Design Decisions What are analogous to hubs and authorities in formalmath? Dependency Graphs– Theorems and Definitions (Rules, Tactics?)– Definitions have no (logical) dependencies Direct Forward Dependencies Control over size and components of Graph, “Seeding”primesgcdints10/28/2004Nijmegen0474
Graph Statistics Nuprl5 Standard & Num Thy Subset Bickford’s Event egen0475
Nuprl5 Number Theory10/28/2004Nijmegen0476
Standard and Numthy Communities1 listify length, select listify id,int seg ind,select append front,decidable ex int seg, or,decidable, so apply11divides of absvals,absval assoced, absval wf2chrem exists aux a,gcd ex n,chrem exists aux,atomic char,prime elim, gcd exists n,bezout ident n, chrem exists3div 3 to 1, div 2 to 1,div 4 to 1, divide wf, nequal4eqff to assert, eqtt to assert,assert of bnot,assert of band, prop2 fincr formation, fincr wf,fincr wf2,equiv rel functionality wrt iff3 fib coprime, gcd sat gcd p,gcd sat pred, fib wf, gcd wfycomb, not wf4 atomic char, assert of eq int,prime elim, assert of eq atom,le wf10/28/2004Nijmegen0477
Weight Distributions Nuprl5AUTHORITIESHUBS*HUBS.2.5.2Hub Weigh Seeded List Library.4.3.1.1Value V1Value V1.20.0171319 2531 37Case Number 434955 61 67737985 91970.01611 16 21 26 31 36 41 46 51 56 61 66 71 76 81 86 91Case Number.10.011162116312641365146615671668176Sorted Hub Weight IndexStep-like Weight Distributions– Booleans, lower plateau on authority graph– Stratified development of hubs, Bickford’s extended list theory10/28/2004Nijmegen0478918696
Level Distribution Def: A node, n, is in level, i, iff n depends only on nodes inlevels i, and i is the smallest value for which this is thecase. Characteristic peaks found, suggest characteristicsize/complexity of proofsNUPRL5EVENT SYSTEMS200700600500400100200Value V1Num 113151719212325272931Case NumberLEVEL10/28/2004100Nijmegen0479
HELM Coq Library Comparison Nuprl5Event Systems Coq in HELMNodes 5586378765-0.29491795 130648921070816648-0.158965346 5170176132309363093-0.1884646132 was /Coq/Reals/RiemannInt/RiemannInt P2810/28/2004Nijmegen0480
Coq Graph10/28/2004Nijmegen0481
Coq Link AnalysisCoq OutlinksCOQ 2345062468LOGDEPSLOGDEPS Similar link distribution 4567LOGLINKSLOGLINKS10/28/20040-1Nijmegen0482
Coq HITSAUTHORITIES/Init/Logic/eq.ind/Init/Logic/eq ind/Reals/Rdefinitions/R/Init/Logic/eq ind go alt/cos bound/Reals/SeqProp/cv speed pow fact/Reals/RiemannInt/RiemannInt P12RiemannInt P6RiemannInt P28/Reals/Rtopology/Heine/Reals/Alembert/Alembert C2/Reals/RiemannInt/RiemannInt P25RiemannInt P8Nijmegen0483
Coq Communities Logic/Berardi/inv Arith/Wf nat/induction gtof1Arith/Wf nat/lt wf rec1 IntMap/Mapaxioms/MapMerge assocLogic/Berardi/i Logic/Berardi/j Bool/Bvector/VconstBool/Bvector/vector rec Bool/Bvector/vector indInit/Datatypes/bool ind Init/Datatypes/bool recLogic/ClassicalFacts/f1 o f2IntMap/Mapaxioms/FSetUnion idempotentIntMap/Mapc/MapMerge idempotent c Logic/Diaconescu/proof irrelLogic/Berardi/retract rect IntMap/Mapaxioms/MapMerge assocLogic/Eqdep/eq dep dep1 Logic/Eqdep/eq dep1 eqRelations/Newman/Newman Init/Datatypes/bool rectBool/Bvector/vector rect IntMap/Mapaxioms/MapMerge assoc10/28/2004Nijmegen0484
Coq Communities II Logic/Hurkens/lemma2 Logic/Hurkens/U Logic/Hurkens/sbLogic/Hurkens/le Logic/Hurkens/UInit/Logic Type/identity rect r Init/Logic Type/identity rec rInit/Logic Type/identity ind r Init/Datatypes/identity rectromega/ReflOmegaCore/Tred factor3 stableomega/OmegaLemmas/fast Zred factor3ZArith/auxiliary/Zred factor3 romega/ReflOmegaCore/Tred factor3ring/Ring abstract/minus varlist insert okring/Ring abstract/minus varlist insertring/Ring theory/Th plus zero left2 ring/Ring theory/Th plus comm10/28/2004Nijmegen0485
Coq HITSHUB WEIGHTAUTH 20.10.010.05001 51 101 151 201 251 301 351 401 451 501 551 601 651 701 7511815 22 29 36 43 50 57 64 71 78 85 92 99 Smoother weight degradation Very small hub values10/28/2004Nijmegen0486
ReferencesP. Aczel. Notes on the simply typed lambda calculus. In Berger and Schwichtenberg. 1999.P. Aczel. The type theoretic interpretation of constructive set theory: Inductive definition. In Logic, Methodology andPhilosophy of Science VII.1986.P. Aczel and M. Rathjen. Notes on Constructive Set Theory. Mittag-Leffler Technical Report No.40, 2000/2001.P. Aczel. The type theoretic interpretation of constructive set theory. In Logic Colloquium ’77.P. Aczel. The type theoretick interpretations of constructive set theory: Choice principles. In The L.E.J. BrouwerCentenary Symposium. 1982.S. Allen. Abstract identifiers, intertextual reference and a computational basis for recordkeeping. First Monday,9(2), 2004. www.firstmonday.orgS. Allen. A Non-type-theoretic Definition of Martin-Lof’s Types. In Gries. 1997.H. Barendregt and H. Geuvers. Proof Assistants using dependent type systems. In Handbook of AutomatedReasoning. 2001.S. Berghofer. Proofs, Programs and Executable Specifications in Higher Order Logic. PhD thesis, TechnischeUniversitat Munchen, 2003.S. Berghofer and T. Nipkow. Executing higher order logic. In Types for Proofs and Programs: TYPES 2000. 2002.dR. Constable. Types in logic, mathematics and programming. In S. R. Buss, editor, Handbook of Proof Theory. 1998.D. Howe. Importing mathematics from HOL into Nuprl. In Theorem Proving in Higher Order Logics, volume 1125, ofLecture Notes in Computer Science. 1996.D. Howe. Semantic foundations for embedding HOL in Nuprl. In volume 1101 of Lecture Notes in Computer Science.1996.E. Moran. Adding Intersection and Union Types to Howe’s Model of Type Theory [working title]. PhD thesis, CornellUniversity, 2003.10/28/2004Nijmegen0487
1. Community using formal proofs is relatively small Market for formal proofs is small - proof technology not widely used in software - proof technology not widely used in science and math - proof technology not widely used in education Formal proving is still hard work - expansion factor - shallow base of basic mathematical facts
May 02, 2018 · D. Program Evaluation ͟The organization has provided a description of the framework for how each program will be evaluated. The framework should include all the elements below: ͟The evaluation methods are cost-effective for the organization ͟Quantitative and qualitative data is being collected (at Basics tier, data collection must have begun)
Silat is a combative art of self-defense and survival rooted from Matay archipelago. It was traced at thé early of Langkasuka Kingdom (2nd century CE) till thé reign of Melaka (Malaysia) Sultanate era (13th century). Silat has now evolved to become part of social culture and tradition with thé appearance of a fine physical and spiritual .
On an exceptional basis, Member States may request UNESCO to provide thé candidates with access to thé platform so they can complète thé form by themselves. Thèse requests must be addressed to esd rize unesco. or by 15 A ril 2021 UNESCO will provide thé nomineewith accessto thé platform via their émail address.
̶The leading indicator of employee engagement is based on the quality of the relationship between employee and supervisor Empower your managers! ̶Help them understand the impact on the organization ̶Share important changes, plan options, tasks, and deadlines ̶Provide key messages and talking points ̶Prepare them to answer employee questions
Dr. Sunita Bharatwal** Dr. Pawan Garga*** Abstract Customer satisfaction is derived from thè functionalities and values, a product or Service can provide. The current study aims to segregate thè dimensions of ordine Service quality and gather insights on its impact on web shopping. The trends of purchases have
Bruksanvisning för bilstereo . Bruksanvisning for bilstereo . Instrukcja obsługi samochodowego odtwarzacza stereo . Operating Instructions for Car Stereo . 610-104 . SV . Bruksanvisning i original
Chính Văn.- Còn đức Thế tôn thì tuệ giác cực kỳ trong sạch 8: hiện hành bất nhị 9, đạt đến vô tướng 10, đứng vào chỗ đứng của các đức Thế tôn 11, thể hiện tính bình đẳng của các Ngài, đến chỗ không còn chướng ngại 12, giáo pháp không thể khuynh đảo, tâm thức không bị cản trở, cái được
10 tips och tricks för att lyckas med ert sap-projekt 20 SAPSANYTT 2/2015 De flesta projektledare känner säkert till Cobb’s paradox. Martin Cobb verkade som CIO för sekretariatet för Treasury Board of Canada 1995 då han ställde frågan
