Grzegorz Bancerek, Publications

• Grzegorz Bancerek. On the structure of Mizar types. Electronic Notes in Theoretical Computer Science, Vol. 85 (7), Elsevier, 2003.
• Grzegorz Bancerek, Piotr Rudnicki. Information retrieval in MML. In A. Asperti, B. Buchberger, J.H. Davenport, editors, Mathematical Knowledge Management, LNCS 2594: 119-132, Springer, 2003.
• Grzegorz Bancerek, Piotr Rudnicki. A Compendium of Continuous Lattices in Mizar. (Formalizing recent mathematics), Journal of Automated Reasoning, Vol. 29 (3-4): 189-224, Kluwer, 2002.
• Grzegorz Bancerek, Noboru Endou, Yasunari Shidama. Lim-inf convergence and its compactness. Mechanized Mathematics and Its Applications, Vol. 2(1): 29-35, MIZAR Japan, 2002.
• Grzegorz Bancerek. Development of the Theory of Continuous Lattices in Mizar. In M. Kerber and M. Kohlhase, editors, Symbolic Computation and Automated Reasoning, pages 65-80, The CALCULEMUS-2000 Symposium, A.K.Peters, 2001.

Journal of Formalized Mathematics

• Volume 1, 1989
  1. The Fundamental Properties of Natural Numbers, FM 1(1):41-46, 1990.
  2. The Ordinal Numbers, FM 1(1):91-96, 1990.
  3. Segments of Natural Numbers and Finite Sequences, FM 1(1):107-114, 1990, with Krzysztof Hryniewiecki.
  4. The Well Ordering Relations, FM 1(1):123-129, 1990.
  5. A Model of ZF Set Theory Language, FM 1(1):131-145, 1990.
  6. Models and Satisfiability. Defining by Structural Induction and Free Variables in ZF-formulae, FM 1(1):191-199, 1990.
  7. The Contraction Lemma, FM 1(1):201-203, 1990.
  8. Zermelo Theorem and Axiom of Choice, FM 1(2):265-267, 1990.
  9. Properties of ZF Models, FM 1(2):277-280, 1990.
  10. Sequences of Ordinal Numbers, FM 1(2):281-290, 1990.
  11. Cardinal Numbers, FM 1(2):377-382, 1990.
  12. Kuratowski - Zorn Lemma, FM 1(2):387-393, 1990, with Wojciech A. Trybulec.
  13. Introduction to Trees, FM 1(2):421-427, 1990.
  14. Connectives and Subformulae of the First Order Language, FM 1(3):451-458, 1990.
  15. Variables in Formulae of the First Order Language, FM 1(3):459-469, 1990, with Czeslaw Bylinski.
• Volume 2, 1990
  16. Ordinal Arithmetics, FM 1(3):515-519, 1990.
  17. Curried and Uncurried Functions, FM 1(3):537-541, 1990.
  18. Cardinal Arithmetics, FM 1(3):543-547, 1990.
  19. Tarski's Classes and Ranks, FM 1(3):563-567, 1990.
  20. König's Theorem, FM 1(3):589-593, 1990.
  21. Universal Classes, FM 1(3):595-600, 1990, with Bogdan Nowak.
  22. Increasing and Continuous Ordinal Sequences, FM 1(4):711-714, 1990.
  23. Filters - Part I. Implicative Lattices, FM 1(5):813-819, 1990.
  24. Replacing of Variables in Formulas of ZF Theory, FM 1(5):963-972, 1990.
  25. The Reflection Theorem, FM 1(5):973-977, 1990.
  26. Consequences of the Reflection Theorem, FM 1(5):989-993, 1990.
  27. Countable Sets and Hessenberg's Theorem, FM 2(1):65-69, 1991.
  28. Definable Functions, FM 2(1):143-145, 1991.
  29. Propositional Calculus, FM 2(1):147-150, 1991, with Agata Darmochwal and Andrzej Trybulec.
• Volume 3, 1991
  30. König's Lemma, FM 2(3):397-402, 1991.
  31. Mostowski's Fundamental Operations - Part II, FM 2(3):425-427, 1991, with Andrzej Kondracki.
  32. Filters - Part II. Quotient Lattices Modulo Filters and Direct Product of Two Lattices, FM 2(3):433-438, 1991.
  33. Cartesian Product of Functions, FM 2(4):547-552, 1991.
• Volume 4, 1992
  34. Comma Category, FM 2(5):679-681, 1991, with Agata Darmochwal.
  35. Context-Free Grammar - Part I, FM 2(5):683-687, 1991, with Patricia L. Carlson.
  36. Complete Lattices, FM 2(5):719-725, 1991.
  37. On Powers of Cardinals, FM 3(1):89-93, 1992.
  38. Sets and Functions of Trees and Joining Operations of Trees, FM 3(2):195-204, 1992.
  39. Monoids, FM 3(2):213-225, 1992.
  40. Monoid of Multisets and Subsets, FM 3(2):227-233, 1992.
  41. Product of Families of Groups and Vector Spaces, FM 3(2):235-240, 1992, with Anna Lango.
• Volume 5, 1993
  42. Development of Terminology for SCM, FM 4(1):61-67, 1993, with Piotr Rudnicki.
  43. Two Programs for \bf SCM. Part I - Preliminaries, FM 4(1):69-72, 1993, with Piotr Rudnicki.
  44. Two Programs for \bf SCM. Part II - Programs, FM 4(1):73-75, 1993, with Piotr Rudnicki.
  45. Joining of Decorated Trees, FM 4(1):77-82, 1993.
  46. On Defining Functions on Trees, FM 4(1):91-101, 1993, with Piotr Rudnicki.
  47. On Defining Functions on Binary Trees, FM 5(1):9-13, 1996, with Piotr Rudnicki.
  48. A Compiler of Arithmetic Expressions for SCM, FM 5(1):15-20, 1996, with Piotr Rudnicki.
• Volume 6, 1994
  49. Quantales, FM 5(1):85-91, 1996.
  50. Ideals, FM 5(2):149-156, 1996.
  51. Categorial Categories and Slice Categories, FM 5(2):157-165, 1996.
  52. Subtrees, FM 5(2):185-190, 1996.
  53. Terms over many sorted universal algebra, FM 5(2):191-198, 1996.
• Volume 7, 1995
  54. Combining of Circuits, FM 5(2):283-295, 1996, with Yatsuka Nakamura.
  55. Indexed Category, FM 5(3):329-337, 1996.
  56. Full Adder Circuit. Part I, FM 5(3):367-380, 1996, with Yatsuka Nakamura.
  57. Continuous, Stable, and Linear Maps of Coherence Spaces, FM 5(3):381-393, 1996.
  58. Minimal Manysorted Signature for Partial Algebra, FM 5(3):405-414, 1996.
  59. Reduction Relations, FM 5(4):469-478, 1996.
• Volume 8, 1996
  60. Miscellaneous Facts about Functions, FM 5(4):485-492, 1996, with Andrzej Trybulec.
  61. Translations and Endomorphisms in Many Sorted Algebras, FM 5(4):553-564, 1996.
  62. Bounds in Posets and Relational Substructures, FM 6(1):81-91, 1997.
  63. Directed Sets, Nets, Ideals, Filters, and Maps, FM 6(1):93-107, 1997.
  64. The "Way-Below" Relation, FM 6(1):169-176, 1997.
  65. Duality in Relation Structures, FM 6(2):227-232, 1997.
  66. Prime Ideals and Filters, FM 6(2):241-247, 1997.
  67. Institution of Many-sorted Algebras, Part I : Signature Reduct of an Algebra, FM 6(2):279-287, 1997.
• Volume 9, 1997
  68. Closure Operators and Subalgebras, FM 6(2):295-301, 1997.
  69. Algebra of Morphisms, FM 6(2):303-310, 1997.
• Volume 10, 1998
  70. Bases and Refinements of Topologies, FM 7(1):35-43, 1998.
  71. The Lawson Topology, FM 7(2):163-168, 1998.
  72. Lawson Topology and Continuous Lattices, FM 7(2):177-184, 1998.
• Addenda
  73. Arithmetic of Positive Rational Numbers,
• Volume 11, 1999
  74. Retracts and Inheritance,
  75. Techincal Preliminaries to Algebraic Specifications,
  76. Continuous Lattices of Maps between T₀ Spaces,
  77. Function Spaces in the Category of Directed Suprema Preserving Maps, with Adam Naumowicz.
• Volume 12, 2000
  78. The Characterization of the Continuity of Topologies, with Adam Naumowicz.
• Volume 13, 2001
  79. Concrete Categories,
  80. Circuit Generated by Terms and Circuit Calculating Terms,
  81. The set of primitive recursive functions, with Piotr Rudnicki.
  82. On Characterizations of Compactness, with Noboru Endou and Yuji Sakai.
  83. Compactness of Lim-inf Topologie, with Noboru Endou.
  84. Miscellaneous facts about functors,
  85. Categorial Background for Duality Theory,
  86. Duality based on Galois connection. Part I,
  87. Yet another construction of free algebra, with Artur Kornilowicz.
  88. Zero-based finite sequences, with Tetsuya Tsunetou and Yatsuka Nakamura.
  89. On state machines of calculating type, with Hisayoshi Kunimune and Yatsuka Nakamura.
• Volume 14, 2002
  90. Combining of multi cell circuits, FM 10(1): 47-64, 2002, with Shin'nosuke Yamaguchi and Yasunari Shidama
  91. Full adder circuit. Part II, FM 10(1): 65-71, 2002, with Shin'nosuke Yamaguchi and Katsumi Wasaki
  92. Preliminaries to automatic generation of Mizar documentation for circuits, FM 10(3): 117-133, 2002, with Adam Naumowicz
  93. Processes in Petri nets, FM 11(1): 125-132, 2003, with Mitsuru Aoki, Akio Matsumoto, and Yasunari Shidama
• Volume 15, 2003
  94. Full subtracter circuit. Part II, FM 11(3): ??-??, 2003, with Shin'nosuke Yamaguchi and Katsumi Wasaki
  95. On semilattice structure of Mizar types, FM 11(4): 355?-369?, 2003.
  96. Lattice of fuzzy sets, FM 11(4): 393?-398?, 2003, with Takashi Mitsuishi
  97. Transitive closure of fuzzy relations, with Takashi Mitsuishi

• Verification of Circuit Designs with the Aid of the Mizar System. Position paper on Verification workshop of International Joint Conference on Automated Reasoning, Siena, 2001. (coauthors Yasushi Fuwa, Pauline N. Kawamoto, and Katsumi Wasaki)
• Codifying mathematics. Case study: the theory of continuous lattices. In Volume of Abstracts, 11-th International Congress of Logic, Methodology and Philosophy of Science, Cracow, August 20-26, 1999.
• Mizar - a work environment for a mathematician: an experiment with continuous lattices. In Abstracts of Short Communications and Poster Sessions, International Congress of Mathematicians, Berlin, August 18-27, 1998.
• The mutilated chessboard problem. In R. Matuszewski, editor, The QED Workshop II, Technical Report No. L/1/95, pages 37-38, Warsaw University, Bialystok Branch, 1995.
• Semi automated translation for mathematics. In J. Darski and Z. Vetulani, editors, Sprache-Kommunikation-Informatik, pages 131-136, Akten des 26. Linguistischen Kolloquiums, Niemeyer, Poznan, 1991. (coauthor Patricia Carlson)