Curriculum Vitae

Department of Information Engineering
Faculty of Engineering
Shinshu University
380-8553 Japan
Nagano-ken, Nagano-city
Wakasato 4-17-1

Institute of Computer Science
Faculty of Mathematics and Physics
University of Bialystok

ul. Akademicka 2
15-267 Bialystok, Poland

Education:

• Master degree: Warsaw University, Bialystok Campus (1990)
• Doctorate: Polish Academy of Sciences, Institute of Mathematics (1997)

• 2000-2002 JSPS Postdoctoral Fellow
  Department of Information Engineering
  Faculty of Engineering
  Shinshu University
  Nagano, Japan
• 1999-2001 Associate Professor
  Institute of Computer Science
  University of Bialystok
• 1998-1999 Associate Professor
  Institute of Mathematics
  University of Bialystok
• 1996-1997 Assistant Professor
  Institute of Mathematics
  Warsaw University, Bialystok Branch
• 1992-1996, Ph.D. student
  Institute of Mathematics
  Polish Academy of Sciences
• 1991-1992 Assistant Professor
  Institute of Mathematics
  Polish Academy of Sciences
• 1990-1991 Assistant Professor
  Institute of Mathematics
  Warsaw University, Bialystok Branch

1. main field - algebraic and categorial aspects of logic
2. other fields - continuous lattices, computation theory
3. current research interest - computer aided formalization of mathematics

1. Mizar formalization the theory of continuous lattices

Formalization in Mizar language the theory of continuous lattices according to the book A Compendium of Continuous Lattices by G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. Springer-Verlag, Berlin, Heidelberg, New York, 1980.

Subproject of project 3. started in 1996 and is still continued.

57 Mizar articles written by 15 authors from Poland, Canada, and Japan.

Supported by ONR Grant N00014-95-1-1336, ONR Grant N00014-97-1-0777, NATO Grant CRG 951368, and KBN Grant 8 T11C 018 12.

My contribution: project leader, 19 Mizar articles (including 4 coauthored).

2. Journal of Formalized Mathematics

Automatic text translation/generation from Mizar language into Math English in TeX and HTML form. Resulted programs are used to typeset the journal Formalized Mathematics (ISSN 1426-2630) and its electronic version (URL: http://www.mizar.org/JFM/).

Project started in 1990 and is still developed.

Supported by ONR Grant N00014-95-1-1336 and ONR Grant N00014-97-1-0777.

My contribution: software designer and developer.

3. Mizar Mathematical Library (MML)

MML is a collection of Mizar articles consequently developing mathematical knowledge from Tarski-Grothendieck set theory axioms.

Project started in 1989 and is still developed.

702 articles written by more than 120 authors from 9 countries.

My contribution: 87 articles (including 24 coauthored).

4. Mizar encyclopaedia

Interactive web pages (URL: http://megrez.mizar.org/services/ency/) to browse, search, and analyse the MML. Devoted to aid/support writing Mizar articles.

Project started in 2000.

My contribution: my individual project.

5. Mizar lectures on the Internet

Computer instructions by interactive web pages (URL: http://megrez.mizar.org/classes/) to learn Mizar language, system, and the MML. Designed as a part of Shinshu University, Graduate School of Science and Technology on the Internet.

Project started in 2001.

Project is in a state of designing.

My contribution: my individual project.

• Mizar - 87 articles, teaching,
• Pascal: turbo, Borland, object (Delphi, Kylix) - Mizar utilities: Abstractor, Bibart, translator and editorial tools for the journal Formalized Mathematics, tools for preparation data for MML Encyclopaedial Browser, editor to write hierarchical text (used by me to write Ph.D. thesis), teaching,
• TeX, LaTeX - typesetting of the journal Formalized Mathematics,
• Perl - CGI programs in MML Encyclopaedial Browser and CGI database management for lecture Programming over Internet,
• HTML, JavaScript, Java - MML Encyclopaedial Browser, database management interface, typesetting of electronic version of the journal Formalized Mathematics, teaching,
• PostgreSQL (+ Perl DBI) - MML Encyclopaedial Browser, Mizar lectures on the Internet,
• MS Office, Visual Basic - teaching.

• good - English, Russian,
• fair - German, speaking Japanese.

1. Association of Mizar Users (Stowarzyszenie Uzytkownikow Mizara), member of the Board
2. American Mathematical Society
3. Association for Automated Reasoning
4. Association for Computing Machinery, Polish Chapter
5. Polish Society of Logic and Philosophy of Sciences (Polskie Towarzystwo Logiczne i Filozofii Nauk)

• The Sleszynski Prize of the Association of Mizar Users (1991)
• The Lesniewski Prize of the Association of Mizar Users (1993)
• The Lesniewski Prize of the Association of Mizar Users (1996)
• The Prize of the Rector of Warsaw University, Bialystok Branch (1996)
• The Prize of the Rector of University of Bialystok (1997)
• The Postdoctoral Fellowship by Japanese Society for Promotion of Science (1999)

• 1996-1997 - leader of the topic group in ONR Grant N00014-95-1-1336.
• 1997-1998 - co-principal investigator in ONR Grant N00014-97-1-0777.
• 1998 - CSMSFB Grant, Berlin ICM'98.
• 2000 - 5th European Framework Program, CALCULEMUS, HPRN-CT-2000-00102.
• 2000 - Tokubetsu Kenkyuin Shorei-hi (Nr. 12000025) - Grant-in-Aid for Scientific Research.

• UCL - Universite catholique de Louvain, 1989, 1 month
• UofA - University of Alberta, 1993, 2 months
• Shinshu University, 1994, 2 months
• UofA - University of Alberta, 1998, 2 months
• TUB - Budapest University of Technology and Economics, 2000, 1 week

Teaching

• Algebra, 3rd grade of mathematics, 1997/98.
• Introduction to programming, 1st and 2nd grades of mathematics, 1997/98/99/2000.
• Introduction to computer use, 1st and 2nd grades of mathematics, 1997/98/99/2000.
• Mizar system, 3rd grade of computer science, 2000/01.

• Lattice theory, 3th grade of mathematics, 1998/99.
• Continuous lattices, 4th and 5th grades of mathematics, 1999/2000.
• Orders and numbers, 4th and 5th grades of mathematics, 1999/2000.
• Algebraic systems of reduction, 3rd grade of mathematics, 1998/99 and 1999/2000.
• Object programming, 4th and 5th grades of mathematics, 1999/2000.
• Programing over Internet, 3rd-5th grades of mathematics, 1998/99.

• Preseminar, 3rd grade, 1998/99 and 1999/2000.
• Lattice theory and topology, 4th and 5th grades, 1998/99.
• Machines and computability theory, 4th grade, 1999/2000.
• Lattice theory and reduction systems, 5th grade, 1999/2000.

• Marek Dudzicz, graduated in 2000
• Ewa Gradzka, graduated in 2000
• Jaroslaw Walesiuk, graduated in 2000
• Piotr Walesiuk, graduated in 2000

• Enrolment officer, 1991.
• Elected member of the Council of Faculty of Mathematics and Physics, University of Bialystok, 1998-1999.

Presentations and publications

• Tarski-Grothendieck set theory as knowledge management system, 36 Konferencja Historii Logiki, Cracow, 1990.
• Semi automated translation for mathematics, 26. Linguistischen Kolloquiums, Poznan, 1991. (co-speaker Patricia L. Carlson).
• Metoda lokalnych przesuniec, Wroclawsko-Warszawskie Seminarium Informatyki Teoretycznej, Wroclaw, 1994.
• The mutilated chessboard problem, The QED Workshop II, Warsaw, 1995.
• Mizaring the theory of continuous lattices, Computer Reconstruction of the Technology of Mathematics, University of Bialystok, May 22-23, 1998.
• Mizar - a work environment for a mathematician: an experiment with continuous lattices, International Congress of Mathematicians, Berlin, August 18-27, 1998.
• Journal of Formalized Mathematics - towards the encyclopaedia of mathematics, International Congress of Mathematicians, Berlin, August 18-27, 1998.
• Codifying mathematics. Case study: the theory of continuous lattices, 11-th International Congress of Logic, Methodology and Philosophy of Science, Cracow, August 20-26, 1999.
• Formalizacja w Mizarze na podstawie teorii krat ciaglych, Informatyka Teoretyczna: Metody analizy informacji niekompletnej i rozproszonej, Bialystok, November 26-28, 1999.
• Projekt Mizar, Konferencja sprawozdawcza grantow KBN, Zakopane, January, 2000.
• Mizar among automated deduction and reasoning systems, Budapest, March, 2000.
• Development of the Theory of Continuous Lattices in Mizar, CALCULEMUS-2000, St. Andrews, August, 2000.
• Algebra of constructors in Mizar system, Tsukuba Software Science Seminar, May, 2001.

List of selected publications:

Continuous lattices

1. 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, Natick, Massachsetts.
2. 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.
3. 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.
4. Duality based on Galois connection. Part I, Formalized Mathematics, to appear, (URL: http://mizar.org/JFM/Vol13/waybel34.html).
5. On Characterizations of Compactness, Formalized Mathematics, to appear, (URL: http://mizar.org/JFM/Vol13/yellow19.html), (coauthors Noboru Endou and Yuji Sakai).
6. The Characterization of the Continuity of Topologies, Formalized Mathematics, to appear, (URL: http://mizar.org/JFM/Vol12/waybel29.html), (coauthor Adam Naumowicz).
7. Lawson Topology and Continuous Lattices, Formalized Mathematics, to appear, (URL: http://mizar.org/JFM/Vol10/waybel21.html).
8. Prime ideals and filters, Formalized Mathematics, 6(2):241-247, 1997, (URL: http://mizar.org/JFM/Vol8/waybel_7.html).
9. The ``way-below'' relation, Formalized Mathematics, 6(1):169-176, 1997, (URL: http://mizar.org/JFM/Vol8/waybel_3.html).
10. Complete lattices, Formalized Mathematics, 2(5):719-725, 1991, (URL: http://mizar.org/JFM/Vol4/lattice3.html).

Set theory

11. 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.
12. A model of ZF set theory language. Formalized Mathematics, 1(1):131-145, 1990.
13. The contraction lemma. Formalized Mathematics, 1(1):201-203, 1990.
14. The reflection theorem. Formalized Mathematics, 1(5):973-977, 1990.
15. Universal classes. Formalized Mathematics, 1(3):595-600, 1990. (coauthor Bogdan Nowak)
16. Zermelo theorem and axiom of choice. Formalized Mathematics, 1(2):265-267, 1990.
17. Kuratowski - Zorn lemma. Formalized Mathematics, 1(2):387-393, 1990. (coauthor Wojciech A. Trybulec)
18. König's lemma. Formalized Mathematics, 2(3):397-402, 1991.

Universal algebras

19. Minimal signature for partial algebra. Formalized Mathematics, 5(3):405-414, 1996.
20. Translations, endomorphisms, and stable equational theories. Formalized Mathematics, 5(4):553-564, 1996.
21. Institution of many sorted algebras. Part I: Signature reduct of an algebra. Formalized Mathematics, 6(2):279-287, 1997.
22. Technical preliminaries to algebraica specifications, Formalized Mathematics, to appear,
23. Yet another construction of free algebra, Formalized Mathematics, to appear, (coauthor Artur Kornilowicz).

Abstract computers and formal verification

24. Combining of circuits. Formalized Mathematics, 5(2):283-295, 1996. (coauthor Yatsuka Nakamura)
25. Full adder circuit. Part I. Formalized Mathematics, 5(3):367-380, 1996. (coauthor Yatsuka Nakamura)
26. Development of terminology for SCM. Formalized Mathematics, 4(1):61-67, 1993. (coauthor Piotr Rudnicki)
27. A compiler of arithmetic expressions for SCM. Formalized Mathematics, 5(1):15-20, 1996. (coauthor Piotr Rudnicki)
28. Circuit generated by terms and circuits calculating terms, Formalized Mathematics, to appear, (URL: http://mizar.org/JFM/Vol13/circtrm1.html).
29. The set of primitive recursive functions, Formalized Mathematics, to appear, (URL: http://mizar.org/JFM/Vol13/comput_1.html), (coauthor Piotr Rudnicki).

Automated translation

30. 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 L. Carlson)