03 Mathematical logic and foundations Section P S 03A05 Philosophical and critical For philosophy of mathematics, see also 00A30 03B General logic 9 03C Model theory ...
03B General logic Section P S 03B05 Classical propositional logic 03B10 Classical first-order logic 9 03B15 Higher-order logic and type theory 03B20 Subsystems of ...
General logic Classical first-order logic Primary classification # Article 1 qc lang1 A First Order Language Piotr Rudnicki and Andrzej Trybulec 2 qc lang2 Connectives ...
03C Model theory Section P S 03C05 Equational classes, universal algebra See also 08Axx, 08Bxx, 18C05 03C07 Basic properties of first-order languages and structures ...
Model theory Models of arithmetic and set theory Primary classification # Article 1 zf lang A Model of ZF Set Theory Language Grzegorz Bancerek 2 zf model Models ...
03E Set theory Section P S 03E02 Partition relations 03E04 Ordered sets and their cofinalities; pcf theory 03E05 Other combinatorial set theory 03E10 Ordinal and ...
03E10 Set theory Ordinal and cardinal numbers Primary classification # Article 1 ordinal1 The Ordinal Numbers. Transfinite Induction and Defining by Transfinite ...
03E20 Set theory Other classical set theory Primary classification # Article 1 hidden Built-in Concepts Andrzej Trybulec 2 tarski Tarski Grothendieck Set Theory ...
03E25 Set theory Axiom of choice and related propositions Primary classification # Article Secondary classification # Article 1 wellord2 Zermelo Theorem and Axiom ...
03E55 Set theory Large cardinals Primary classification # Article 1 card fil Basic facts about inaccessible and measurable cardinals Josef Urban 2 card lar Mahlo ...
03E65 Set theory Other hypotheses and axioms Primary classification # Article Secondary classification # Article 1 tarski Tarski Grothendieck Set Theory Andrzej ...
03E99 Set theory None of the above, but in this section Primary classification # Article 1 finseq 1 Segments of Natural Numbers and Finite Sequences Grzegorz Bancerek ...
05 Combinatorics Section P S 05A Enumerative combinatorics 05B Designs and configurations For applications of design theory, see 94C30 05C Graph theory For applications ...
05C Graph theory Section P S 05C05 Trees 6 05C07 Degree sequences 05C10 Topological graph theory, imbedding See also 57M15, 57M25 05C12 Distance in graphs 05C15 Coloring ...
05C05 Graph theory Trees Primary classification # Article 1 trees 1 Introduction to Trees Grzegorz Bancerek 2 trees 2 K\"onig's Lemma Grzegorz Bancerek 3 trees 3 ...
06B Lattices Section P S 06B05 Structure theory 06B10 Ideals, congruence relations 06B15 Representation theory 06B20 Varieties of lattices 06B23 Complete lattices ...
06B99 Lattices None of the above, but in this section Primary classification # Article 1 nat lat The Lattice of Natural Numbers and The Sublattice of it. The Set ...
06E Boolean algebras (Boolean rings) Section P S 06E05 Structure theory 06E10 Chain conditions, complete algebras 06E15 Stone space and related constructions 06E20 ...
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 ...
11A05 Elementary number theory Multiplicative structure; Euclidean algorithm; greatest common divisors Primary classification # Article 1 nat 1 The Fundamental Properties ...
11A41 Elementary number theory Primes Primary classification # Article 1 nat 3 Fundamental {T}heorem of {A}rithmetic Artur Korni{\l}owicz and Piotr Rudnicki Secondary ...
11A51 Elementary number theory Factorization; primality Primary classification # Article 1 pepin Public-Key Cryptography and Pepin's Test for the Primality of Fermat ...
11A55 Elementary number theory Continued fractions Primary classification # Article 1 real 3 Simple Continued Fractions and Their Convergents Bo Li , Yan Zhang and ...
12 Field theory and polynomials Section P S 12D Real and complex fields 5 12E General field theory 12F Field extensions 12G Homological methods (field theory) 12H ...
12D Real and complex fields Section P S 12D05 Polynomials: factorization 12D10 Polynomials: location of zeros (algebraic theorems) For the analytic theory, see 26C10 ...
Real and complex fields None of the above, but in this section Primary classification # Article 1 numbers Subsets of Complex Numbers Andrzej Trybulec 2 xcmplx 0 ...
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 ...
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 ...
13F07 Arithmetic rings and other special rings Euclidean rings and generalizations Primary classification # Article 1 int 3 The Ring of Integers, Euclidean Rings ...
15 Linear and multilinear algebra; matrix theory Section P S 15A03 Vector spaces, linear dependence, rank 16 1 15A04 Linear transformations, semilinear transformations ...
15A03 Linear and multilinear algebra; matrix theory Vector spaces, linear dependence, rank Primary classification # Article 1 rlvect 1 Vectors in Real Linear Space ...
16 Associative rings and algebras Section P S 16B General and miscellaneous 16D Modules, bimodules and ideals 13 16E Homological methods For commutative rings, see ...
16D Modules, bimodules and ideals Section P S 16D10 General module theory 11 16D20 Bimodules 16D25 Ideals 16D30 Infinite-dimensional simple rings (except as in 16Kxx ...
16D10 Modules, bimodules and ideals General module theory Primary classification # Article 1 vectsp 2 Construction of Rings and Left-, Right-, and Bi-Modules over ...
16D40 Modules, bimodules and ideals Free, projective, and flat modules and ideals Primary classification # Article 1 mod 3 Free Modules Michal Muzalewski Secondary ...
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 ...
18A General theory of categories and functors Section P S 18A05 Definitions, generalizations 8 18A10 Graphs, diagram schemes, precategories See especially 20L05 18A15 ...
18A05 General theory of categories and functors Definitions, generalizations Primary classification # Article 1 cat 1 Introduction to Categories and Functors Czes ...
18B Special categories Section P S 18B05 Category of sets, characterizations See also 03-xx 18B10 Category of relations, additive relations 18B15 Embedding theorems ...
18B40 Special categories Groupoids, semigroupoids, semigroups, groups Primary classification # Article 1 grcat 1 Categories of Groups Michal Muzalewski Secondary ...
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 ...
20A Foundations Section P S 20A05 Axiomatics and elementary properties 6 20A10 Metamathematical considerations For word problems, see 20F10 20A15 Applications of ...
20A05 Foundations Axiomatics and elementary properties Primary classification # Article 1 group 1 Groups Wojciech A. Trybulec 2 group 2 Subgroup and Cosets of Subgroups ...
20E Structure and classification of infinite or finite groups Section P S 20E05 Free nonabelian groups 20E06 Free products, free products with amalgamation, Higman ...
20E15 Structure and classification of infinite or finite groups Chains and lattices of subgroups, subnormal subgroups Primary classification # Article 1 group 4 ...
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 ...
26A Functions of one variable Section P S 26A03 Foundations: limits and generalizations, elementary topology of the line 6 26A06 One-variable calculus 26A09 Elementary ...
26A03 Functions of one variable Foundations: limits and generalizations, elementary topology of the line Primary classification # Article 1 arytm 2 Non negative ...
26A09 Functions of one variable Elementary functions Primary classification # Article 1 square 1 Some Properties of Real Numbers. Operations: min, max, square, and ...
26A24 Functions of one variable Differentiation (functions of one variable): general theory, generalized derivatives, meanvalue theorems Primary classification ...
26A99 Functions of one variable None of the above, but in this section Primary classification # Article 1 arytm 3 Arithmetic of Non Negative Rational Numbers Grzegorz ...
26D Inequalities Section P S 26D05 Inequalities for trigonometric functions and polynomials 26D07 Inequalities involving other types of functions 26D10 Inequalities ...
26D15 Inequalities Inequalities for sums, series and integrals Primary classification # Article 1 series 3 On the Partial Product of Series and Related Basic Inequalities ...
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 ...
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 ...
28A25 Classical measure theory Integration with respect to measures and other set functions Primary classification # Article 1 mesfunc3 Lebesgue Integral of Simple ...
33 Special functions Section P S 33B Elementary classical functions 8 33C Hypergeometric functions 33D Basic hypergeometric functions 33E Other special functions ...
33B Elementary classical functions Section P S 33B10 Exponential and trigonometric functions 8 33B15 Gamma, beta and polygamma functions 33B20 Incomplete beta and ...
33B10 Elementary classical functions Exponential and trigonometric functions Primary classification # Article 1 sin cos Trigonometric Functions and Existence of ...
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 ...
54 General topology Section P S 54A Generalities 54B Basic constructions 54C Maps and general types of spaces defined by maps 54D Fairly general properties 54E Spaces ...
54E Spaces with richer structures Section P S 54E05 Proximity structures and generalizations 54E15 Uniform structures and generalizations 54E17 Nearness spaces 54E18 ...
68 Computer science Section P S 68M Computer system organization 68N Software 1 68P Theory of data 4 68Q Theory of computing 38 68R Discrete mathematics in relation ...
68N Software Section P S 68N01 General 68N15 Programming languages 68N17 Logic programming 68N18 Functional programming and lambda calculus See also 03B40 68N19 Other ...
68N20 Software Compilers and interpreters Primary classification # Article 1 scm comp A compiler of arithmetic expressions for { \bf SCM } Grzegorz Bancerek and ...
68P Theory of data Section P S 68P01 General 68P05 Data structures 68P10 Searching and sorting 4 68P15 Database theory 68P20 Information storage and retrieval 68P25 ...
68P10 Theory of data Searching and sorting Primary classification # Article scmbsort Bubble Sort on SCM+FSA JingChao Chen and Yatsuka Nakamura scmisort Insert Sort ...
68Q Theory of computing Section P S 68Q01 General 68Q05 Models of computation (Turing machines, etc.) See also 03D10, 81P68 38 68Q10 Modes of computation (nondeterministic ...
68Q05 Theory of computing Models of computation (Turing machines, etc.) Primary classification # Article 1 ami 1 A Mathematical Model of CPU Yatsuka Nakamura and ...
94 Information and communication, circuits Section P S 94A Communication, information 94B Theory of error-correcting codes and error-detecting codes 94C Circuits ...
94C Circuits, networks Section P S 94C05 Analytic circuit theory 94C10 Switching theory, application of Boolean algebra; Boolean functions See also 06E30 94C12 Fault ...
94C99 Circuits, networks None of the above, but in this section Primary classification # Article 1 gate 1 Logic Gates and Logical Equivalence of Adders Yatsuka Nakamura ...
AdminTopic See TopicClassification for complete topic category list SEARCH{ " T opicClassification. (td..td value\ ). A dminTopic" casesensitive "on" regex "on" nosearch ...
Description of The Mizar Error Messages Describe the meaning of the Mizar error codes here, post typical or weird examples, suggest changes. SEARCH{ " T opicClassification ...
Answered Questions See also MizarQuestion: Ask your questions here, answer new questions! AssignedQuestions: Under investigation. AnsweredQuestions: Answered! ClosedUnanswered ...
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 ...
Bug: Incorrect Error Explanations Sometimes the error explanation is incorrect (or rather partially correct ... it does not take into account al possibilities). Test ...
Bug Reports This is the place to report bugs in Mizar. Note: Please start a new topic for each bug. New bug topic: (Use a name in TWiki.WikiNotation) Reported bugs ...
Bug: CheckerClusterRounding Checker (sometimes?) forgets to do the "cluster rounding up". Test case (taken from the Hagenberg course) having the cluster being T1 ...
How to do Computer Algebra in Mizar TOC Problem description Eventually, users will want to have things like inverse matrix for concrete 5x5 matrices quickly available ...
Suggestion: Rename the attribute "connected" We have definition let L be non empty RelStr; attr L is connected means :: WAYBEL 0:def 29 for x,y being Element of L ...
Libraries of Formalized Mathematics Deductive AI Meets the Inductive AI (originally a presentation for Main.JosefUrban's talk at the Knowledge Management in Formalized ...
Description of The Mizar Error Messages Describe the meaning of the Mizar error codes here, post typical or weird examples, suggest changes. See AllErrorMessages ...