TWiki> Mizar Web>WebIndex (2001-11-24, PeterThoeny?)EditAttach

Results from Mizar web retrieved at 01:48 (GMT)

03 Mathematical logic and foundations Section P S 03A05 Philosophical and critical For philosophy of mathematics, see also 00A30 03B General ...
03B General logic Section P S 03B05 Classical propositional logic 3 03B10 Classical first order logic 25 03B15 Higher order ...
03B05 General logic Classical propositional logic Primary classification # Article 1 lukasi 1 Propositional Calculus Grzegorz Bancerek, Agata Darmochwal ...
03B10 General logic Classical first order logic Primary classification # Article 1 qc lang1 A First Order Language Piotr Rudnicki and Andrzej Trybulec ...
03B44 General logic Temporal logic Primary classification # Article 1 ltlaxio2 The Derivations of Temporal Logic Formulas Mariusz Giero 2 ltlaxio3 The ...
03B45 General logic Modal logic Primary classification # Article 1 modal 1 Introduction to Modal Propositional Logic Alicia de~la~Cruz Secondary ...
03B70 General logic Logic in computer science Primary classification # Article 1 intpro 1 Intuitionistic Propositional Calculus in the Extended Framework ...
03C Model theory Section P S 03C05 Equational classes, universal algebra See also 08Axx, 08Bxx, 18C05 03C07 Basic properties of first ...
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 ...
03D Computability and recursion theory Section P S 03D03 Thue and Post systems, etc. 03D05 Automata and formal grammars in connection ...
Computability and recursion theory Recursive functions and relations, subrecursive hierarchies Primary classification # Article 1 recdef 2 Recursive Definitions ...
03E Set theory Section P S 03E02 Partition relations 2 03E04 Ordered sets and their cofinalities; pcf theory 1 03E05 Other ...
03E02 Set theory Partition relations Primary classification # Article 1 eqrel 1 Equivalence Relations and Classes of Abstraction Konrad Raczkowski, Pawel ...
03E04 Set theory Ordered sets and their cofinalities; pcf theory Primary classification # Article 1 orders 1 Partially Ordered Sets Wojciech A. Trybulec ...
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 xboole 0 Boolean Properties of Sets Definitions Library Committee 2 ...
03E25 Set theory Axiom of choice and related propositions Primary classification # Article 1 wellord2 Zermelo Theorem and Axiom of Choice. The correspondence ...
03E30 Set theory Axiomatics of classical set theory and its fragments Primary classification # Article 1 tarski Tarski Grothendieck Set Theory Andrzej ...
03E55 Set theory Large cardinals Primary classification # Article 1 card fil Basic facts about inaccessible and measurable cardinals Josef Urban 2 card ...
03E65 Set theory Other hypotheses and axioms Primary classification # Article Secondary classification # Article 1 tarski Tarski ...
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 ...
03G Algebraic logic Section P S 03G05 Boolean algebras See also 06Exx 2 03G10 Lattices and related structures See also 06Bxx ...
03G05 Algebraic logic Boolean algebras Primary classification # Article 1 xboolean On the Arithmetic of Boolean Values Library Committee 2 mboolean ...
03G25 Algebraic logic Other algebras related to logic Primary classification # Article 1 normform Algebra of Normal Forms Andrzej Trybulec 2 heyting1 ...
05 Combinatorics Section P S 05A Enumerative combinatorics 1 05B Designs and configurations For applications of design theory, see 94C30 ...
05A Enumerative combinatorics Section P S 05A05 Permutations, words, matrices 05A10 Factorials, binomial coefficients, combinatorial ...
05A10 Enumerative combinatorics Factorials, binomial coefficients, combinatorial functions Primary classification # Article 1 newton Factorial and Newton ...
05C Graph theory Section P S 05C05 Trees 7 05C07 Degree sequences 05C10 Topological graph theory, imbedding See also 57M15 ...
05C05 Graph theory Trees Primary classification # Article 1 trees 1 Introduction to Trees Grzegorz Bancerek 2 trees 2 K\"onig's Lemma Grzegorz Bancerek ...
05C17 Graph theory Perfect graphs Primary classification # Article 1 mycielsk The Mycielskian of a Graph Piotr Rudnicki, Lorna Stewart ...
05C20 Graph theory Directed graphs (digraphs), tournaments Primary classification # Article 1 glib 000 Alternative Graph Structures Gilbert Lee, Piotr ...
05C40 Graph theory Connectivity Primary classification # Article 1 friends1 The Friendship Theorem Karol Pak Secondary classification ...
05C99 Graph theory None of the above, but in this section Primary classification # Article 1 msscyc 1 The Correspondence Between Monotonic Many Sorted Signatures ...
06 Order, lattices, ordered algebraic structures Section P S 06A Ordered sets 11 06B Lattices See also 03G10 42 06C Modular ...
06A Ordered sets Section P S 06A05 Total order 06A06 Partial order, general 7 06A07 Combinatorics of partially ordered sets ...
06A06 Ordered sets Partial order, general Primary classification # Article 1 waybel 0 Directed Sets, Nets, Ideals, Filters, and Maps Grzegorz Bancerek ...
06A11 Ordered sets Algebraic aspects of posets Primary classification # Article 1 yellow10 The Properties of Product of Relational Structures Artur Kornilowicz ...
06A15 Ordered sets Galois correspondences, closure operators Primary classification # Article 1 waybel 1 Galois Connections Czeslaw Bylinski 2 waybel10 ...
06B Lattices Section P S 06B05 Structure theory 2 06B10 Ideals, congruence relations 5 06B15 Representation theory ...
06B05 Lattices Structure theory # Article 1 lattices Introduction to Lattice Theory Stanislaw Zukowski 2 lattice2 Finite Join and Finite Meet, and Dual ...
06B10 Lattices Ideals, congruence relations # Article 1 filter 0 Filters Part I Grzegorz Bancerek 2 filter 1 Filters Part II. Quotient Lattices Modulo ...
06B23 Lattices Complete lattices, completions # Article 1 lattice3 Complete Lattices Grzegorz Bancerek 2 waybel11 Scott Topology Andrzej Trybulec ...
06B30 Lattices Topological lattices, order topologies # Article 1 waybel18 Injective Spaces Jaroslaw Gryko 2 waybel24 Scott Continuous Functions. Part ...
06B35 Lattices Continuous lattices and posets, applications Primary classification # Article 1 waybel 2 Meet Continuous Lattices Artur Kornilowicz ...
06B99 Lattices None of the above, but in this section Primary classification # Article 1 setwiseo Semilattice Operations on Finite Subsets Andrzej Trybulec ...
06C Modular lattices, complemented lattices Section P S 06C05 Modular lattices, Desarguesian lattices 1 06C10 Semimodular lattices, geometric ...
06C05 Modular lattices, complemented lattices Modular lattices, Desarguesian lattices Primary classification # Article 1 yellow11 On the Characterization ...
06D Distributive lattices Section P S 06D05 Structure and representation theory 06D10 Complete distributivity 06D15 Pseudocomplemented ...
06D99 Distributive lattices None of the above, but in this section Primary classification # Article 1 latticea Prime Filters and Ideals in Distributive ...
06E Boolean algebras (Boolean rings) Section P S 06E05 Structure theory 06E10 Chain conditions, complete algebras 06E15 ...
06E25 Boolean algebras (Boolean rings) Boolean algebras with additional operations (diagonalizable algebras, etc.) Primary classification # Article 1 robbins1 ...
06E30 Boolean algebras (Boolean rings) Boolean functions Primary classification # Article 1 bvfunc 1 A Theory of Boolean Valued Functions and Partitions ...
06E99 Boolean algebras (Boolean rings) None of the above, but in this section Primary classification # Article 1 boolealg Boolean Properties of Lattices ...
06F Ordered structures Section P S 06F05 Ordered semigroups and monoids See also 20M 06F07 Quantales 06F10 Noether lattices ...
06F25 Ordered structures Ordered rings, algebras, modules Primary classification # Article 1 termord Term Orders Christoph Schwarzweller
06F35 Ordered structures BCK algebras, BCI algebras Primary classification # Article 1 bcialg 1 Several Classes of BCI algebras and Their Properties Yuzhong ...
08 General algebraic systems Section P S 08 00 General reference works (handbooks, dictionaries, bibliographies, etc.) 08 01 Instructional ...
08A Algebraic structures Section P S 08A02 Relational systems, laws of composition 1 08A05 Structure theory 3 08A30 Subalgebras ...
08A02 Algebraic structures Relational systems, laws of composition Primary classification # Article 1 yellow 3 Cartesian Products of Relations and Relational ...
08A05 Algebraic structures Structure theory Primary classification # Article 1 struct 0 Preliminaries to Structures Library Committee 2 instalg1 Institution ...
08A30 Algebraic structures Subalgebras, congruence relations Primary classification # Article 1 tdgroup A Construction of an Abstract Space of Congruence ...
08A35 Algebraic structures Automorphisms, endomorphisms Primary classification # Article 1 autalg 1 On the Group of Automorphisms of Universal Algebra and ...
08A40 Algebraic structures Operations, polynomials, primal algebras Primary classification # Article 1 polyalg1 The Algebra of Polynomials Ewa Gr #261 ...
08A55 Algebraic structures Partial algebras Primary classification # Article 1 pua2mss1 Minimal Signature for Partial Algebra Grzegorz Bancerek
08A70 Algebraic structures Applications of universal algebra in computer science Primary classification # Article Secondary classification ...
08A99 Algebraic structures None of the above, but in this section Primary classification # Article 1 unialg 1 Basic Notation of Universal Algebra Jaroslaw ...
08B Varieties Section P S 08B05 Equational logic, Mal'cev (Mal'tsev) conditions 2 08B10 Congruence modularity, congruence distributivity ...
08B05 Varieties Equational logic, Mal'cev (Mal'tsev) conditions Primary classification # Article 1 msualg 6 Translations, Endomorphisms, and Stable Equational ...
08B20 Varieties Free algebras # Article 1 freealg Free Universal Algebra Construction Beata Perkowska 2 msafree Free Many Sorted Universal Algebra Beata ...
08B25 Varieties Products, amalgamated products, and other kinds of limits and colimits Primary classification # Article 1 pralg 1 Product of Family of Universal ...
08C Other classes of algebras Section P S 08C05 Categories of algebras See also 18C05 1 08C10 Axiomatic model classes See also 03Cxx, in ...
08C05 Other classes of algebras Categories of algebras Primary classification # Article 1 msinst 1 Examples of Category Structures Adam Grabowski
11 Number theory Section P S 11A Elementary number theory For analogues in number fields, see 11R04 33 11B Sequences and sets 6 ...
11A Elementary number theory Section P S 11A05 Multiplicative structure; Euclidean algorithm; greatest common divisors 21 11A07 Congruences ...
11A05 Elementary number theory Multiplicative structure; Euclidean algorithm; greatest common divisors Primary classification # Article 1 arytm 3 Arithmetic ...
11A25 Elementary number theory Arithmetic functions; related numbers; inversion formulas Primary classification # Article 1 valued 1 Properties of Number ...
11A41 Elementary number theory Primes Primary classification # Article 1 nat 5 The Perfect Number Theorem and Wilson's Theorem Marco Riccardi 2 numeral2 ...
11A51 Elementary number theory Factorization; primality Primary classification # Article 1 pepin Public Key Cryptography and Pepin's Test for the Primality ...
11A55 Elementary number theory Continued fractions Primary classification # Article 1 real 3 Simple Continued Fractions and Their Convergents Bo Li , ...
11B Sequences and sets Section P S 11B05 Density, gaps, topology 11B13 Additive bases, including sumsets See also 05B10 11B25 ...
11B39 Sequences and sets Fibonacci and Lucas numbers and polynomials and generalizations Primary classification # Article 1 pre ff Two Programs for \bf ...
11B73 Sequences and sets Bell and Stirling numbers Primary classification # Article 1 stirl2 1 Stirling Numbers of the Second Kind Karol Pak ...
11C Polynomials and matrices Section P S 11C08 Polynomials See also 13F20 1 11C20 Matrices, determinants See also 15B36 11C99 ...
11C08 Polynomials and matrices Polynomials Primary classification # Article 1 uniroots Primitive Roots of Unity and Cyclotomic Polynomials Broderick Arneson ...
11R Algebraic number theory: global fields Section P S 11R04 Algebraic numbers; rings of algebraic integers 1 11R06 PV numbers and ...
11R04 Algebraic number theory: global fields Algebraic numbers; rings of algebraic integers Primary classification # Article 1 gaussint Gaussian Integers ...
11R52 Algebraic number theory: global fields Quaternion and other division algebras: arithmetic, zeta functions Primary classification # Article 1 quaterni ...
11S Algebraic number theory: local and p adic fi elds Section P S 11S05 Polynomials 1 11S15 Rami cation and extension theory ...
11S05 Algebraic number theory: local and p adic fields Polynomials Primary classification # Article 1 polyeq 1 Solving Roots of Polynomial Equations of ...
12 Field theory and polynomials Section P S 12D Real and complex fields 3 12E General field theory 10 12F Field extensions ...
12D Real and complex fields Section P S 12D05 Polynomials: factorization 12D10 Polynomials: location of zeros (algebraic theorems ...
12D99 Real and complex fields None of the above, but in this section Primary classification # Article 1 arithm Field Properties of Complex Numbers Requirements ...
12E General field theory Section P S 12E05 Polynomials (irreducibility, etc.) 10 12E10 Special polynomials 12E12 Equations ...
General field theory Polynomials (irreducibility, etc.) Primary classification # Article 1 pre poly Preliminaries to Polynomials Andrzej Trybulec 2 polynom1 ...
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 Section P S 13C05 Structure, classi cation theorems 13C10 Projective and free modules and ideals See ...
13C10 Theory of modules and ideals Projective and free modules and ideals Primary classification # Article 1 zmodul03 Free $\mathbb Z$ module Yuichi Futa ...
13C99 Theory of modules and ideals None of the above, but in this section Primary classification # Article 1 zmodul01 $\mathbb Z$ modules Yuichi Futa, ...
13F Arithmetic rings and other special rings Section P S 13F05 Dedekind, Prüfer and Krull rings and their generalizations 13F07 Euclidean ...
13F07 Arithmetic rings and other special rings Euclidean rings and generalizations Primary classification # Article 1 int 3 The Ring of Integers, Euclidean ...
14 Algebraic Geometry Section P S 14A Foundations 14B Local theory 14C Cycles and subschemes 14D Families ...
14R Affine geometry Section P S 14R05 Classi cation of affine varieties 14R10 Affine spaces (automorphisms, embeddings, exotic structures ...
Affine geometry Affine spaces (automorphisms, embeddings, exotic structures, cancellation problem) Primary classification # Article 1 aff 1 Parallelity ...
15 Linear and multilinear algebra; matrix theory Section P S 15 00 General reference works (handbooks, dictionaries, bibliographies, etc.) ...
15A Basic linear algebra 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 ...
15A04 Linear and multilinear algebra; matrix theory Basic linear algebra Linear transformations, semilinear transformations Primary classification # Article ...
15A06 Linear and multilinear algebra; matrix theory Basic linear algebra Linear equations Primary classification # Article 1 matrix15 Solutions of Linear ...
15A09 Linear and multilinear algebra; matrix theory Basic linear algebra Matrix inversion, generalized inverses Primary classification # Article 1 matrix14 ...
15A15 Linear and multilinear algebra; matrix theory Basic linear algebra Determinants, permanents, other special matrix functions Primary classification # Article ...
15A23 Linear and multilinear algebra; matrix theory Basic linear algebra Factorization of matrices Primary classification # Article 1 matrixj1 Block Diagonal ...
15A30 Linear and multilinear algebra; matrix theory Basic linear algebra Algebraic systems of matrices Primary classification # Article 1 matrix 1 Abelian ...
15A99 Linear and multilinear algebra; matrix theory Basic linear algebra Miscellaneous topics Primary classification # Article 1 matrix 5 A Theory of ...
16 Associative rings and algebras Section P S 16B General and miscellaneous 16D Modules, bimodules and ideals 13 16E ...
16D Modules, bimodules and ideals Section P S 16D10 General module theory 11 16D20 Bimodules 16D25 Ideals ...
16D10 Modules, bimodules and ideals General module theory Primary classification # Article 1 vectsp 2 Construction of Rings and Left , Right , and Bi Modules ...
16D40 Modules, bimodules and ideals Free, projective, and flat modules and ideals Primary classification # Article 1 mod 3 Free Modules Michal Muzalewski ...
16D90 Modules, bimodules and ideals Module categories Primary classification # Article 1 modcat 1 Category of Left Modules Micha{\l} Muzalewski ...
16W Rings and algebras with additional structure Section P S 16W10 Rings with involution; Lie, Jordan and other nonassociative structures See ...
16W60 Rings and algebras with additional structure Valuations, completions, formal power series and related constructions Primary classification # Article ...
18 Category theory; homological algebra Section P S 18A General theory of categories and functors 12 18B Special categories 1 ...
18A General theory of categories and functors Section P S 18A05 Definitions, generalizations 12 18A10 Graphs, diagram schemes, precategories ...
18A05 General theory of categories and functors Definitions, generalizations Primary classification # Article 1 cat 1 Introduction to Categories and Functors ...
18B Special categories Section P S 18B05 Category of sets, characterizations See also 03 xx 18B10 Category of relations, additive relations ...
18B40 Special categories Groupoids, semigroupoids, semigroups, groups Primary classification # Article 1 grcat 1 Categories of Groups Michal Muzalewski ...
20 Group theory and generalizations Section P S 20A Foundations 6 20B Permutation groups 20C Representation theory of ...
20A Foundations Section P S 20A05 Axiomatics and elementary properties 6 20A10 Metamathematical considerations For word problems, see ...
20A05 Foundations Axiomatics and elementary properties Primary classification # Article 1 group 1 Groups Wojciech A. Trybulec 2 group 2 Subgroup and ...
20E Structure and classification of infinite or finite groups Section P S 20E05 Free nonabelian groups 20E06 Free products, free products ...
20E15 Structure and classification of infinite or finite groups Chains and lattices of subgroups, subnormal subgroups Primary classification # Article 1 ...
20F Special aspects of infinite or finite groups Section P S 20F05 Generators, relations, and presentations 20F06 Cancellation theory ...
20F34 Special aspects of infinite or finite groups Fundamental groups and their automorphisms Primary classification # Article 1 topalg 1 The Fundamental ...
20M Semigroups Section P S 26A03 Foundations: limits and generalizations, elementary topology of the line 6 20M05 Free semigroups, generators ...
20M05 Semigroups Free semigroups, generators and relations, word problems Primary classification # Article 1 algstr 4 Free Magmas Marco Riccardi
20M14 Semigroups Commutative semigroups Primary classification # Article 1 algstr 0 Basic Algebraic Structures Library Committee
26A Functions of one variable Section P S 20N02 Sets with a single binary operation (groupoids) 20N05 Loops, quasigroups See also ...
26A03 Functions of one variable Foundations: limits and generalizations, elementary topology of the line Primary classification # Article 1 algstr 1 From ...
20N10 Other generalizations of groups Ternary systems (heaps, semiheaps, heapoids, etc.) Primary classification # Article 1 algstr 3 Ternary Fields Michal ...
26 Real functions Section P S 26A Functions of one variable 29 26B Functions of several variables 26C Polynomials, rational ...
26A Functions of one variable Section P S 26A03 Foundations: limits and generalizations, elementary topology of the line 6 26A06 One variable ...
26A03 Functions of one variable Foundations: limits and generalizations, elementary topology of the line Primary classification # Article 1 arytm 2 Non ...
26A09 Functions of one variable Elementary functions Primary classification # Article 1 square 1 Some Properties of Real Numbers. Operations: min, max, ...
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 ...
26D Inequalities Section P S 26D05 Inequalities for trigonometric functions and polynomials 26D07 Inequalities involving other types ...
26D15 Inequalities Inequalities for sums, series and integrals Primary classification # Article 1 series 3 On the Partial Product of Series and Related ...
28 Measure and integration Section P S 28A Classical measure theory 13 28B Set functions, measures and integrals with values in abstract ...
28A Classical measure theory Section P S 28A05 Classes of sets (Borel fields, $\sigma$ rings, etc.), measurable sets, Suslin sets, analytic sets ...
28A12 Classical measure theory Contents, measures, outer measures, capacities Primary classification # Article 1 measure1 The $\sigma$ additive Measure ...
28A20 Classical measure theory Measurable and nonmeasurable functions, sequences of measurable functions, modes of convergence Primary classification # Article ...
28A25 Classical measure theory Integration with respect to measures and other set functions Primary classification # Article 1 mesfunc3 Lebesgue Integral ...
33 Special functions Section P S 33B Elementary classical functions 8 33C Hypergeometric functions 33D Basic hypergeometric ...
33B Elementary classical functions Section P S 33B10 Exponential and trigonometric functions 8 33B15 Gamma, beta and polygamma functions ...
33B10 Elementary classical functions Exponential and trigonometric functions Primary classification # Article 1 sin cos Trigonometric Functions and Existence ...
40 Sequences, series, summability Section P S 40A Convergence and divergence of infinite limiting processes 6 40B05 Multiple sequences ...
40A Convergence and divergence of infinite limiting processes Section P S 40A05 Convergence and divergence of series and sequences 6 40A10 ...
40A05 Convergence and divergence of infinite limiting processes Convergence and divergence of series and sequences Primary classification # Article 1 seq ...
46 Functional analysis Section P S 46A Topological linear spaces and related structures For function spaces, see 46E 46B Normed linear ...
46C Inner product spaces and their generalizations, Hilbert spaces Section P S 46C05 Hilbert and pre Hilbert spaces: geometry and topology (including ...
Inner product spaces and their generalizations, Hilbert spaces Primary classification # Article 1 bhsp 1 Introduction to Banach and Hilbert Spaces Part ...
54 General topology Section P S 54A Generalities 4 54B Basic constructions 6 54C Maps and general types of spaces defined ...
54A Generalities Section P S 54A05 Topological spaces and generalizations (closure spaces, etc.) 4 54A10 Several topologies on one set ...
54A05 Generalities Topological spaces and generalizations # Article 1 yellow12 On the Characterization of Hausdorff Spaces Artur Kornilowicz 2 yellow15 ...
54B Basic constructions Section P S 54B05 Subspaces 54B10 Product spaces 54B15 Quotient spaces, decompositions ...
54B99 Basic constructions None of the above, but in this section # Article 1 yellow 9 Bases and Refinements of Topologies Grzegorz Bancerek 2 topgen ...
54E Spaces with richer structures Section P S 54E05 Proximity structures and generalizations 54E15 Uniform structures and generalizations ...
54E30 Spaces with richer structures Moore spaces # Article 1 yellow 6 Moore Smith Convergence Andrzej Trybulec
54E35 Spaces with richer structures Metric spaces, metrizability Primary classification # Article 1 metric 1 Metric Spaces Stanis{\l}awa Kanas, Adam Lecko ...
54E52 Spaces with richer structures Baire category, Baire spaces # Article 1 yellow 8 Baire Spaces, Sober Spaces Andrzej Trybulec 2 waybel12 On the Baire ...
68 Computer science Section P S 68M Computer system organization 4 68N Software 1 68P Theory of data 9 68Q Theory ...
68M Computer system organization Section P S 68M01 General 68M07 Mathematical problems of computer architecture 4 68M10 ...
68M07 Theory of computing Models of computation (Turing machines, etc.) Primary classification # Article 1 compos 0 Commands Structure Andrzej Trybulec ...
68N Software Section P S 68N01 General 68N15 Programming languages 68N17 Logic programming 68N18 Functional ...
68N20 Software Compilers and interpreters Primary classification # Article 1 scm comp A compiler of arithmetic expressions for { \bf SCM } Grzegorz Bancerek ...
68P Theory of data Section P S 68P01 General 68P05 Data structures 2 68P10 Searching and sorting 5 68P15 Database ...
68P05 Theory of data Data structures Primary classification # Article 1 stacks 1 Representation Theorem for Stacks Grzegorz Bancerek 2 matroid0 Introduction ...
68P10 Theory of data Searching and sorting Primary classification # Article 1 scmbsort Bubble Sort on SCM FSA JingChao Chen and Yatsuka Nakamura 2 ...
68P15 Theory of data Database theory Primary classification # Article 1 mmlquery Semantic of MML Query Grzegorz Bancerek 2 mmlquer2 The Semantics of ...
68Q Theory of computing Section P S 68Q01 General 68Q05 Models of computation (Turing machines, etc.) See also 03D10, 81P68 38 ...
68Q05 Theory of computing Models of computation (Turing machines, etc.) Primary classification # Article 1 ami 1 A Mathematical Model of CPU Yatsuka Nakamura ...
68T Artificial intelligence Section P S 68T01 General 68T05 Learning and adaptive systems See also 68Q32, 91E40 68T10 ...
68T35 Artificial intelligence Languages and software systems (knowledge based systems, expert systems, etc.) Primary classification # Article 1 abcmiz 0 ...
68W Algorithms Section P S 68W01 General 4 68W05 Nonnumerical algorithms 68W10 Parallel algorithms 68W15 ...
68W01 Algorithms General Primary classification # Article 1 aofa 000 Mizar Analysis of Algorithms: Preliminaries Grzegorz Bancerek 2 aofa i00 Mizar ...
94 Information and communication, circuits Section P S 94A Communication, information 94B Theory of error correcting codes and error ...
94C Circuits, networks Section P S 94C05 Analytic circuit theory 15 94C10 Switching theory, application of Boolean algebra; Boolean functions ...
94C05 Circuits, networks Analytic circuit theory # Article 1 pre circ Preliminaries to Circuits, I Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, Pauline ...
94C99 Circuits, networks None of the above, but in this section Primary classification # Article 1 gate 1 Logic Gates and Logical Equivalence of Adders ...
nop AdminTopic See TopicClassification for complete topic category list WikiRoot 04 Jul 2002
Description of The Mizar Error Messages Describe the meaning of the Mizar error codes here, post typical or weird examples, suggest changes. Related topics ...
Answered Questions See also MizarQuestion: Ask your questions here, answer new questions! AssignedQuestions: Under investigation. AnsweredQuestions ...
NewTechnology translation in Formalized Mathematics by GrzegorzBancerek 09 Dec 2005 I don't know if the whole translation can be re programmed inside XSLT, ...
Bug: Incorrect Error Explanations Sometimes the error explanation is incorrect (or rather partially correct ... it does not take into account al possibilities). ...
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 WikiNotation) ...
Bug: Enter bug title here I was able to deduce contradiction using the latest version of verifier. Test case Here's the article which proves that 2 2 5: I was ...
Bug: CheckerClusterRounding Checker (sometimes?) forgets to do the "cluster rounding up". Test case (taken from the Hagenberg course) having the cluster being ...
Removing non clusterable attributes, cluster mechanism propositions JosefUrban 07 Jul 2002
Collaborative Manual Polish version Abstracts Correctness Conditions Definitions Environment Formulae Proof Tactics Properties ...
How to do Computer Algebra in Mizar 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 ...
See http://megrez.mizar.org/ccl/ GrzegorzBancerek 15 Aug 2002
Libraries of Formalized Mathematics Deductive AI Meets the Inductive AI (originally a presentation for JosefUrban's talk at the Knowledge Management in Formalized ...
Form 2 Definition for the Mizar web Name: Type: Size: Values: Tooltip message: TopicClassification select 1 TWikiDeployment Classify ...
Definition for the Mizar web DocsAdminForm Name: Type: Size: Values: Tooltip message: TopicClassification select 1 Select one.. ...
Description of The Mizar Error Messages Describe the meaning of the Mizar error codes here, post typical or weird examples, suggest changes. See AllErrorMessages ...
Error Number: 10 Mizar Message: Too many basic sentences in an inference Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 100 Mizar Message: Inaccessible locus Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1001 Mizar Message: Invalid function number Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1002 Mizar Message: File not found Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1003 Mizar Message: Path not found Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1004 Mizar Message: Too many open files Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1005 Mizar Message: File access denied Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1006 Mizar Message: Invalid file handle Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 101 Mizar Message: Unknown mode Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1012 Mizar Message: Invalid file access code Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1015 Mizar Message: Invalid drive number Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1016 Mizar Message: Cannot remove current directory Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 1017 Mizar Message: Cannot rename across drives Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 1018 Mizar Message: No more files Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 102 Mizar Message: Unknown predicate Description Some causes of this error are: Omitting a necessary registration directive Overriding a ...
Error Number: 103 Mizar Message: Unknown functor Description The func being used is not defined on the argument type. Some causes of this error are (examples below ...
Error Number: 104 Mizar Message: Unknown structure Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 105 Mizar Message: Illegal projection Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 106 Mizar Message: Unknown attribute Description A declared attribute is inapplicable to the subject locus. If the attribute was not a vocabulary symbol ...
Error Number: 107 Mizar Message: Invalid list of arguments of redefined constructor Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 108 Mizar Message: Invalid list of arguments of redefined constructor Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 109 Mizar Message: Invalid order of arguments of redefined constructor Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 11 Mizar Message: Too many constants in an inference Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 110 Mizar Message: Only nullary prefixes allowed Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 1100 Mizar Message: Disk read error Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1101 Mizar Message: Disk write error Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1102 Mizar Message: File not assigned Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1103 Mizar Message: File not open Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1104 Mizar Message: File not open for input Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1105 Mizar Message: File not open for output Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1106 Mizar Message: Invalid numeric format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 111 Mizar Message: Non registered attribute cluster Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 112 Mizar Message: Unknown predicate Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 113 Mizar Message: Unknown functor Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 114 Mizar Message: Unknown mode Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 115 Mizar Message: Unknown attribute Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1150 Mizar Message: Disk is write protected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1151 Mizar Message: Bad drive request struct length Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 1152 Mizar Message: Drive not ready Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1154 Mizar Message: CRC error in data Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1156 Mizar Message: Disk seek error Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1157 Mizar Message: Unknown media type Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1158 Mizar Message: Sector Not Found Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1159 Mizar Message: Printer out of paper Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 116 Mizar Message: Invalid "qua" Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1160 Mizar Message: Device write fault Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1161 Mizar Message: Device read fault Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1162 Mizar Message: Hardware failure Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 117 Mizar Message: Invalid specification Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 118 Mizar Message: Invalid specification Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 119 Mizar Message: Illegal cluster Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 12 Mizar Message: Too long universal prefix Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 120 Mizar Message: Disagreement of argument types Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 1200 Mizar Message: Division by zero Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1201 Mizar Message: Range check error Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1202 Mizar Message: Stack overflow error Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1203 Mizar Message: Heap overflow error Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1204 Mizar Message: Invalid pointer operation Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1205 Mizar Message: Floating point overflow Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1206 Mizar Message: Floating point underflow Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1207 Mizar Message: Invalid floating point operation Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 1208 Mizar Message: Overlay manager not installed Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 1209 Mizar Message: Overlay file read error Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 121 Mizar Message: Disagreement of argument types Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 1210 Mizar Message: Object not initialized Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1211 Mizar Message: Call to abstract method Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1212 Mizar Message: Stream registration error Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1213 Mizar Message: Collection index out of range Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 1214 Mizar Message: Collection overflow error Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1215 Mizar Message: Arithmetic overflow error Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 1216 Mizar Message: General Protection fault Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 122 Mizar Message: Disagreement of argument types Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 123 Mizar Message: Disagreement of argument types Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 124 Mizar Message: Disagreement of argument types Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 125 Mizar Message: Argument of a selector must be a structure Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 1255 Mizar Message: Ctrl Break Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 126 Mizar Message: Unknown selector functor Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 127 Mizar Message: Argument must be an elementary type Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 128 Mizar Message: Arguments must be elementary types Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 129 Mizar Message: Invalid free variables in a Fraenkel operator Description Often happens if the types of variables ("LambdaVariables") parameterizing ...
Error Number: 13 Mizar Message: Too many complexes Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 130 Mizar Message: Redefinition of an attribute with predicate pattern is not allowed Description Please contribute Typical examples Please contribute ...
Error Number: 131 Mizar Message: No reserved type for a variable, free in the default type Description Please contribute Typical examples Please contribute Weird ...
Error Number: 132 Mizar Message: Invalid "exactly" Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 133 Mizar Message: Cannot cluster attribute with arguments Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 134 Mizar Message: Cannot redefine expandable mode Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 135 Mizar Message: Inaccessible selector Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 136 Mizar Message: Non registered cluster Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 137 Mizar Message: "requirements SUBSET;" missing Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 138 Mizar Message: Cannot identify a local constant, free in the default type Description The locus being declared depends upon a hidden variable which ...
Error Number: 14 Mizar Message: Too many terms in an inference Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 140 Mizar Message: Unknown variable Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 141 Mizar Message: Locus repeated Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 142 Mizar Message: Unknown locus Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 143 Mizar Message: No implicit qualification Description Please contribute Typical examples Please contribute Weird examples Can occur when a symbol ...
Error Number: 144 Mizar Message: Unknown label Description For MML references often means that you do not have the article in the TheoremDirective. Typical examples ...
Error Number: 145 Mizar Message: Inaccessible label Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 146 Mizar Message: Theorem number must be greater than 0 Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 147 Mizar Message: Unknown theorems file Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 148 Mizar Message: Unknown private functor Description This can be caused by referencing a function without importing the necessary vocabulary. Importing ...
Error Number: 149 Mizar Message: Unknown private predicate Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 15 Mizar Message: Too many equalities in an inference Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 150 Mizar Message: A variable free in default type has explicit qualification Description Please contribute Typical examples Please contribute Weird ...
Error Number: 151 Mizar Message: Unknown mode format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 152 Mizar Message: Unknown functor format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 153 Mizar Message: Unknown predicate format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 154 Mizar Message: Unknown field Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 155 Mizar Message: Unknown prefix Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 156 Mizar Message: Invalid equality format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 157 Mizar Message: Exactly one term is expected before "is" Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 158 Mizar Message: Two different formats for a structure symbol Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 159 Mizar Message: Invalid iterative equality Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 16 Mizar Message: Collection Overflow Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 160 Mizar Message: This variable still cannot be accessed Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 161 Mizar Message: Fixed variables cannot be postqualified Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 162 Mizar Message: A free variable identified with a new implicit qualification Description Please contribute Typical examples Please contribute ...
Error Number: 163 Mizar Message: Disagreement of reservations of a free variable Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 164 Mizar Message: Nothing to link Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 165 Mizar Message: Unknown functor format Description Seems that this most often means that you do not have the symbol in articles vocabularies. JosefUrban ...
Error Number: 166 Mizar Message: Unknown functor format Description Similar to error 165. A term with argument does not match a known notation a notation directive ...
Error Number: 167 Mizar Message: Unknown functor format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 168 Mizar Message: Unknown functor format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 169 Mizar Message: Unknown functor format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 170 Mizar Message: Unknown functor format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 171 Mizar Message: Unknown functor format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 172 Mizar Message: Unknown functor format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 173 Mizar Message: Unknown functor format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 174 Mizar Message: Unknown functor format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 175 Mizar Message: Unknown attribute format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 176 Mizar Message: Unknown structure format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 177 Mizar Message: Link assumes a straightforward justification Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 178 Mizar Message: Link assumes a straightforward justification Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 179 Mizar Message: It is not a locus Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 180 Mizar Message: Too many arguments Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 181 Mizar Message: Not so many arguments in this definition Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 182 Mizar Message: Unknown selector format Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 183 Mizar Message: Accessible mode format has empty list of arguments Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 184 Mizar Message: Accessible structure format has empty list of arguments Description Please contribute Typical examples Please contribute Weird ...
Error Number: 185 Mizar Message: Unknown structured mode format Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 190 Mizar Message: Inaccessible theorem Description The theorem used depends on a constructor which is not accessible. To fix, add the missing constructors ...
Error Number: 191 Mizar Message: Unknown scheme Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 192 Mizar Message: Inaccessible theorem Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 193 Mizar Message: Inaccessible scheme Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 194 Mizar Message: Wrong number of premises Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 195 Mizar Message: Scheme uses constructors which are not in your environment Description Please contribute Typical examples Please contribute Weird ...
Error Number: 196 Mizar Message: Unknown scheme Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 197 Mizar Message: Scheme definition repeated Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 198 Mizar Message: It is meaningless to define an antonym to a functor or a mode Description Please contribute Typical examples Please contribute ...
Error Number: 199 Mizar Message: Inaccessible definitional theorem Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 1994 Mizar Message: I/O stream error: Put of unregistered object type Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 1995 Mizar Message: I/O stream error: Get of unregistered object type Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 1996 Mizar Message: I/O stream error: Cannot expand stream Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 1997 Mizar Message: I/O stream error: Read beyond end of stream Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 1998 Mizar Message: I/O stream error: Cannot initialize stream Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 1999 Mizar Message: I/O stream error: Access error Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 20 Mizar Message: The structure of the sentences disagrees with the scheme Description a. A statement Q justified by a scheme does not match the ...
Error Number: 200 Mizar Message: Too long source line Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 201 Mizar Message: Only characters with decimal ASCII codes between 32 and 126 are allowed Description Please contribute Typical examples Please contribute ...
Error Number: 202 Mizar Message: Too large numeral Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 203 Mizar Message: Unknown token, maybe the forbidden underscore character used in an identifier Description This error is generated under two conditions ...
Error Number: 21 Mizar Message: The structure of sentences disagrees the scheme Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 210 Mizar Message: Wrong item in environment declaration Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 211 Mizar Message: Unexpected "environ" Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 212 Mizar Message: "environ" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 213 Mizar Message: "begin" missing Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 214 Mizar Message: "end" missing Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 215 Mizar Message: No pairing "end" for this word Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 216 Mizar Message: Unexpected "end" Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 217 Mizar Message: ";" missing Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 219 Mizar Message: Unexpected "proof" Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 22 Mizar Message: Impossible matching of a locus of a predicate Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 229 Mizar Message: "redefine" repeated Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 23 Mizar Message: Impossible reconstruction of the definiens of a predicate Description Please contribute Typical examples Please contribute Weird ...
Error Number: 230 Mizar Message: Only one "per cases" is allowed in a reasoning Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 231 Mizar Message: "per cases" missing Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 232 Mizar Message: "case" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 24 Mizar Message: Impossible matching of a locus of a functor Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 240 Mizar Message: Definition blocks must not be nested Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 241 Mizar Message: Directives are not allowed in the text proper Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 242 Mizar Message: "reserve", "struct", "scheme" and "theorem" not allowed in a definition block Description Please contribute Typical examples Please ...
Error Number: 25 Mizar Message: A variable bound in a substituted predicate occurs beyond the predicate Description Please contribute Typical examples Please contribute ...
Error Number: 250 Mizar Message: "$1",...,"$8" are allowed only inside definiens of a private constructor Description Please contribute Typical examples Please ...
Error Number: 251 Mizar Message: "it" is allowed only inside definiens of a public functor or mode Description Predicates and attributes may reference loci (parameter ...
Error Number: 253 Mizar Message: "means" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 255 Mizar Message: It is not allowed for expandable modes Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 26 Mizar Message: A variable bound in a substituted functor occurs beyond the functor Description Please contribute Typical examples Please contribute ...
Error Number: 27 Mizar Message: Cannot solve cluster ambiguities Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 271 Mizar Message: Redefined mode cannot be expandable Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 272 Mizar Message: It's meaningless to redefine cluster Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 274 Mizar Message: Don't use "means" in the definition of an expandable mode Description Please contribute Typical examples Please contribute Weird ...
Error Number: 28 Mizar Message: Cannot widen the type of the substituted term to the type of functor variable Description Please contribute Typical examples Please ...
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 ...
Error Number: 301 Mizar Message: Predicate symbol expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 302 Mizar Message: Functor symbol expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 303 Mizar Message: Mode symbol expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 304 Mizar Message: Structure symbol expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 305 Mizar Message: Selector symbol expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 306 Mizar Message: Attribute symbol expected Description The designated symbol is not declared as category V in the vocabulary: It may be missing ...
Error Number: 307 Mizar Message: Numeral expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 308 Mizar Message: Identifier or theorem file name expected Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 309 Mizar Message: Type or attribute expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 31 Mizar Message: Disagreement of correspondents of a constant Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 310 Mizar Message: Right functor bracket expected Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 311 Mizar Message: Paired functor brackets must be of the same kind Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 32 Mizar Message: Too many fillings of a functor Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 320 Mizar Message: Selector or structure symbol expected Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 321 Mizar Message: Predicate symbol or "is" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 329 Mizar Message: Selector without argument is allowed only inside a structure pattern Description Please contribute Typical examples Please contribute ...
Error Number: 33 Mizar Message: Too many fillings of a predicate Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 330 Mizar Message: Unexpected end of an item (perhaps ";" missing) Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 336 Mizar Message: Associative notation must not be used for "iff" and "implies" Description Mizar does not apply a default association rule to consecutive ...
Error Number: 340 Mizar Message: "holds", "for" or "ex" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 350 Mizar Message: "that" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 351 Mizar Message: "cases" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 360 Mizar Message: "(" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 361 Mizar Message: " " expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 362 Mizar Message: "{" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 363 Mizar Message: "(#" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 364 Mizar Message: "(" or " " expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 370 Mizar Message: ")" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 371 Mizar Message: " " expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 372 Mizar Message: "}" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 373 Mizar Message: "#)" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 380 Mizar Message: " " expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 381 Mizar Message: "if" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 382 Mizar Message: "for" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 383 Mizar Message: "is" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 384 Mizar Message: ":" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 385 Mizar Message: " " expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 386 Mizar Message: "means" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 387 Mizar Message: "st" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 388 Mizar Message: "as" expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 391 Mizar Message: Incorrect beginning of a text item Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 392 Mizar Message: Incorrect beginning of a definition item Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 393 Mizar Message: Incorrect beginning of a reasoning item Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 394 Mizar Message: Statement expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 395 Mizar Message: Justification expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 396 Mizar Message: Formula expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 397 Mizar Message: Term expected Description An off category or unknown symbol appears where a term is expected. Some possible causes include: ...
Error Number: 398 Mizar Message: Type expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 399 Mizar Message: Functor pattern expected Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 4 Mizar Message: This inference is not accepted Description The checker said "no" Typical examples Please contribute Weird examples I just spent ...
Error Number: 40 Mizar Message: Non unique matching of a locus of the substitute of a predicate variable Description Please contribute Typical examples Please contribute ...
Error Number: 400 Mizar Message: Still not implemented Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 41 Mizar Message: Non unique matching of a locus of the substitute of a functor variable Description Please contribute Typical examples Please contribute ...
Error Number: 42 Mizar Message: Non unique matching of a locus of the substitute of a functor variable Description Please contribute Typical examples Please contribute ...
Error Number: 43 Mizar Message: Cannot decompose a conjunction of formal sentences Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 44 Mizar Message: A formal predicate in a Fraenkel operator of formal construction Description Please contribute Typical examples Please contribute ...
Error Number: 45 Mizar Message: Wrong order of the declarations of scheme functor or nested functor Description Please contribute Typical examples Please contribute ...
Error Number: 450 Mizar Message: Too many variables Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 451 Mizar Message: Too many predicate formats Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 452 Mizar Message: Too many functor formats Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 453 Mizar Message: Too many mode formats Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 454 Mizar Message: Too large theorem number Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 455 Mizar Message: Too many labels in a definition block Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 456 Mizar Message: Too many references in an inference Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 458 Mizar Message: Too many private predicates Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 459 Mizar Message: Too many private functors Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 46 Mizar Message: Probably the incorporation of an argument Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 460 Mizar Message: Too many reserved identifiers Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 461 Mizar Message: Too many free variables Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 462 Mizar Message: Too many modes Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 465 Mizar Message: Too many predicates Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 466 Mizar Message: Too many functors Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 467 Mizar Message: Too many structures Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 468 Mizar Message: Too many selectors Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 469 Mizar Message: Too many loci Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 470 Mizar Message: Too complicated term Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 471 Mizar Message: Too many selectors in one structure definition Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 472 Mizar Message: Too many references Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 473 Mizar Message: Too many justifications Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 474 Mizar Message: Too complicated term Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 476 Mizar Message: Too many default signature files Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 477 Mizar Message: Too many predicate, mode or functor symbols Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 478 Mizar Message: Too many labels Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 479 Mizar Message: Too many loci in one definition block Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 480 Mizar Message: Too many default vocabulary files Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 481 Mizar Message: Too many functor symbols in default vocabulary files Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 482 Mizar Message: Too many free variable scopes Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 483 Mizar Message: Too many variables Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 484 Mizar Message: Too many reservations Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 485 Mizar Message: Too nested reasoning Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 486 Mizar Message: Too many functor formats Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 487 Mizar Message: Too many scheme identifiers Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 488 Mizar Message: Too many unreserved free variables Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 489 Mizar Message: Memory handling in unifier failed Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 490 Mizar Message: Too many free variables in reservations Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 491 Mizar Message: Too many structure formats Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 492 Mizar Message: Too many functor formats Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 493 Mizar Message: Too many parameters in one scheme Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 494 Mizar Message: Too complicated scheme (too many external variables) Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 495 Mizar Message: Too complicated scheme (too many occurrences of a functor variable) Description Please contribute Typical examples Please contribute ...
Error Number: 496 Mizar Message: Too complicated scheme (too many occurrences of a predicate variable) Description Please contribute Typical examples Please contribute ...
Error Number: 497 Mizar Message: Too many functor symbols Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 498 Mizar Message: Too many occurrences of arguments of a second order variable Description Please contribute Typical examples Please contribute ...
Error Number: 499 Mizar Message: Too many errors Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 50 Mizar Message: Nongeneralizable variable in the skeleton of a reasoning Description Please contribute Typical examples Please contribute Weird ...
Error Number: 500 Mizar Message: Obsolete signature directive Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 51 Mizar Message: Invalid conclusion Description Error 51 can result when proving an equivalence (i.e. bi implication, iff) in an unexpected way. Mizar ...
Error Number: 52 Mizar Message: Invalid assumption Description The assumed condition is not equivalent to the antecedent of the current thesis. Some causes include ...
Error Number: 53 Mizar Message: Invalid case Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 54 Mizar Message: The cases are not exhausted Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 55 Mizar Message: Invalid generalization Description A local constant being generalized by let or exemplified by take is deficient with respect ...
Error Number: 56 Mizar Message: Disagreement of types Description A local constant being generalized by let disagrees in type with the corresponding quantified ...
Error Number: 57 Mizar Message: The type of the instantiated term doesn't widen properly Description The instantiated term is not a sub type of the term's required ...
Error Number: 58 Mizar Message: Mixing "case" with "suppose" is not allowed in one "per cases" reasoning Description Please contribute Typical examples Please contribute ...
Error Number: 59 Mizar Message: The theses in each case should be equal formulae Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 60 Mizar Message: Something remains to be proved in this case Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 601 Mizar Message: Irrelevant label Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 602 Mizar Message: Irrelevant reference Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 603 Mizar Message: Irrelevant linking Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 604 Mizar Message: Irrelevant inference Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 605 Mizar Message: Irrelevant linked inference Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 607 Mizar Message: Justification can be straightforward Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 608 Mizar Message: Linkable statement Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 609 Mizar Message: Irrelevant "that" Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 610 Mizar Message: Beginning of an inaccessible item Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 611 Mizar Message: End of an inaccessible item Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 612 Mizar Message: Beginning of an inaccessible conditions Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 613 Mizar Message: End of an inaccessible conditions Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 614 Mizar Message: Duplicating label identifier Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 615 Mizar Message: Unexpected "
Error Number: 616 Mizar Message: "be" recommended Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 62 Mizar Message: Free variables not allowed in an iterative equality Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 63 Mizar Message: Unexpected proof Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 64 Mizar Message: Invalid exemplification in a diffuse statement Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 65 Mizar Message: "thesis" is allowed only inside a proof Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 68 Mizar Message: Nongeneralizable variable in the skeleton of a reasoning Description Please contribute Typical examples Please contribute Weird ...
Error Number: 69 Mizar Message: Nongeneralizable variable in a definiens Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 70 Mizar Message: Something remains to be proved Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 703 Mizar Message: Unnecessary "proof thus thesis; end;" Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 704 Mizar Message: Irrelevant signature directive Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 706 Mizar Message: Unnecessary theorems directive Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 707 Mizar Message: Unnecessary schemes directive Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 708 Mizar Message: Theorem should be replaced by an equal one Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 709 Mizar Message: Irrelevant vocabulary directive Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 710 Mizar Message: Irrelevant definitions directive Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 711 Mizar Message: Identity functor definition Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 712 Mizar Message: Synonym of a functor definition Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 713 Mizar Message: Irrelevant redefinition of a functor Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 714 Mizar Message: Irrelevant redefinition of a mode Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 715 Mizar Message: Irrelevant reconsider of a variable Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 716 Mizar Message: Irrelevant reconsider of a term Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 717 Mizar Message: Irrelevant reconsider Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 72 Mizar Message: Unexpected correctness condition Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 720 Mizar Message: The first two arguments of the iterative equality are equal Description Please contribute Typical examples Please contribute Weird ...
Error Number: 721 Mizar Message: The first argument of the iterative equality is equal with a next one Description Please contribute Typical examples Please contribute ...
Error Number: 722 Mizar Message: The second argument of the iterative equality is equal with a next one Description Please contribute Typical examples Please contribute ...
Error Number: 724 Mizar Message: This argument of the iterative equality is equal with a next one Description Please contribute Typical examples Please contribute ...
Error Number: 725 Mizar Message: The equal argument of the iterative equality with a previous one Description Please contribute Typical examples Please contribute ...
Error Number: 73 Mizar Message: Correctness condition missing Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 730 Mizar Message: The redundant reconsidering of variables Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 731 Mizar Message: The redundant reconsidering of terms Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 732 Mizar Message: The redundant reconsidering of a variable Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 733 Mizar Message: The redundant reconsidering of a term Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 734 Mizar Message: The redundant considering Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 735 Mizar Message: Irrelevant variable reservation Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 736 Mizar Message: Unused private functor Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 737 Mizar Message: Unused private predicate Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 746 Mizar Message: References can be moved to the next step of this iterative equality Description Please contribute Typical examples Please contribute ...
Error Number: 76 Mizar Message: Don't mix cluster correctness with other correctness conditions Description Please contribute Typical examples Please contribute ...
Error Number: 77 Mizar Message: Still not implemented Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 78 Mizar Message: The type of the argument must widen to the result type Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 79 Mizar Message: Types of arguments must be equal Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 80 Mizar Message: Cannot be used in a permissive definition Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 800 Mizar Message: Library corrupted Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 801 Mizar Message: Cannot find vocabulary file Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 802 Mizar Message: Cannot find formats file Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 803 Mizar Message: Cannot find notations file Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 804 Mizar Message: Cannot find signature file Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 805 Mizar Message: Cannot find definitions file Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 806 Mizar Message: Cannot find theorems file Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 807 Mizar Message: Cannot find schemes file Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 808 Mizar Message: Cannot find constructors file Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 809 Mizar Message: Cannot find clusters file Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 81 Mizar Message: It is meaningful for binary predicates only Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 810 Mizar Message: Directive name repeated Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 811 Mizar Message: Invalid priority of a functor symbol on a vocabulary file Description Please contribute Typical examples Please contribute Weird ...
Error Number: 812 Mizar Message: An empty line on a vocabulary file Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 813 Mizar Message: Invalid qualifier on a vocabulary file Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 814 Mizar Message: Invalid character or space in a symbol Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 815 Mizar Message: A vocabulary symbol repeated Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 816 Mizar Message: Invalid priority Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 817 Mizar Message: An empty symbol Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 82 Mizar Message: It is meaningful for binary functors only Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 821 Mizar Message: A scheme identifier repeated Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 825 Mizar Message: Cannot find constructors name on constructor list Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 83 Mizar Message: It is meaningful for unary functors only Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 830 Mizar Message: Nothing imported from notations Description A notation directive appears in the environment, but nothing is utilizing any of the ...
Error Number: 831 Mizar Message: Nothing imported from clusters Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 832 Mizar Message: Nothing imported from definitions Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 833 Mizar Message: Nothing imported from theorems Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 834 Mizar Message: Nothing imported from schemes Description A scheme, used to justify a statement, relies on undefined notation. A notations directive ...
Error Number: 84 Mizar Message: The result type is not invariant under swapping the arguments Description Please contribute Typical examples Please contribute ...
Error Number: 85 Mizar Message: The type of the argument must be equal to the result type Description Please contribute Typical examples Please contribute Weird ...
Error Number: 856 Mizar Message: Inaccessible requirements directive Description A requirements directive needs prerequisite information that is not being supplied ...
Error Number: 89 Mizar Message: As yet not implemented for redefined functors Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 891 Mizar Message: MML identifier should be written in capitals Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 892 Mizar Message: MML identifier should be at most eight characters long Description Please contribute Typical examples Please contribute Weird ...
Error Number: 9 Mizar Message: Too many instantiations Description Please contribute Typical examples environ vocabularies ZFMISC 1, PRE TOPC, EUCLID; constructors ...
Error Number: 91 Mizar Message: Homonimic fields in stucture declaration Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 911 Mizar Message: Too long term without parentheses Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 912 Mizar Message: Too long right nesting of a term Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 913 Mizar Message: Too many labels (simultaneously accessible) Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 914 Mizar Message: Too many references in an inference Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 915 Mizar Message: Too many ranges of free variables Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 916 Mizar Message: Too many reservations Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 917 Mizar Message: Too many free variables in reservations Description Please contribute Typical examples Please contribute Weird examples Please ...
Error Number: 918 Mizar Message: Too many variables (simultaneously accessible) Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 919 Mizar Message: Too many reserved identifiers Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 92 Mizar Message: Type of the field must be equal to the type in prefix Description Please contribute Typical examples Please contribute Weird examples ...
Error Number: 920 Mizar Message: Too many private functors Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 921 Mizar Message: Too many private predicates Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 923 Mizar Message: Too many different clusters Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 924 Mizar Message: Common number of loci exceeded Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 925 Mizar Message: Too many predicate patterns Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 926 Mizar Message: Too many functors Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 927 Mizar Message: Too many functor patterns Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 928 Mizar Message: Too many modes Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 929 Mizar Message: Too many mode patterns Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 93 Mizar Message: Missing field of a prefix Description While giving a definition to the structure one or more fields of the parent structure are omitted ...
Error Number: 930 Mizar Message: Too many attributes Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 931 Mizar Message: Too many attribute patterns Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 933 Mizar Message: Too many structures Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 935 Mizar Message: Too many selectors Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 936 Mizar Message: Too many registered clusters Description Please contribute Typical examples Please contribute Weird examples Please contribute ...
Error Number: 937 Mizar Message: Too many arguments Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 938 Mizar Message: Too many terms Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 94 Mizar Message: Prefix must be a structure Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 95 Mizar Message: Inconsistent cluster Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 950 Mizar Message: Too many schemes Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 951 Mizar Message: Too many imported files Description Please contribute Typical examples Please contribute Weird examples Please contribute
Error Number: 96 Mizar Message: Only standard functors and selectors can be used in a functor cluster Description Please contribute Typical examples Please contribute ...
Error Number: 97 Mizar Message: Non clusterable attribute Description Please contribute Typical examples Please contribute Weird examples Please contribute
Frequently Asked Questions About Online Proof Read to Formalized Mathematics What is it? GrzegorzBancerek 28 Dec 2005
Ideas and Brainstorming The place for brainstorming around Mizar and Mizar technology in general. NOTE: Start a new topic for each idea. New brainstorming ...
Despite the permissive defintion of the type Element http://mizar.uwb.edu.pl/JFM/Vol1/subset 1.abs.html#M1 the Frankel term still requires its arguments to widen into ...
FraenkelTerms, LambdaTerms in Mizar?, features wanted, their implementation JosefUrban 07 Jul 2002
FunctorResultClusters There seems to be some redundancy in clusters for f.x see FUNCT 1:func.1 funcreg Follow up
FunctorSynonyms The definition of dist(x,y) could be just a synonym. With appropriate clusters, the result type of (the distance of M).(x,y) is a real number already ...
Integrated semantic browsing of the Mizar Mathematical Library for authoring Mizar articles Motivation Exact browsing of the overloaded Mizar notation Presentation ...
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 ...
FAQ: Question: How to install Mizar system on PC with Windows XP and get the first example article? Answer: MichaelNedzelsky 13 Jul 2005 Step by ...
Journal Of Formalized Mathematics Bialystok: http://mizar.uwb.edu.pl/JFM/ JosefUrban 16 Jul 2002
MichaelNedzelsky 30 Oct 2006 The utility was removed from this page. You can get the code at MizarParser MichaelNedzelsky 09 Oct 2006 The following simple ...
03 XX: MATHEMATICAL LOGIC AND FOUNDATIONS 03Bxx: General logic 03B05: Classical propositional logic lukasi 1: Propositional Calculus by Grzegorz Bancerek, Agata ...
Suggestion: RLVECT into NAT 1 Move theorems about naturals from RLVECT 1 and RLVECT 2 to NAT 1 before NAT 1:18. Follow up RLVECT 1: RLVECT 1:th.98 RLVECT 1:th.99 ...
MPTP Challenge: Why, What, How, Results, What to do Next Current TPTP, CASC, ATP TPTP in 2003: mostly CNF problems ATPs working mostly in CNF, only a few ...
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 ...
Abstrakt start Abstrakt to streszvczenie artyku #322;u zawieraj #261;ce eportowalne elementy: twierdzenia, schematy, definicje, rejestracje i wprowadzenia notacji ...
start Artyku #322; Artyku #322; Mizarowy to tekst ASSCI zawieraj #261;cy dwie cz #281; #347;ci: #347;rodowisko i tekst w #322;a #347;ciwy.
Formu #322;a atomowa start S #261; 4 typy formu #322;y atomowej: Predykatywna formu #322;a atomowa Ogólna posta #263;: 1, ..., k k 1, ..., ...
Atrubut start definition let x1 be Theta;1; ..... let xn be Theta;n; attr xn is (a1,...,am) means Phi;(x1,...,xn); end; gdzie {a1,...,am} {x1,...,xn ...
Rozdzia #322; 1: Artyku #322; Podstawow #261; jednostk #261; biblioteki MML jest artyku #322;. .
start Rejestracja warunkowa registration let x1 be Theta;1; ..... let xn be Theta;n; cluster 1 ... k 1 ... m for Theta;(x1,...,xn); coherence ...
Konstruktor start Jest 7 rodzajów konstruktorów: Atrybut konstructor przymiotnika Funktor konstruktor termu Mode konstruktor type Predykat konstruktor formu #322 ...
Warunki poprawno #347;ci start warunek znaczenie definicja/rejestracja existence istnieje obiekt odpowieniego typu spe #322;niaj #261;cy definins lub spe ...
Podr #281;cznik Korelaty semantyczne Korelaty semantyczne s #261; postaciami normalnymi systemu redukcji z nast #281;puj #261;cymi regu #322;ami: wzorzec ...
Definicja start Definicja zaczyna si #281; od s #322;owa kluczowego definition , a ko #324;czy si #281; s #322;owem end . Definicja zawiera deklaracj #281; locus ...
Definicje do g #211;ry Definicje s #322;u #380; #261; wprowadzaniu nowych konstruktorów (orygina #322;y) wraz z w #322;a #347;ciwo #347;ciami i redefiniowanu orygina ...
#346;rodowosko start #346;rodowisko zawiera dyrektywy importu z bazy MML. vocabularies notations constructors requirement registrations ...
start Rejestracja egzystencjalna registration let x1 be Theta;1; ..... let xn be Theta;n; cluster 1 ... m for Theta;(x1,...,xn); existence proof ...
Formu #322;a start Formu #322;a jest zbudowana z formu #322; atomowych po #322; #261;czonych za pomoc #261; spójników logicznych: negacji not , koniunkcji , alternatywy ...
start Rejestracja funktorowa registration let x1 be Theta;1; ..... let xn be Theta;n; cluster (x1,...,xn) 1 ... m; coherence proof :: thesis ...
start Funktor definition let x1 be Theta;1; ..... let xn be Theta;n; func (a1,...,am) (am 1,...,ak) #920;(x1,...,xn) means #934;(x1,...,xn ...
start Rejestracja identyczno #347;ci registration let x1 be Theta;1; ..... let xn be Theta;n; identify (a1,...,ak) (ak 1,...,am) with (b1,...,bj) ...
start Cykl praxy z Mizarem Tekst artyku #322;u Mizarowego powstaje przy u #380;yciu edytora, np. emacsa. Co pewien czas wo #322;any jest weryfikator, który zaznacza ...
Funktor start definition let x1 be Theta;1; ..... let xn be Theta;n; mode of (a1,...,am) Theta;' means Phi;(x1,...,xn,it); end; definition let ...
start Notacja Notacja to wzorzec konstruktor.
Pragmaty start Pragmat ma posta #263; ::$X ....... gdzie X jest du #380; #261; liter #261;. ::$N nazwa elementu ::$EOF koniec pliku ::$P /::$P wy ...
Predykat start definition let x1 be Theta;1; ..... let xn be Theta;n; pred a1,...,am am 1,...,ak means Phi;(x1,...,xn,it); end; gdzie {a1,...,ak} ...
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 ...
W #322;asno #347;ci start definition definition let x1 be Theta;1; let x1 be Theta;1; ...... .... ...
start Rejestracja redukcji registration let x1 be Theta;1; ..... let xn be Theta;n; reduce '; reducibility proof thus '; end; end ...
Redefinicja start Redefinicja typu definition let x1 be Theta;1; ... let xn by Theta;n; redefine func (x1,...,xn) Theta;' of x1,...,xn; coherence ...
start Rejestracje Rejestracja egzystencjalna Rejestracja funktorowa Rejestracja identyczno #347;ci Rejestracja redukcji Rejestracja warunkowa ...
Schemat start Schemat to twierdzenie drugiego rz #281;du u #380;ywaj #261;ce zmiennych reprezentuj #261;xych formu #322;y i termy. Schemat zaczyna si #281; od s ...
Selector start Definicja struktury definition let x1 be Theta;1; ..... let xn be Theta;n; struct ( Sigma;1,..., Sigma;n) Sigma; over a1,...,am ( ...
start Rejestracja w #322;asno #347;ci sethood registration let x1 be Theta;1; ..... let xn be Theta;n; sethood of 1 ... m Theta;(x1,...,xn) proof ...
Przyk #322;ady formalizacji Liczby naturalne
Struktura start definition let x1 be Theta;1; ..... let xn be Theta;n; struct ( Sigma;1,..., Sigma;n) Sigma; over a1,...,am (# 1 Theta ...
Twierdzenie start Twierdzenie zawira s #322;owo kluczowe theorem , formu #322; #281; i uzasadnienie. Twierdzenie mo #380;e by #263; poprzedzone pragmatem z nazw ...
List of pages with Mathematics Subject Classification of Mizar articles NOTE: Start a new topic for each tool. New tool (use a .WikiWord title): ...
Mathematics Subject Classification 2010 Classified 559 articles of 1189 (MML Version 5.20), see MathSC2000 for listing of existing classification pages. See ListOfArticle ...
Suggestion: Meet for functions In FUNCT 6:def 4 to omit problems with identification change meet f Meet f In PROB 1:def 5 and PROB 3:def 9 Intersection should ...
Renaming lables, indentation suggestions, etc. JosefUrban 07 Jul 2002
is at http://mizar.uwb.edu.pl/system/#download JosefUrban 22 Feb 2003
Frequently Asked Questions About The Mizar Checker Submit a new FAQ Please ask questions in MizarQuestion. The FAQs are here for frequently asked questions ...
FAQ: Answer: Back to: MizarFAQ
MizarForum A mailing list devoted to discussions concerning Mizar. http://mizar.uwb.edu.pl/forum/ JosefUrban 24 Apr 2004
An Attempt to Find Consensus about Indenting Rules for Mizar Block Rules proof, now, hereby, suppose, case should increase indentation, end; should decrease it, ...
jEdit http://www.jedit.org is a mature and well designed programmer's text editor, written in pure Java. MichaelNedzelsky 31 Jul 2005
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 ...
Mizar Mode for Emacs the mizar mode for Emacs is now a part of the MizarDistribution the latest (and probably experimental) version can be downloaded from ...
MichaelNedzelsky 30 Oct 2006 Now the parser can build an incomplete parse tree (in which some nodes are non terminals) for given Mizar article. Type information is ...
Most common errors during Mizaring (add your negative experience, create new topics; check the ErrorMessages, FeatureBrainstorming and MizarQuestions topics) Some ...
Mizar Proof Advisor is a system providing hints for a proof of arbitrary Mizar formula, trained on MML proofs by data mining techniques. More detailed description ...
Ask a Mizar Question: Before you ask a question please check: MizarDocumentation MizarFAQ has frequently asked questions in general AnsweredQuestions ...
Mizar syntax AdamNaumowicz 2015 09 16 A number of updates to the grammar GrzegorzBancerek 2012 11 18 New syntax of postqualification; multipredicate format ...
How to attack a theory, typical solutions to typical problems CopyAndPaste: Pros and cons PrivateLibrary TypeCasting PrivateVsPublicTheorems ...
This page provides a dictionary of terms used in the Mizar community. GAB: Generated ABstract. See Query Homepage. JesseAlama 15 Jan 2007
abcmiz 0 GrzegorzBancerek 2013 11 26
Tools for better Mizaring and more NOTE: Start a new topic for each tool. New tool (use a .WikiWord title): JosefUrban 08 Jan 2005 ...
Mizar Translations this is now mostly a collection of e mails I (JosefUrban) exchanged with various people about translation of Mizar to various formats. People who ...
Mizar TWiki discussion, pros and cons, suggestions For general TWiki discussion, see WikiCulture, Wiki:WhyWikiWorks, TWiki:Main/TWikiPresentations Mizar specific ...
Mizar project wishlist (originally a note submitted to the 30 Years of Mizar MKM 2004 Affiliated Workshop http://merak.pb.bialystok.pl/mkm2004 ) My main wishes for ...
Some info on the Mizar XML implementation Kernel related stuff, more important Syntactic XML parts are described right in the Pascal files (mostly iocorrel ...
CVS of the MML Revisions http://alioth.uwb.edu.pl/cgi bin/viewcvs.cgi JosefUrban 16 Jul 2002
MML projects and descriptions MML description http://mizar.uwb.edu.pl/JFM/mmlident.html MML Projects CclFormalisation JordanTheorem FundamentalTheoremofAlgebra ...
MML Query MML Query is installed at http://mmlquery.mizar.org/mmlquery/three.html http://mmlquery.mizar.org/mmlquery/three.html http://megrez.mizar ...
MmlQuery, http://merak.pb.bialystok.pl/mmlquery/ Examples of queries, see also examples A constructor with the symbol symbol dom notation Registrations ...
KrzysztofRetel's instruction for local installation of MmlQuery I present one possible installation of MML Query engine locally. First you have to download (from ...
Grammar of MML Query Source: mmlquery.xml Date: Oct 7, 2003 (version) Version: 0.0 Initial term: Query sequenceContents General Queries Operations Ordering Abbreviations ...
Proposed changes to existing MML articles The place to suggest improvements and revisions to existing MML articles. NOTE: Start a new topic for each idea. ...
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 ...
MoMM Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics (originally a presentation for JosefUrban's talk at the IJCAR 2004 Workshop on ...
Mizar Problems for Theorem Proving (MpTP) see MpTP02 for second version of MpTP and MptpTodo for suggested improvements MpTP is collection of theorem proving ...
Mizar Problems for Theorem Proving 0.2 second version of the MpTP system (MpTP02) MpTP02 is downloadable at http://kti.ms.mff.cuni.cz/~urban/MPTP2/mptp0.2.tar ...
The MPTP2078 benchmark The MPTP2078 benchmark is a collection of 2078 ATP problems generated from MML by the MpTP02 system. The benchmark was created as follows: The ...
The MPTP $100 Challenges The MPTP $100 Challenges are sets of classical first order reasoning problems, expressed in the TpTP language, to be proved by fully automated ...
Questions and Answers for the MPTP Challenge Questions about the selected problems What is the difference betwen the first distribution and the current one? Fixing ...
List of plans and suggestions for future MpTP versions New functionality Learning support add arities to constr names.pl for easy printing into E KNOWLEDGE ...
Bug: Enter bug title here Enter description here Test case Environment Mizar version: MML version: OS: ...
Suggestion: Enter Suggestion title here Enter description here Article name: MML version: Follow up
Question . Mizar version: MML version: OS: Answer .
link Resources: ART miz xml xml1 BIB FMART bxb surface of ART and bibliogrphy FXM FXI kind.nr xml of (being) translated article items ...
Pretty Names for Mizar Constructors Set MML http://mmlquery.mizar.org/mml/4.48.930/ Here is the table of constructors for MML version 4.48.930 see . First ...
The order of articles in the NotationDirective is important. If two definitions of the same symbol from two different articles mentioned in notation are applicable ...
The following page contains all the definitions from first 10 MML articles in order of processing (see mml.lar file in Mizar distribution). It seems to be a good way ...
Suggestion: Partial unions, intersections, etc. See attached file. GrzegorzBancerek 04 Jan 2006 Article name: MML version: Follow ...
It seems that the current implementation does not allow a FunctorCluster for a RedefinedFunctor. This may be a serious problem, if a function is redefined immediately ...
Suggestion: Interface between Relations and Graphs It would be nice to have an easy transition between the notions and theorems written in MML for graphs and those ...
Tu powinny sie znalezc kryteria, ktorymi maja sie kierowac recenzenci przy recenzji artykulu do FM (i MML) GrzegorzBancerek 09 Dec 2005 0. W bibie obowiazkowe ...
Could any reviewer write down how the policy looks like? Lost potential (co)author
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 ...
Suggestion: Revising the proof of Gödel's Completeness Theorem I would like to propose some changes to GOEDELCP, which contains a proof of Gödel's completeness theorem ...
MMLQuery: http://mmlquery.mizar.org/mmlquery/three.html MML browsing: http://mmlquery.mizar.org/ Template maker: http://mmlquery.mizar.org/template maker ...
Suggestion: sigma Field of Subsets Two introductions of one concept, SigmaField from PROB 1 and sigma Field Subset from MEASURE1, should be unified. GrzegorzBancerek ...
You can execute this application from the command line: java cp mizutils.jar org.mizarutils.GUI The application take the value of MIZFILES environment variable to ...
Let's document the discussion about Mizar structures St. like "strict independence" (maybe property?) of some constructors would be quite useful; I am having the following ...
Most common errors during Mizaring This should become a structured version of MizarPitfalls. (add your negative experience at MizarPitfalls, create new topics; check ...
Suggestion: Casting theorem for integers I did not find st. like i0 is Nat iff ex n being Nat st n theorem :: INT 1:16 0 Article name: INT 1 ...
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 ...
Support questions have this status: MizarQuestion: Ask your questions here! AssignedQuestions: Under investigation. AnsweredQuestions: Answered ...
Tarski Grothendieck Set Theory (TG) Mizar article: MML IdtitleauthorsFMabstractsfull article tarski Tarski Grothendieck Set Theory Andrzej Trybulec FM abstracts: jfm ...
Question How do you do? . Mizar version: MML version: OS: WikiRoot 05 Jul 2002 Answer . Well well
Bug: TestBugNoTwo Enter description here BuggygBuggy Test case None Environment TWiki version: TWiki plugins: Server OS: ...
TestFeature WikiRoot 04 Jul 2002
FAQ: testquestion Answer: testanswer Back to: MizarFAQ WikiRoot 05 Jul 2002
Is this a question? WikiRoot 05 Jul 2002
Andrzej Trybulec suggests that JGRAPH 1:65, named "Fashoda meet theorem" by the author (Y. Nakamura), is a special case of a corollary from the Poincare Miranda theorem ...
Suggestion: TopRealAsSynonym Replace EUCLID:def.8 with a synonym TOP REAL n for nop TopSpaceMetr (Euclid n) the strictness is then automatic, the nop TopSpace ...
Topic Classification Each topic in the TWiki.Mizar has a classification. Set it using the WebForm when you edit a topic. Click on a classification below to generate ...
TPTP Thousands of Problems for Theorem Provers The TPTP Problem Library for Automated Theorem Proving by Geoff Sutcliffe (http://www.tptp.org) and its syntax (http ...
Mechanisms identifying, implying or interpreting theorems between intuitively "similar" notions should be discussed in general. As of the current Mizar, I would include ...
Form Definition for the Mizar web Name: Type: Size: Values: Tooltip message: TopicClassification select 1 Select one..., AnsweredQuestions ...
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 ...
See also the faster WebTopicList
Web Web Home Changes Index Search Webs
nop 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 have to ...
TWiki.Mizar Web Preferences The following settings are web preferences of the TWiki.Mizar web. These preferences overwrite the site level preferences in . ...
Statistics for TWiki.Mizar Web Month: Topic views: Topic saves: File uploads: Most popular topic views: Top contributors for topic save ...
See also the verbose WebIndex.
Articles that are being worked on: Author(s) Article Title Start Date Percent Complete Main.MarcoRiccardi MFOLD 3 Product of Manifolds. Tori. 2011 ...
XML for Mizar and MML See http://ktiml.mff.cuni.cz/~urban/mizxml.ps for description of Mizar XML ization. See MizarXmlImplementation for implementation notes. JosefUrban ...
Number of topics: 786

See also the faster WebTopicList

Topic revision: r2 - 2001-11-24 - 11:41:09 - PeterThoeny?
 
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback