Statistics for TWiki.Mizar Web Month: Topic views: Topic saves: File uploads: Most popular topic views: Top contributors for topic save and uploads: Jul 2008 7064 ...
Articles that are being worked on: Author(s) Article Title Start Date Percent Complete Main.JesseAlama VECTSP11 Bases of Finite and Countable Vector Spaces 2007-06 ...
M(ost uch) of M(izar ath) Matches (MoMM) MoMM is a matching, interreduction and database tool for mathematical databases, optimized for Mizar, the description is ...
NOTIFYTOPIC is a subscription service to be automatically notified by email when topics change in the TWiki.Mizar web. This is a convenient service, so you do not ...
Mizar syntax Main.GrzegorzBancerek 12 Dec 2007 Redefinition-Block cannot repeat (it is intention, not practice(?)). In Identify-Registration, the intention is to ...
Podr #281;cznik Wersja angielska Mizar co to jest? Mizar jest proof checkerem wyposa #380;onym we w #322;asny j #281;zyk i bibliotek #281; artyku #322; #243;w matematycznych ...
Tu powinny sie znalezc kryteria, ktorymi maja sie kierowac recenzenci przy recenzji artykulu do FM (i MML) Main.GrzegorzBancerek 09 Dec 2005 0. W bibie obowiazkowe ...
Taktyki dowodowe do g #211;ry Taktyki dowodowe zale #380; #261; od korelat #243;w semantycznych: korelat dowodzonej formu #322;y (z ewentualnymi rozwini #281;ciami ...
Mizar TWiki The Mizar web is the main collaboration area for people using the Mizar proof checker and people involved in its implementation or implementation of related ...
MPTP Challenge: Why, What, How, Results, What to do Next TOC Current TPTP, CASC, ATP TPTP in 2003: mostly CNF problems ATPs working mostly in CNF, only a few exceptions ...
The grammar of Mizar with examples, comments and suggestions Editable version of the grammar is now available as appendix to MizarSyntax, view it at http://wiki.mizar ...
Suggestion: Revising FINSEQ 1:20 FINSEQ 1:20 is a nice little minitheorem on composing finite sequences with other functions: for f being Function for p being FinSequence ...
Suggestion: Revising MATRLIN:20 MATRLIN:20 is the theorem for K being Field for V2, V1 being finite-dimensional VectSp of K for f being Function of V1,V2 for p being ...
Mathematics Subject Classification 2000 Classified 259 articles on 962 (MML Version 4.81), see MathSC2000 for listing of existing classification pages. Section P ...
26 Real functions Section P S 26A Functions of one variable 25 26B Functions of several variables 26C Polynomials, rational functions 26D Inequalities For maximal ...
26D15 Inequalities Inequalities for sums, series and integrals Primary classification # Article 1 series 3 On the Partial Product of Series and Related Basic Inequalities ...
26D Inequalities Section P S 26D05 Inequalities for trigonometric functions and polynomials 26D07 Inequalities involving other types of functions 26D10 Inequalities ...
40 Sequences, series, summability Section P S 40A Convergence and divergence of infinite limiting processes 6 40B05 Multiple sequences and series 40C General summability ...
40A Convergence and divergence of infinite limiting processes Section P S 40A05 Convergence and divergence of series and sequences 6 40A10 Convergence and divergence ...
40A05 Convergence and divergence of infinite limiting processes Convergence and divergence of series and sequences Primary classification # Article 1 seq 1 Real ...
Main.KrzysztofRetel's instruction for local installation of MmlQuery I present one possible installation of MML Query engine locally. First you have to download ...
Automated translation in Formalized Mathematics by Main.GrzegorzBancerek 09 Dec 2005 I don't know if the whole translation can be re-programmed inside XSLT, however ...
28A25 Classical measure theory Integration with respect to measures and other set functions Primary classification # Article 1 mesfunc3 Lebesgue Integral of Simple ...
28A Classical measure theory Section P S 28A05 Classes of sets (Borel fields, $\sigma$-rings, etc.), measurable sets, Suslin sets, analytic sets See also 03E15, 26A21 ...
28 Measure and integration Section P S 28A Classical measure theory 13 28B Set functions, measures and integrals with values in abstract spaces 28C Set functions ...
FAQ: Question: How to install Mizar system on PC with Windows XP and get the first example article? Answer: Main.MichaelNedzelsky 13 Jul 2005 Step by step introduction ...
Error Number: 300 Mizar Message: Identifier expected Description Please contribute Typical examples (As far as I know, this is a typical example; I wouldn't call ...
Suggestion: Use expandable mode definition of Field In VECTSP 1, I find the reservation block: reserve F for Field, x for Element of F, V for VectSp-like add-associative ...
20E15 Structure and classification of infinite or finite groups Chains and lattices of subgroups, subnormal subgroups Primary classification # Article 1 group 4 ...
20E Structure and classification of infinite or finite groups Section P S 20E05 Free nonabelian groups 20E06 Free products, free products with amalgamation, Higman ...
20A05 Foundations Axiomatics and elementary properties Primary classification # Article 1 group 1 Groups Wojciech A. Trybulec 2 group 2 Subgroup and Cosets of Subgroups ...
20A Foundations Section P S 20A05 Axiomatics and elementary properties 6 20A10 Metamathematical considerations For word problems, see 20F10 20A15 Applications of ...
20 Group theory and generalizations Section P S 20A Foundations 6 20B Permutation groups 20C Representation theory of groups See also 19A22 (for representation rings ...
18 Category theory; homological algebra Section P S 18A General theory of categories and functors 8 18B Special categories 1 18C Categories and theories 18D Categories ...
18B40 Special categories Groupoids, semigroupoids, semigroups, groups Primary classification # Article 1 grcat 1 Categories of Groups Michal Muzalewski Secondary ...
18B Special categories Section P S 18B05 Category of sets, characterizations See also 03-xx 18B10 Category of relations, additive relations 18B15 Embedding theorems ...
13F07 Arithmetic rings and other special rings Euclidean rings and generalizations Primary classification # Article 1 int 3 The Ring of Integers, Euclidean Rings ...
13F Arithmetic rings and other special rings Section P S 13F05 Dedekind, Prüfer and Krull rings and their generalizations 13F07 Euclidean rings and generalizations ...
13 Commutative rings and algebras Section P S 13A General commutative ring theory 13B Ring extensions and related topics 13C Theory of modules and ideals 13D Homological ...
11 Number theory Section P S 11A Elementary number theory For analogues in number fields, see 11R04 11 11B Sequences and sets 11C Polynomials and matrices 11D Diophantine ...
11A Elementary number theory Section P S 11A05 Multiplicative structure; Euclidean algorithm; greatest common divisors 5 11A07 Congruences; primitive roots; residue ...