Miz-m

Table of Contents

1 A Summary of Mizar

2 An Outline of the Mizar Language

3 The Structure of the Mizar Article

3. 1 The Structure of the Mizar

3. 2 Environment Section

3. 2. 1 Vocabulary Section

3. 2. 2 Signature Section

3. 2. 3 Definitions Section

3. 2. 4 Theorems Section

3. 2. 5 Schemes Section

3. 3 The Main Section

3. 3. 1 Sentences

3. 3. 2 Theorem

4 Method for Demonstration

4. 1 Basic Method for Demonstration

4. 2 Irrational Method

4. 3 Dividing the Demonstrations

4. 4 Demonstration of the Equivalence

4. 5 Method for Using Now

4. 5. 1 Caution About End

4. 6 All Symbols

4. 6. 1 When There Are Two Variables

4. 6. 2 Method for Writing With such that

4. 6. 3 Division of Sentences

4. 6. 4 Dividing Sentences With Assume

4. 6. 5 Caution Following that

4. 7 Existing Symbols

4. 7. 1 Method for Using Consider

4. 7. 2 Method for Using Given

4. 8 Dividing Into Cases

4. 8. 1 Premise for Dividing Into Cases

4. 8. 2 Labels for Dividing Into Labels

4. 8. 3 Warning About Labels

4. 9 Method for Using @proof

5 About Mode

5. 2 Structure Level

5. 3 Mode Extension

5. 4 Declaration of Mode During a Demonstration

5. 4. 1 Warning About c=

5. 4. 2 Example of Actually Using a Definition

6 Definition

6. 1 Definition

6. 2 Method for Writing the Vocabulary File

6. 3 Predicate Definitio

6. 4 Functor Definition

6. 5 Mode Definition

7 Practice Environment

7. 1 Installation

7. 2 Preparation for Using Mizar

7. 3 Mizar System

7. 4 The Mizar Usage

7. 4. 1 Accommodate

7. 4. 2 Mizar Checker

7. 4. 3 When There Is An Error

7. 4. 4 Useful Command

7. 4. 5 To Call Mizar From the Editorエ

8 Registering to the Library

8. 1 Improvement of an Article

8. 1. 1 Improvement of the Main Section

8. 1. 2 Checking the Enviromnent Section

8. 2 Preparation for Registration

A. List of Reserved Words

A 1. Mizar Checker (including the accomodation data)

A 2. Only the Accomodation Data

B. A Compilation of Mizar Library Theorems

TABLE of ASCII Code

TABLE of ASCII Code(2)

Appendix D

D 1. Contacting the Mizar Society

D. 1. 1 Mizar Society

D. 1. 2 Mizar Society Nagano Circle

D 2. Acquisition of Mizar by ftp

D 3. WWW Homepage

D 4. Formalized Mathematics

Conclusion/Reference

Mizar Lecture Notes