This page is available under URL:
http://www.cs.shinshuu.ac.jp/~bancerek/cv.html
Curriculum Vitae
Date: August 29, 2001
Surname: Bancerek
First name: Grzegorz
Date and place of birth: August 29, 1966; Makowo, Poland
Marital status: Married, 2 children (born 1993, 1996)
Nationality: Polish
Scientific position:
Associate Professor,
JSPS Postdoctoral Fellow
Affiliation and office address:
Department of Information Engineering
Faculty of Engineering
Shinshu University
3808553 Japan
Naganoken, Naganocity
Wakasato 4171
Previous affiliation
Institute of Computer Science
Faculty
of Mathematics and Physics
University of Bialystok
ul. Akademicka 2
15267 Bialystok, Poland
Email:
bancerek@mizar.org
Www:
http://www.cs.shinshuu.ac.jp/~bancerek/
Education:
 Master degree: Warsaw University, Bialystok Campus (1990)
 Doctorate: Polish Academy of Sciences, Institute of Mathematics (1997)
Employment:
Specialization:
 main field  algebraic and categorial aspects of logic
 other fields  continuous lattices, computation theory
 current research interest 
computer aided formalization of mathematics
Project contributions
 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.
SpringerVerlag, 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 N000149511336, ONR Grant N000149710777, 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 14262630) and its electronic version
(URL: http://www.mizar.org/JFM/).
 Project started in 1990 and is still developed.
 Supported by ONR Grant N000149511336 and ONR Grant N000149710777.
 My contribution: software designer and developer.
 3. Mizar Mathematical Library (MML)
 MML is a collection of Mizar articles consequently
developing mathematical knowledge from TarskiGrothendieck 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.
Computer systems and programming experiences
 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.
Languages
 good  English, Russian,
 fair  German, speaking Japanese.
Membership of Professional Societies:
 Association of Mizar Users (Stowarzyszenie Uzytkownikow Mizara), member of the Board
 American Mathematical Society
 Association for Automated Reasoning
 Association for Computing Machinery,
Polish Chapter
 Polish Society of Logic and Philosophy of Sciences
(Polskie Towarzystwo Logiczne i Filozofii Nauk)
Awards:
 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)
Grants:
 19961997  leader of the topic group in ONR Grant N000149511336.
 19971998  coprincipal investigator in ONR Grant N000149710777.
 1998  CSMSFB Grant, Berlin ICM'98.
 2000  5th European Framework Program, CALCULEMUS, HPRNCT200000102.
 2000  Tokubetsu Kenkyuin Shoreihi (Nr. 12000025)
 GrantinAid for Scientific Research.
Short visits:
 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
Regular lectures
 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.
Monographic lectures
 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, 3rd5th grades of mathematics, 1998/99.
Seminars
 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.
Master's students
 Marek Dudzicz, graduated in 2000
 Ewa Gradzka, graduated in 2000
 Jaroslaw Walesiuk, graduated in 2000
 Piotr Walesiuk, graduated in 2000
Other university activity
 Enrolment officer, 1991.
 Elected member of the Council of Faculty of Mathematics and Physics, University of Bialystok,
19981999.
Presentations and publications
Presentations:
 TarskiGrothendieck set theory as knowledge management system, 36 Konferencja Historii Logiki, Cracow, 1990.
 Semi automated translation for mathematics,
26. Linguistischen Kolloquiums, Poznan, 1991. (cospeaker Patricia L. Carlson).
 Metoda lokalnych przesuniec, WroclawskoWarszawskie 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 2223, 1998.
 Mizar  a work environment for a mathematician: an experiment with continuous lattices,
International Congress of Mathematicians, Berlin, August 1827, 1998.
 Journal of Formalized Mathematics  towards the encyclopaedia of mathematics,
International Congress of Mathematicians, Berlin, August 1827, 1998.
 Codifying mathematics. Case study: the theory of continuous lattices,
11th International Congress of Logic, Methodology and Philosophy of Science,
Cracow, August 2026, 1999.
 Formalizacja w Mizarze na podstawie teorii krat ciaglych,
Informatyka Teoretyczna: Metody analizy informacji niekompletnej i rozproszonej,
Bialystok, November 2628, 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,
CALCULEMUS2000, St. Andrews, August, 2000.
 Algebra of constructors in Mizar system,
Tsukuba Software Science Seminar,
May, 2001.
List of selected publications:
 Continuous lattices

Development of the Theory of Continuous Lattices in Mizar.
In M. Kerber and M. Kohlhase, editors,
Symbolic Computation and Automated Reasoning,
pages 6580, The CALCULEMUS2000 Symposium,
A.K.Peters, Natick, Massachsetts.

Codifying mathematics. Case study: the theory of continuous lattices.
In Volume of Abstracts,
11th International Congress of Logic, Methodology and Philosophy of Science,
Cracow, August 2026, 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 1827, 1998.
 Duality
based on Galois connection. Part I, Formalized Mathematics,
to appear, (URL: http://mizar.org/JFM/Vol13/waybel34.html).
 On
Characterizations of Compactness, Formalized Mathematics,
to appear, (URL: http://mizar.org/JFM/Vol13/yellow19.html),
(coauthors
Noboru Endou and
Yuji Sakai).
 The
Characterization of the Continuity of Topologies,
Formalized Mathematics, to appear,
(URL: http://mizar.org/JFM/Vol12/waybel29.html),
(coauthor Adam Naumowicz).
 Lawson Topology and Continuous Lattices,
Formalized Mathematics, to appear,
(URL: http://mizar.org/JFM/Vol10/waybel21.html).
 Prime ideals and filters,
Formalized Mathematics, 6(2):241247, 1997,
(URL: http://mizar.org/JFM/Vol8/waybel_7.html).
 The ``waybelow'' relation,
Formalized Mathematics, 6(1):169176, 1997,
(URL: http://mizar.org/JFM/Vol8/waybel_3.html).
 Complete lattices,
Formalized Mathematics, 2(5):719725, 1991,
(URL: http://mizar.org/JFM/Vol4/lattice3.html).
 Set theory
 The mutilated chessboard problem.
In R. Matuszewski, editor, The QED Workshop II, Technical
Report No. L/1/95, pages 3738, Warsaw University, Bialystok Branch,
1995.
 A model of ZF set theory language.
Formalized Mathematics, 1(1):131145, 1990.
 The contraction lemma.
Formalized Mathematics, 1(1):201203, 1990.
 The reflection theorem.
Formalized Mathematics, 1(5):973977, 1990.
 Universal classes.
Formalized Mathematics, 1(3):595600, 1990.
(coauthor Bogdan Nowak)
 Zermelo theorem and axiom of choice.
Formalized Mathematics, 1(2):265267, 1990.
 Kuratowski  Zorn lemma.
Formalized Mathematics, 1(2):387393, 1990.
(coauthor Wojciech A. Trybulec)
 König's lemma.
Formalized Mathematics, 2(3):397402, 1991.
 Universal algebras
 Minimal signature for partial algebra.
Formalized Mathematics, 5(3):405414, 1996.
 Translations, endomorphisms, and stable equational theories.
Formalized Mathematics, 5(4):553564, 1996.
 Institution of many sorted algebras. Part I: Signature reduct of
an algebra.
Formalized Mathematics, 6(2):279287, 1997.
 Technical preliminaries to algebraica specifications,
Formalized Mathematics, to appear,
 Yet another construction of free algebra,
Formalized Mathematics, to appear,
(coauthor Artur Kornilowicz).
 Abstract computers and formal verification

Combining of circuits.
Formalized Mathematics, 5(2):283295, 1996.
(coauthor Yatsuka Nakamura)

Full adder circuit. Part I.
Formalized Mathematics, 5(3):367380, 1996.
(coauthor Yatsuka Nakamura)

Development of terminology for SCM.
Formalized Mathematics, 4(1):6167, 1993.
(coauthor Piotr Rudnicki)

A compiler of arithmetic expressions for SCM.
Formalized Mathematics, 5(1):1520, 1996.
(coauthor Piotr Rudnicki)

Circuit generated by terms and circuits calculating terms,
Formalized Mathematics, to appear,
(URL: http://mizar.org/JFM/Vol13/circtrm1.html).

The set of primitive recursive functions,
Formalized Mathematics, to appear,
(URL: http://mizar.org/JFM/Vol13/comput_1.html),
(coauthor Piotr Rudnicki).
 Automated translation
 Semi automated translation for mathematics.
In J. Darski and Z. Vetulani, editors,
SpracheKommunikationInformatik, pages 131136, Akten des 26.
Linguistischen Kolloquiums, Niemeyer, Poznan, 1991.
(coauthor Patricia L. Carlson)
Curriculum vitae 1998