Bibliography

1

Grzegorz Bancerek.
Tarski's classes and ranks.
Formalized Mathematics, 1(3):563-567, 1990.
MML: CLASSES1.

2

Grzegorz Bancerek.
König's theorem.
Formalized Mathematics, 1(3):589-593, 1990.
MML: CARD_3.

3

Grzegorz Bancerek.
Cartesian product of functions.
Formalized Mathematics, 2(4):547-552, 1991.
MML: FUNCT_6.

4

Grzegorz Bancerek.
Complete lattices.
Formalized Mathematics, 2(5):719-725, 1991.
MML: LATTICE3.

5

Grzegorz Bancerek.
Bounds in posets and relational substructures.
Formalized Mathematics, 6(1):81-91, 1997.
MML: YELLOW_0.

6

Grzegorz Bancerek.
Directed sets, nets, ideals, filters, and maps.
Formalized Mathematics, 6(1):93-107, 1997.
MML: WAYBEL_0.

7

Grzegorz Bancerek.
The ``way-below'' relation.
Formalized Mathematics, 6(1):169-176, 1997.
MML: WAYBEL_3.

8

Grzegorz Bancerek.
Duality in relation structures.
Formalized Mathematics, 6(2):227-232, 1997.
MML: YELLOW_7.

9

Grzegorz Bancerek.
Prime ideals and filters.
Formalized Mathematics, 6(2):241-247, 1997.
MML: WAYBEL_7.

10

Grzegorz Bancerek.
Arithmetic of Non Negative Rational Numbers.
Journal of Formalized Mathematics, Addenda.
MML: ARYTM_3.

11

Grzegorz Bancerek.
Bases and refinements of topologies.
Formalized Mathematics, 7(1):35-43, 1998.
MML: YELLOW_9.

12

Grzegorz Bancerek.
The Lawson Topology.
Formalized Mathematics, 7(2):163-168, 1998.
MML: WAYBEL19.

13

Grzegorz Bancerek.
Lawson topology in continuous lattices.
Formalized Mathematics, 7(2):177-184, 1998.
MML: WAYBEL21.

14

Grzegorz Bancerek.
Development of the theory of continuous lattices in MIZAR.
Symbolic Computation and Automated Reasoning, M. Kerber and M. Kohlhase, Eds., A K Peters, 2001.

15

Grzegorz Bancerek.
Continuous lattices of maps between T$_0$ spaces.
Formalized Mathematics, 9(1):111-117, 2001.
MML: WAYBEL26.

16

Józef Biaas.
Group and field definitions.
Formalized Mathematics, 1(3):433-439, 1990.
MML: REALSET1.

17

Ewa Bonarska.
An Introduction to PC Mizar.
Fondation Philippe le Hodey, Brussels, 1990.
Revised version, 2000.
http://mizar.org/project/bibliography.html.

18

Czesaw Bylinski.
Some basic properties of sets.
Formalized Mathematics, 1(1):47-53, 1990.
MML: ZFMISC_1.

19

Czesaw Bylinski.
Introduction to categories and functors.
Formalized Mathematics, 1(2):409-420, 1990.
MML: CAT_1.

20

Czesaw Bylinski.
Category Ens.
Formalized Mathematics, 2(4):527-533, 1991.
MML: ENS_1.

21

Czesaw Bylinski and Piotr Rudnicki.
The Scott topology. Part II.
Formalized Mathematics, 6(3):441-446, 1997.
MML: WAYBEL14.

22

M. Davis.
Obvious logical inferences.
In Proceedings of the 7th IJCAI, pages 530-531, 1981.

23

A. Degtyarev, A. Lyaletski, and M. Morokhovets.
Evidence algorithm and sequent logical inference search.
In LNAI 1705, pages 44-61, 1999.

24

H. Friedman.
FOM: 107: Automated proof checking, May 2001.

www.math.psu.edu/simpson/fom/postings.

25

G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. W. Mislove, and D. S. Scott.
A Compendium of Continuous Lattices.
Springer-Verlag, Berlin Heidelberg New York, 1980.

26

Adam Grabowski and Robert Milewski.
Boolean posets, posets under inclusion and products of relational structures.
Formalized Mathematics, 6(1):117-121, 1997.
MML: YELLOW_1.

27

Jarosaw Gryko.
Injective spaces.
Formalized Mathematics, 7(1):57-62, 1998.
MML: WAYBEL18.

28

Andrzej Grzegorczyk.
Zarys arytmetyki teoretycznej.
Biblioteka Matematyczna. PWN, Warszawa, 1971.

29

Stanisaw Jaskowski.
On the Rules of Supposition in Formal Logic.
Studia Logica. Warsaw University, 1934.
Reprinted in S. McCall, Polish Logic in 1920-1939, Clarendon Press, Oxford.

30

Peter T. Johnstone.
Stone Spaces.
Cambridge University Press, Cambridge, London, New York, 1982.

31

L. S. van Benthem Jutting.
Checking Landau's ``Grundlagen'' in the Automath system.
THE Eindhoven, PhD thesis, 1977.

32

John L. Kelley.
General Topology.
van Nostrand, New York, 1955.

33

Artur Korniowicz.
Cartesian products of relations and relational structures.
Formalized Mathematics, 6(1):145-152, 1997.
MML: YELLOW_3.

34

Artur Korniowicz.
On the topological properties of meet-continuous lattices.
Formalized Mathematics, 6(2):269-277, 1997.
MML: WAYBEL_9.

35

E. G. H. Landau.
Grundlagen der Analysis.
Akademische Verlag, Leipzig, 1930.

36

Library Committee of the Association of Mizar Users.
Preliminaries to Structures.
Journal of Formalized Mathematics, Addenda.
MML: STRUCT_0.

37

Library Committee of the Association of Mizar Users.
Preliminaries to Arithmetic.
Journal of Formalized Mathematics, Addenda.
MML: ARYTM.

38

Beata Madras.
Product of family of universal algebras.
Formalized Mathematics, 4(1):103-108, 1993.
MML: PRALG_1.

39

Robert Milewski.
Algebraic lattices.
Formalized Mathematics, 6(2):249-254, 1997.
MML: WAYBEL_8.

40

R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer.
Selected papers on Automath.
North-Holland, Amsterdam, 1994.

41

Beata Padlewska and Agata Darmochwa.
Topological Spaces and Continuous Functions.
Formalized Mathematics, 1(1):223-230, 1990.
MML: PRE_TOPC.

42

H. Rasiowa and R. Sikorski
The Mathematics of Metamathematics
PWN, Warszawa, 1968.

43

P. Rudnicki.
Obvious inferences.
Journal of Automated Reasoning, 3:383-393, 1987.

44

Piotr Rudnicki.
Kernel projections and quotient lattices.
Formalized Mathematics, 7(2):169-175, 1998.
MML: WAYBEL20.

45

P. Rudnicki, Ch. Schwarzweller and A. Trybulec.
Commutative Algebra in the Mizar System.
Journal of Symbolic Computation, 32:143-169, 2001.

46

Piotr Rudnicki and Andrzej Trybulec.
On equivalents of well-foundedness.
Journal of Automated Reasoning, 23(3-4):197-234, 1999.

47

Alexander Yu. Shibakov and Andrzej Trybulec.
The Cantor set.
Formalized Mathematics, 5(2):233-236, 1996.
MML: CANTOR_1.

48

Andrzej Trybulec.
Tarski Grothendieck set theory.
Formalized Mathematics, 1(1):9-11, 1990.
MML: TARSKI.

49

Andrzej Trybulec.
Built-in concepts.
Formalized Mathematics, 1(1):13-15, 1990.
MML: AXIOMS.

50

Andrzej Trybulec.
Categories without uniqueness of cod and dom.
Formalized Mathematics, 5(2):259-267, 1996.
MML: ALTCAT_1.

51

Andrzej Trybulec.
Functors for alternative categories.
Formalized Mathematics, 5(4):595-608, 1996.
MML: FUNCTOR0.

52

Andrzej Trybulec.
Moore-Smith convergence.
Formalized Mathematics, 6(2):213-225, 1997.

53

Andrzej Trybulec.
Scott topology.
Formalized Mathematics, 6(2):311-319, 1997.
MML: WAYBEL11.

54

Andrzej Trybulec.
Non Negative Real Numbers, Part I.
Journal of Formalized Mathematics, Addenda.
MML: ARYTM_2.

55

Andrzej Trybulec.
Non Negative Real Numbers, Part II.
Journal of Formalized Mathematics, Addenda.
MML: ARYTM_1.

56

Wojciech A. Trybulec.
Partially ordered sets.
Formalized Mathematics, 1(2):313-319, 1990.
MML: ORDERS_1.

57

Zinaida Trybulec and Halina Swieczkowska.
Boolean properties of sets.
Formalized Mathematics, 1(1):17-23, 1990.
MML: BOOLE.

58

Freek Wiedijk.
Mizar: An Impression. http://www.cs.kun.nl/~freek/notes.

59

Freek Wiedijk.
Estimating the Cost of a Standard Library for a Mathematical Proof Checker. http://www.cs.kun.nl/~freek/notes.

60

Freek Wiedijk.
The de Bruijn factor. http://www.cs.kun.nl/~freek/notes.

61

Edmund Woronowicz.
Relations defined on sets.
Formalized Mathematics, 1(1):181-186, 1990.
MML: RELSET_1.

62

Edmund Woronowicz and Anna Zalewska.
Properties of Binary Relations.
Formalized Mathematics, 1(1):85-89, 1990.
MML: RELAT_2.

63

Stanisaw Zukowski.
Introduction to lattice theory.
Formalized Mathematics, 1(1):215-222, 1990.
MML: LATTICES.