Curriculum Vitae

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

Instytut Informatyki
Wydził Matematyczno-Fizyczny
Uniwersytet w Białymstoku

ul. Akademicka 2
15-267 Białystok, Polska

Wykształcenie:

• Stopień magistra: Uniwersytet Warszawski, Filia w Białymstoku (1990)
• Doktorat: Polska Akademia Nauk, Institytut Matematyczny (1997)

• 2000-2002 JSPS Postdoctoral Fellow
  Department of Information Engineering
  Faculty of Engineering
  Shinshu University
  Nagano, Japan
• 1999-2001 Adiunkt
  Instytut Informatyki
  Uniwersytet w Białymstoku
• 1998-1999 Adiunkt
  Instytut Matematyki
  Uniwersytet of Bialystok
• 1996-1997 Asystent
  Instytut Matematyki
  Uniwersytet Warszawski, Filia w Białymstoku
• 1992-1996 Doktorant
  Instytut Matematyczny
  Polska Akademia Nauk
• 1991-1992 Asystent
  Instytut Matematyczny
  Polska Akademia Nauk
• 1990-1991 Asystent
  Instytut Matematyki
  Uniwersytet Warszawski, Filia w Białymstoku

1. główna dziedzina - algebraiczne i kategoryjne aspecty logiki
2. inne dziedziny - kraty ciągłe, teoria obliczalności
3. obecne pole badań - komputerowo wspomagana formalizacja matematyki

1. Mizar formalization the theory of continuous lattices

Formalizacja w języku Mizar teorii krat ciągłych w oparciu o książkę A Compendium of Continuous Lattices, G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. Springer-Verlag, Berlin, Heidelberg, New York, 1980.

Podprojekt projektu 3. rozpoczęty w 1996 i nadal kontynuowany.

Rezultaty projektu: 57 artykułów Mizarowych napisanych przez 15 autorow z Polski, Kanady i Japonii.

Finansowany przez ONR Grant N00014-95-1-1336, ONR Grant N00014-97-1-0777, NATO Grant CRG 951368 oraz KBN Grant 8 T11C 018 12.

Mój wkład: kierownik projektu, 19 artykułów Mizarowych (w tym 4 współautorskie).

2. Journal of Formalized Mathematics

Automatyczne tłumaczenie i generowanie tekstu z języka Mizar na Math English na postać TeX'ową i HTML'ową. Programy wynikowe są używane do składu czasopisma Formalized Mathematics (ISSN 1426-2630) i jego elektronicznej wersji (URL: http://www.mizar.org/JFM/).

Projekt rozpoczęty w 1990 i nadal rozwijany.

Finansowany przez ONR Grant N00014-95-1-1336 i ONR Grant N00014-97-1-0777.

Mój wkład: twórca i deweloper oprogramowania.

3. Mizar Mathematical Library (MML)

MML jest kolekcją artykułów Mizarowych konsekwentnie rozwijających wiedzę matematyczną z aksjomatów teorii mnogości Tarskiego-Grothendiecka.

Projekt rozpoczęty w 1989 i nadal rozwijany.

Rezultaty projektu: 702 artykułów napisanych przez ponad 120 autorów z 9 krajów.

Mój wkład: 87 artykułów (w tym 24 współautorskich).

4. Mizar encyclopaedia

Interaktywne strony www (URL: http://megrez.mizar.org/services/ency/) do przeglądania, wyszukiwania i analizowania MML. Przeznaczone do pomocy i wspomagania pisania artykułów Mizarowych.

Projekt rozpoczęty w 2000.

Mój wkład: mój indywidualny projekt.

5. Mizar lectures on the Internet

Instrukcje komputerowe dostępne przez Internet (URL: http://megrez.mizar.org/classes/) do uczenia języka i systemu Mizar oraz MML. Tworzone jako część Shinshu University, Graduate School of Science and Technology on the Internet.

Projekt rozpoczęty w 2001.

Projekt jest w stanie projektowania.

Mój wkład: mój indywidualny projekt.

• Mizar - 87 artykułów, twórca oprogramowania, nauczanie,
• Pascal: turbo, Borland, object (Delphi, Kylix) - Mizarowe programy użytkowe: Abstractor, Bibart, translator i narzędzia edytorskie czasopisma Formalized Mathematics, programy przygotowujące dane dla MML Encyclopaedial Browser, edytor tekstu hierarchicznego (użyty przeze mnie do napisania rozprawy doktorskiej), nauczanie,
• TeX, LaTeX - skład czasopisma Formalized Mathematics,
• Perl - skrypty CGI w MML Encyclopaedial Browser i skrypty CGI obsługujące baze danych do wykładu Programowanie w Internecie,
• HTML, JavaScript, Java - MML Encyclopaedial Browser, database management interface, skład elektronicznej wersji czasopisma Formalized Mathematics, nauczanie,
• PostgreSQL (+ Perl DBI) - MML Encyclopaedial Browser, Mizar lectures on the Internet,
• MS Office, Visual Basic - nauczanie.

• dobra znajomość - angielski, rosyjski,
• słaba znajomość - niemiecki, mówiony japoński.

1. Association of Mizar Users (Stowarzyszenie Uzytkownikow Mizara), członek Zarządu
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)

• Nagroda Sleszyńskiego Stowarzyszenia Użytkowników Mizara, 1991
• Nagroda Leśniewskiego Stowarzyszenia Użytkowników Mizara, 1993
• Nagroda Leśniewskiego Stowarzyszenia Użytkowników Mizara, 1996
• Nagroda Rektora Uniwersytetu Warszawskiego, Filii w Białymstoku, 1996
• Nagroda Rektora Uniwersytetu w Białymstoku, 1997
• The Postdoctoral Fellowship przyznany przez Japonese Society for Promotion of Science, 1999

• 1996-1997 - kierownik grupy tematycznej w ONR Grant N00014-95-1-1336.
• 1997-1998 - ``co-principal investigator'' w ONR Grant N00014-97-1-0777.
• 1998 - CSMSFB Grant, Berlin ICM'98.
• 2000 - 5 Europejski Program Ramowy, CALCULEMUS-RTN1-1999-00301.
• 2000 - Tokubetsu Kenkyuin Shorei-hi (Nr. 12000025) - Grant-in-Aid for Scientific Research.

• UCL - Universite catholique de Louvain, 1989, 1 miesiąc
• UofA - University of Alberta, 1993, 2 miesiące
• Shinshu University, 1994, 2 miesiące
• UofA - University of Alberta, 1998, 2 miesiące
• TUB - Budapest University of Technology and Economics, 2000, 1 tydzień

Nauczanie

• Algebra, III rok matematyki, 1997/98.
• Wstęp do programowania, I i II rok matematyki, 1997/98/99/2000.
• Pracownia komputerowa, I i II rok matematyki, 1997/98/99/2000.
• Mizar system, III rok informatyki, 2000/01.

• Teoria krat, III rok matematyki, 1998/99.
• Kraty ciągłe, IV i V rok matematyki, 1999/2000.
• Porządki i liczby, IV i V rok matematyki, 1999/2000.
• Algebraiczne systemy redukcji, III rok matematyki, 1998/99 i 1999/2000.
• Programowanie obiektowe, IV i V rok matematyki, 1999/2000.
• Programowanie w Internecie, III-V rok matematyki, 1998/99.

• Preseminarium, III rok matematyki, 1998/99 i 1999/2000.
• Teoria krat i topologia, IV i V rok matematyki, 1998/99.
• Maszyny i teoria obliczalności, IV rok matematyki, 1999/2000.
• Teoria krat i systemy redukcji, V rok matematyki, 1999/2000.

• Marek Dudzicz, obronił magisterium w 2000
• Ewa Grądzka, obroniła magisterium w 2000
• Jarosław Walesiuk, obronił magisterium w 2000
• Piotr Walesiuk, obronił magisterium w 2000

• Sekretarz komisji rekrutacyjnej, 1991.
• Wybieralny członek Rady Wydziału Matematyczno-Fizycznego, Uniwersytetu w Białymstoku, 1998-1999.

Prezentacje i publikacje

• 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.

Lista wybranych publikacji:

Kraty ciągłe

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).

Teoria mnogości

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.

Algebry uniwersalne

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).

Komputery abstrakcyjne i formalna weryfikacja

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ćirctrm1.html).
29. The set of primitive recursive functions, Formalized Mathematics, to appear, (URL: http://mizar.org/JFM/Vol13ćomput_1.html), (coauthor Piotr Rudnicki).

Tłumaczenie automatyczne

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)