Adam Naumowicz

• Education and interests
• List of publications
• Information for students
• Personal information
• Miscellanea
• Contact

• Automated proof checking and theorem proving (development of the Mizar system)
• Computer aided formalization of mathematics (development of Mizar Mathematical Library)
• Formal methods in computer science education
• Also: general topology, continuous lattices, algebraic geometry

Formalized Mathematics Editor	Central European Journal of Computer Science Managing Editor	Studies in Logic, Grammar and Rhetoric Guest Editor for a special issue on Computer Reconstruction of the Body of Mathematics

• Programming: Pascal, C, C++, Java, Perl
• OS administration: Linux (Red Hat Certified Technician (RHCT) and Red Hat Certified Engineer (RHCE) for Red Hat Enterprise Linux 5), FreeBSD, Solaris
• Languages: Polish (native), English, Russian

• CADE 23, The 23rd International Conference on Automated Deduction, July 31-August 5, 2011, Wroclaw, Poland
• CICM 2011, Conference on Intelligent Computer Mathematics, July 18-23, 2011, Bertinoro, Italy (Programme Committee member)
• AMS Special Session on Formal Mathematics for Mathematicians: Developing Large Repositories of Advanced Mathematics, New Orleans, USA, January 6-9, 2011
• TYPES 2010, The 17th Workshop Types for Proofs and Programs, October 13-16, 2010, Warsaw, Poland
• MKM 2010, The 9th International Conference on Mathematical Knowledge Management - as part of Conferences on Intelligent Computer Mathematics (CICM 2010) - July 5-10, 2010, Paris, France (Programme Committee member)
• Cooperative research at Shinshu University, Nagano, Japan, February 2-28, 2010
• Third Indian School on Logic and its Applications, January 18-29, 2010, University of Hyderabad, Gachibowli, India, [download slides]
• TPHOLs 2009, Theorem Proving in Higher Order Logics, 17-20 August, 2009, Munich, Germany [download slides]
• ETAPS 2008 satellite event Formal Methods in Computer Science Education (FORMED2008), March 29, 2008, Budapest, Hungary [download slides]
• TYPES topical workshop MathWiki, October 31 - November 1, 2007, Edinburgh, UK [download slides]
• TYPES Summer School 2007, August 19-31, 2007, Bertinoro, Italy [download slides]
• RDP 2007 affiliated TYPES Workshop on Proof Assistants and Types in Education, June 25, 2007, Paris, France (Programme Committee member)
• TYPES 2006, Conference of the TYPES Project, April 18-21, 2006, Nottingham, UK
• TYPES Summer School 2005, Proofs of Programs and Formalisation of Mathematics, August 15-26, 2005, Goteborg, Sweden
• MKM 2005, Fourth International Conference on Mathematical Knowledge Management, July 15-17, 2005, Bremen, Germany
• Small TYPES Workshop: High Level Languages for Proofs, April 13-14, 2005, Chambery, France [download slides]
• MKM 2004, Third International Conference on Mathematical Knowledge Management, September 19-21, 2004, Bialowieza, Poland
• The Prague 2004 Workshop on Knowledge Management in Formalized Mathematics, June 27-29, 2004, Prague, Czech Republic
• MKM Symposium, November 25-29, 2003, Edinburgh, UK
• CALCULEMUS 2003, 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, September 10-12, 2003, Rome, Italy
• MONET 2003, Mathematics on the Semantic Web, May 12-14, 2003, Eindhoven, The Netherlands
• TYPES 2003, Workshop of the TYPES Working Group, April 30 - May 4, 2003, Turin, Italy
• TYPES 2002, Workshop of the TYPES Working Group, April 24-28, 2002, Berg en Dal (near Nijmegen), The Netherlands
• Cooperative research at Shinshu University, Nagano, Japan - 'Verification of Circuit designs with the Aid of the Mizar System', January 1 - March 12, 2002
• CALCULEMUS 2001, 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, June 21-22, 2001, Siena, Italy

• Association of Mizar Users (Stowarzyszenie Uzytkownikow Mizara), member of the Board of Control

• 2009-2011: MNiSW Grant N519 385136
• 2004-2008: TYPES II EU FP6 510996
• 2003-2006: KBN Grant 4 T11C 039 24
• 2000-2004: CALCULEMUS EU FP5 HPRN-CT-2000-00102
• 2000-2003: TYPES EU FP5 IST-1999-29001
• 1997-1998: ONR Grant N00014-97-1-0777
• 1997-1998: KBN Grant 8 T11C 018 12

• Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, Josef Urban. Licensing the Mizar Mathematical Library. In J. Davenport et al. (Eds.), CALCULEMUS/MKM 2011, LNAI 6824, pp. 149-163, Springer-Verlag Berlin Heidelberg, 2011
• Takao Inoue, Adam Naumowicz, Noboru Endou, Yasunari Shidama. Partial Differentiation, Differentiation and Continuity on n-Dimensional Real Normed Linear Spaces. Formalized Mathematics 19(2), pp. 65-68, 2011
• Takao Inoue, Adam Naumowicz, Noboru Endou, Yasunari Shidama. Partial Differentiation of Vector-Valued Functions on n-Dimensional Real Normed Linear Spaces. Formalized Mathematics 19(1), pp. 1-9, 2011
• Adam Grabowski, Artur Kornilowicz, Adam Naumowicz. Mizar in a Nutshell. In A. Asperti, J. Harrison and C. Munoz (Eds.) User Tutorials I. Journal of Formalized Reasoning 3(2), pp. 153-245, 2010.
• Adam Naumowicz. Interfacing External CA Systems for Gröbner Bases Computation in Mizar Proof Checking. International Journal of Computer Mathematics 87(1), pp. 1-11, 2010
• Adam Grabowski, Adam Naumowicz (Eds.) Computer Reconstruction of the Body of Mathematics. Studies in Logic, Grammar and Rhetoric 18(31), 2009
• Adam Naumowicz. Enhanced Processing of Adjectives in Mizar. In A. Grabowski and A. Naumowicz (Eds.), Computer Reconstruction of the Body of Mathematics, Studies in Logic, Grammar and Rhetoric 18(31), pp. 89-101, 2009
• Adam Naumowicz, Artur Kornilowicz. A Brief Overview of Mizar. In S. Berghofer et al. (Eds.), TPHOLs 2009, LNCS 5674, pp. 67-72, Springer-Verlag Berlin Heidelberg, 2009
• Adam Naumowicz. Teaching How to Write a Proof. In Proceedings of ETAPS 2008 satellite workshop Formal Methods in Computer Science Education (FORMED2008) pp. 91-100, Budapest, March 29, 2008
• Adam Naumowicz. Formalization of the Tietze Extension Theorem in Mizar. Mechanized Mathematics and Its Applications, Vol. 6, No. 1, pp. 41-45, Mizar Japan, 2007
• Adam Naumowicz. Evaluating Prospective Built-in Elements of Computer Algebra in MIZAR. In R. Matuszewski and A. Zalewska (Eds.), From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric 10(23), pp. 191-200, 2007
• Adam Naumowicz. How to Teach to Write a Proof. In Proceedings of RDP 2007 affiliated TYPES Workshop on Proof Assistants and Types in Education, pp. 69-76, Paris, June 25, 2007
• Adam Naumowicz. An Example of Formalizing Recent Mathematical Results in MIZAR. In C. Benzmueller (Ed.), Towards Computer Aided Mathematics, Journal of Applied Logic, 4(4), pp. 396-413, Elsevier, 2006
• Adam Naumowicz. On the Representation of Natural Numbers in Positional Numeral Systems. Formalized Mathematics, 14(4), pp. 221-223, 2006
• Adam Naumowicz, Grzegorz Bancerek. Homeomorphisms of Jordan Curves. Formalized Mathematics, 13(4), pp. 477-480, 2005
• Artur Kornilowicz, Grzegorz Bancerek, Adam Naumowicz. Tietze Extension Theorem. Formalized Mathematics, 13(4), pp. 471-475, 2005
• Adam Naumowicz. Spaces of Pencils, Grassmann Spaces, and Generalized Veronese Spaces. Formalized Mathematics, 13(1), pp. 133-138, 2005
• Adam Naumowicz. On the Characterisation of Collineations of the Segre Product of Strongly Connected Partial linear Spaces. Formalized Mathematics, 13(1), pp. 125-131, 2005
• Adam Naumowicz, Czeslaw Bylinski. Improving MIZAR Texts with Properties and Requirements. In A. Asperti et al. (Eds.), MKM 2004, LNCS 3119, pp. 290-301, Springer-Verlag Berlin Heidelberg, 2004
• Adam Naumowicz, Krzysztof Prazmowski. The Geometry of Generalized Veronese Spaces. Results in Mathematics, vol. 45, pp. 115-136, Birkhauser Verlag, 2004
• Adam Naumowicz, Czeslaw Bylinski. Basic Elements of Computer Algebra in MIZAR. Mechanized Mathematics and Its Applications, Vol. 2, pp. 9-16, Mizar Japan, 2002
• Grzegorz Bancerek, Adam Naumowicz. Preliminaries to Automatic Generation of Mizar Documentation for Circuits. Formalized Mathematics, 10(3), pp. 117-133, 2002
• Adam Naumowicz, Robert Milewski. Some Remarks on Clockwise Oriented Sequences on Go-boards. Formalized Mathematics, 10(1), pp. 23-27, 2002
• Adam Naumowicz, Krzysztof Prazmowski. On Segre's product of partial line spaces and spaces of pencils. Journal of Geometry, vol. 71, pp. 128-143, Birkhauser Verlag, 2001
• Adam Naumowicz. On cosets in Segre's product of partial linear spaces. Formalized Mathematics, 9(4), pp. 801-806, 2001
• Adam Naumowicz. Some remarks on finite sequences on Go-boards. Formalized Mathematics, 9(4), pp. 821-824, 2001
• Artur Kornilowicz, Robert Milewski, Adam Naumowicz, Andrzej Trybulec. Some properties of cells and arcs. Formalized Mathematics, 9(3), pp. 535-539, 2001
• Artur Kornilowicz, Robert Milewski, Adam Naumowicz, Andrzej Trybulec. Gauges and cages.Part I. Formalized Mathematics, 9(3), pp. 505-513, 2001
• Adam Naumowicz. Segre's product of partial line spaces. Formalized Mathematics, 9(2), pp. 383-390, 2001
• Grzegorz Bancerek, Adam Naumowicz. The characterization of the continuity of topologies. Formalized Mathematics, 9(2), pp. 231-236, 2001
• Adam Naumowicz. A note on affine partial linear spaces. Geometria Wykreslna i Grafika Inzynierska (Descriptive geometry and engineering graphics) Zeszyt nr. 5, ISSN 1425-333X, pp. 57-62, Wroclaw Technical University, 2000
• Grzegorz Bancerek, Adam Naumowicz. Function spaces in the category of directed suprema preserving maps. Formalized Mathematics, 9(1), pp. 171-176, 1999
• Adam Naumowicz, Agnieszka Julia Marasik. The correspondence between lattices of subalgebras of universal algebras and many sorted algebras. Formalized Mathematics, 7(2), pp. 227-231, 1998
• Adam Naumowicz. On the characterization of modular and distributive lattices. Formalized Mathematics, 7(1), pp. 53-55, 1998
• Adam Naumowicz, Mariusz Lapinski. On T_1 reflex of topological space. Formalized Mathematics, 7(1), pp. 31-34, 1998
• Adam Naumowicz. Conjugate sequences, bounded complex sequences and convergent complex sequences. Formalized Mathematics, 6(2), pp. 265-268, 1997

• Podstawy Programowania (in Polish)
• Podstawy Metod Formalnych (in Polish)
• Systemy operacyjne (in Polish)
• Programowanie niskopoziomowe (Assembler) (in Polish)
• Programowanie w internecie (in Polish)
• Information Technology as a Tool for Self-Education

---

Contact adamn@math.uwb.edu.pl

---

Last modification : Fri Dec 30 13:24:18 2011 GMT
This page has been accessed 21000 times.