Andrzej Trybulec
Andrzej W. Trybulec | |
---|---|
Institutions | University of Białystok University of Warsaw Warsaw University of Technology Polish Academy of Sciences University of Connecticut All-Russian Scientific and Technical Information Institute |
Thesis | On some properties of the movable compacta (1975) |
Doctoral advisor | Karol Borsuk |
Notes | |
Andrzej Wojciech Trybulec (29 January 1941 in Kraków, Poland – 11 September 2013 in Białystok, Poland) was a Polish mathematician and computer scientist noted for work on the Mizar system.[1]
Early years
His parents Jan W. Trybulec and Barbara H. Kurlus both were professional pharmacists who owned a chemists shop in a small town
machine-readability of a mathematical text. He earned the doctoral degree in 1974 from the Institute of Mathematics of the Polish Academy of Sciences under Karol Borsuk
.
Research work
Trybulec's first
mathematical papers were in the various topological and metric space topics pioneered by Karol Borsuk. In parallel to his generic topological research, he also worked in computational linguistics and semantics of programming languages. Applying the framework of Tarski–Grothendieck set theory axioms, essentially the Zermelo–Fraenkel set theory supplemented by the Tarski axiom with all the objects being sets and eliminated notion of class, together with the first-order logic of the Gentzen-Jaśkowski natural deduction, in 1973 he designed the formalization system Mizar consisting of a formal language for writing mathematical definitions and proofs, a proof assistant, able to mechanically check proofs written in this language. Although the first presentation of the Mizar system on 14 November 1973 at a seminar in the Institute of Library Science and Scientific Information was an ideology understood as a visionary speculation rather than research project, his idea was later developed by himself and his collaborators to the Mizar Mathematical Library (MML), a library of formalized mathematics which can be used in the proof of new theorems and the world’s largest repository of formalized and computer-checked mathematics. Since 1978 until his death, he had lectured as a professor at the Institute of Computer Science at the University of Białystok, while in 1984-1985 hold visiting professorship at the Department of Computer Science and Engineering of the University of Connecticut
. He published a number of articles, mostly with the journal Formalized Mathematics dedicated to MML contributions.
Publications
- Asperti, Andrea; Bancerek, Grzegorz; Trybulec, Andrzej, eds. (2004), Mathematical Knowledge Management: Proceedings of Third International Conference, MKM 2004, Białowieża, Poland, September 19-21, 2004, Lecture Notes in Computer Science 3119, New York: Springer, ISBN 978-3-540-23029-8
See also
- Mizar system
- Timeline of Polish science and technology
- List of Polish mathematicians
- List of Polish people
References
Further reading
- Matuszewski, Roman; Zalewska, Anna, eds. (2007), "From Insight to Proof: Festschrift in Honour of Andrzej Trybulec" (PDF), ISBN 978-837431128-1
- Matuszewski, Roman; Rudnicki, Piotr (March 2005), "Mizar: The first 30 years" (PDF), Mechanized Mathematics and its Applications, 4 (1): 3–24
- Rudnicki, Piotr (1992), "An overview of the Mizar-Project", in Nordström, Bengt; Petersson, Kent; Plotkin, Gordon (eds.), Proceedings of the 1992 Workshop on Types for Proofs and Programs, Bästad, Sweden, June 1992, Båstad: Chalmers University of Technology, pp. 311–330
External links
- "Andrzej Trybulec", University of Bialystok
- Andrzej Trybulec at the Mathematics Genealogy Project
- Mizar System http://mizar.uwb.edu.pl
- http://math.uwb.edu.pl/~trybulec/awards.html
- https://web.archive.org/web/20060927204402/http://markun.cs.shinshu-u.ac.jp/mizar/mma.dir/2005/mma2005(2).pdf
- http://www-history.mcs.st-and.ac.uk/Biographies/Kuperberg.html
- http://mizar.uwb.edu.pl/cgi-bin/andrzej/memento
- http://www.openmath.org/meetings/eindhoven2003/proceedings/trybulec.pdf