Christoph Schwarzweller: Papers

• Existence and Uniqueness of Algebraic Closures
  in: Journal of Formalized Mathematics, vol. 30(4), pp. 281-294, 2022.

• Artin’s Theorem Towards the Existence of Algebraic Closures
  in: Journal of Formalized Mathematics, vol. 30(3), pp. 199-207, 2022.

• Splitting Fields for the Rational Polynomials X^2-2, X^2+X+1, X^3-1, and X^3-2
  (with S. Burgoa)
  in: Journal of Formalized Mathematics, vol. 30(1), pp. 23-30, 2022.

• Quadratic Extensions
  (with A. Rowińska-Schwarzweller)
  in: Journal of Formalized Mathematics, vol. 29(4), pp. 229-240, 2021.

• Splitting Fields
  in: Journal of Formalized Mathematics, vol. 29(3), pp. 129-139, 2021.

• Algebraic Extensions
  (with A. Rowińska-Schwarzweller)
  in: Journal of Formalized Mathematics, vol. 29(1), pp. 39-47, 2021.

• Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials
  in: Journal of Formalized Mathematics, vol. 28(3), pp. 251-261, 2020.

• Refining Algebraic Hierarchy in Mathematical Repository Mizar
  (with A. Korniłowicz and A. Grabowski)
  in: A. Grabowski, R. Loukanova, Ch. Schwarzweller (eds.),
  AI Aspects in Reasoning, Languages, and Computation Stud. Comp. Intelligence vol. 889, Springer, pp. 49-75, 2020.

• Renamings and a Condition-free Formalization of Kronecker's Construction
  in: Journal of Formalized Mathematics, vol. 28(2), pp. 129-135, 2020.

• Field Extensions and Kronecker's Construction
  in: Journal of Formalized Mathematics, vol. 27(3), pp. 229-235, 2019.

• On the Intersection of Fields F with F[X]
  in: Journal of Formalized Mathematics, vol. 27(3), pp. 223-228, 2019.

• On Monomorphims and Subfields
  in: Journal of Formalized Mathematics, vol. 27(2), pp. 133-137, 2019.

• On Roots of Polynomials over F[X]/‹p›
  in: Journal of Formalized Mathematics, vol. 27(2), pp. 93-100, 2019.

• Representation Matters: An Unexpected Property of Polynomial Rings and its Consequences for Formalizing Abstract Field Theory
  in: M. Ganzha, L. Maciaszek, M. Paprzycki (eds.),
  Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, ACSIS, vol. 15, pp. 67-72, 2018.

• Formally Real Fields
  in: Journal of Formalized Mathematics, vol. 25(4), pp. 249-259, 2017.

• On Roots of Polynomials and Algebraically Closed Fields
  in: Journal of Formalized Mathematics, vol. 25(3), pp. 185-195, 2017.

• Ordered Rings and Fields
  in: Journal of Formalized Mathematics, vol. 25(1), pp. 63-72, 2017.

• Some Algebraic Properties of Polynomial Rings
  (with A. Korniłowicz and A. Rowińska-Schwarzweller)
  in: Journal of Formalized Mathematics, vol. 24(3), pp. 227-237, 2016.

• On Algebraic Hierarchies in Mathematial Repository of Mizar
  (with A. Grabowski and Artur Korniłowicz)
  in: M. Ganzha, L. Maciaszek, M. Paprzycki (eds.),
  Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, ACSIS, vol. 8, pp. 363-371, 2016.

• Characteristic of Rings and Prime Fields
  (with A. Korniłowicz)
  in: Journal of Formalized Mathematics, vol. 23(4), pp. 333-349, 2015.

• Equality in Computer Proof-Assistants
  (with A. Grabowski and A. Korniłowicz)
  in: M. Ganzha, L. Maciaszek, M. Paprzycki (eds.),
  Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, ACSIS, vol. 5, pp. 45-54, 2015.

• The First Isomorphism Theorem and Other Properties of Rings
  (with A. Korniłowicz)
  in: Journal of Formalized Mathematics, vol. 22(4), pp. 291-301, 2014.

• Towards Standard Environments for Formalizing Mathematics
  (with A. Grabowski)
  in: Proceedings of the 6th Podlasie Conference on Mathematics, Białystok, Poland, 2014.

• Proth Numbers
  in: Journal of Formalized Mathematics, vol. 22(2), pp. 111-118, 2014.

• A Test for the Stability of Networks
  (with A. Rowińska-Schwarzweller)
  in: Journal of Formalized Mathematics, vol. 21(1), pp. 47-53, 2013.

• Towards Automatically Categorizing Mathematical Knowledge
  (with A. Grabowski)
  in: M. Ganzha, L. Maciaszek, M. Paprzycki (eds.),
  Proceedings of the 7th International Symposium on Advances in Artificial Intelligence and Applications, pp.63-68, 2012.

• Introduction to Rational Functions
  in: Journal of Formalized Mathematics, vol. 20(2), pp. 181-191, 2012.

• On Duplication in Mathematical Repositories
  (with A. Grabowski)
  in: S. Autexier, J. Calmet et.al. (eds.), Intelligent Computer Mathematics,
  Lecture Notes in Computer Science 6167, pp. 300-314, 2010. © Springer-Verlag

• On Building a Knowledge Base for Stability Theory
  (with A. Rowińska-Schwarzweller)
  in: S. Autexier, J. Calmet et.al. (eds.), Intelligent Computer Mathematics,
  Lecture Notes in Computer Science 6167, pp. 427-439, 2010. © Springer-Verlag

• The Chinese Remainder Theorem, its Proofs and its Generalizations in Mathematical Repositories
  in: Studies in Logic, Grammar and Rhetoric 18(31), p. 103-119, 2009.

• Improving Representation of Knowledge within the Mizar Library
  (with A. Grabowski)
  in: Studies in Logic, Grammar and Rhetoric 18(31), p. 35-50, 2009.

• Modular Integer Arithmetic
  in: Journal of Formalized Mathematics, vol. 16(3), pp. 253-258, 2008.

• Towards Mathematical Knowledge Management for Electrical Engineering
  (with A. Rowińska-Schwarzweller)
  in: M. Kauers, M. Kerber, R. Miner, W. Windsteiger (eds.), Towards Mechanized Mathematical Assistants,
  Lecture Notes in Artificial Intelligence 4573, pp. 371-380, 2007. © Springer-Verlag

• Revisions as an Essential Tool to Maintain Mathematical Repositories
  (with A. Grabowski)
  in: M. Kauers, M. Kerber, R. Miner, W. Windsteiger (eds.), Towards Mechanized Mathematical Assistants,
  Lecture Notes in Artificial Intelligence 4573, pp. 235-249, 2007. © Springer-Verlag

• Mizar Attributes: A Technique to Encode Mathematical Knowledge into Type Systems
  in: Studies in Logic, Grammar and Rhetoric, vol. 10(23), pp. 387-400, 2007.

• Schur's Theorem on the Stability of Networks
  (with A. Rowińska-Schwarzweller)
  in: Journal of Formalized Mathematics, vol. 14(4), pp. 135-142, 2006.

• Multiplication of Polynomials using Discrete Fourier Transformation
  (with K. Treyderowski)
  in: Journal of Formalized Mathematics, vol. 14(4), pp. 121-128, 2006.

• Translating Mathematical Vernacular into Knowledge Repositories
  (with A. Grabowski)
  in: M. Kohlhase (ed.), Proceedings of the 4th International Conference on Mathematical Knowledge Management,
  Lecture Notes in Artificial Intelligence 3863, pp. 49-64, 2006. © Springer-Verlag

• Gröbner Bases --- Theory Refinement in the Mizar System
  in: M. Kohlhase (ed.), Proceedings of the 4th International Conference on Mathematical Knowledge Management,
  Lecture Notes in Artificial Intelligence 3863, pp. 299-314, 2006. © Springer-Verlag

• Computers and Algorithms in the Mizar System
  (with A. Korniłowicz)
  in: Mechanized Mathematics and its Applications, vol. 4(1), pp. 43-50, 2005.

• Construction of Gröbner Bases: Buchberger's First Criterium
  in: Journal of Formalized Mathematics, vol. 13(1), pp. 147-156, 2005.

• Rough Concept Analysis --- Theory Development in the Mizar System
  (with A. Grabowski)
  in: A. Asperti, G. Bancerek, A. Trybulec (eds.), Proceedings of the 3rd International Conference on Mathematical Knowledge Management,
  Lecture Notes in Computer Science 3119, pp. 130-144, 2004. © Springer-Verlag

• Computers and Algorithms in the Mizar System
  (with A. Korniłowicz)
  in: G. Bancerek, A. Grabowski (eds.), Proceedings of the International Workshop ''30 Years of Mizar", Białowieża, Poland, September 2004.

• Towards Formal Support for Generic Programming
  Habilitation thesis, Wilhelm-Schickard-Institute for Computer Science, University of Tübingen, 2003.

• Checking Semantic Requirements of Generic Algorithms
  (with H. Gast)
  unpublished manuscript, 2003.

• Construction of Gröbner bases. S-Polynomials and Standard Representations
  in: Journal of Formalized Mathematics, vol. 11(3-4), pp. 313-322, 2003.

• Characterization and Existence of Gröbner Bases
  in: Journal of Formalized Mathematics, vol. 11(3-4), pp. 303-312, 2003.

• Designing Mathematical Libraries based on Requirements for Theorems
  in: Annals of Mathematics and Artificial Intelligence, vol. 38(1-3), p. 193-209, 2003. © Kluwer Academic Publishers

• Polynomial Reduction
  in: Journal of Formalized Mathematics, vol. 11(1-2), pp. 113-124, 2003.

• Term Orders
  in: Journal of Formalized Mathematics, vol. 11(1-2), pp. 105-112, 2003.

• Symbolic Deduction in Mathematical Databases based on Properties
  in: S. Colton, V. Sorge (eds.), Proceedings of the 2nd International Workshop on the Role of Automated Deduction in Mathematics
  (RADM2002), Kopenhagen, Denmark, July 2002.

• Algebraic Requirements for the Construction of Polynomial Rings
  (with Robert Milewski)
  in: Mechanized Mathematics and its Applications, vol. 2(1), pp. 1-8, 2002.

• Defining Gröbner Bases in the Concept Description Language Tecton
  unpublished manuscript, 2001.

• More on Multivariate Polynomials: Monomials and Constant Polynomials
  in: Journal of Formalized Mathematics, vol.9(4). pp. 849-856, 2001.

• Designing Mathematical Libraries based on Minimal Requirements for Theorems
  in: B. Buchberger, O. Caprotti (eds.), Proceedings of the 1st International Workshop on Mathematical Knowledge Management
  (MKM2001), Linz, Austria, September 2001.

• Commutative Algebra in the Mizar System
  (with Piotr Rudnicki and Andrzej Trybulec)
  in: Journal of Symbolic Computation, vol. 32(1/2), pp. 143-169, 2001. © Elsevier

• Ring Ideals
  (with Jonathan Backer and Piotr Rudnicki)
  in: Journal of Formalized Mathematics, vol.9(3), pp. 565-583, 2000.

• The Binomial Theorem for Algebraic Structures
  in: Journal of Formalized Mathematics, vol.9(3), pp. 559-564, 2000.

• Defining Power Series and Polynomials in Mizar
  (with Piotr Rudnicki and Andrzej Trybulec)
  in: M. Kerber, M. Kohlhase (eds.), Symbolic Computation and Automated Reasoning: The Calculemus-2000 Symposium,
  pp. 191-204, 2000. © A K Peters

• Mizar Formalization of Concept Lattices
  in: Mechanized Mathematics and its Applications, vol. 1(1), pp. 1-10, 2000.

• The Evaluation of Multivariate Polynomials
  (with Andrzej Trybulec)
  in: Journal of Formalized Mathematics, vol.9(2), pp. 331-338, 2000.

• Mizar Correctness Proofs of Generic Fraction Field Artihmetic
  in: M. Jazayeri, R. Loos, D. Musser (eds.), Generic Programming --- International Seminar on Generic Programming,
  Dagstuhl Castle, Germany, Lecture Notes in Computer Science 1766, pp. 178-191, 2000. © Springer-Verlag

• A Characterization of Concept Lattices; Dual Concept Lattices
  in: Journal of Formalized Mathematics, vol.9(1), pp. 55-60, 1999.

• Noetherian Lattices
  in: Journal of Formalized Mathematics, vol.8(1), pp. 169-174, 1999.

• The Tecton Concept Library
  (with Rüdiger Loos, David Musser and Sybille Schupp)
  Technical Report WSI-99-02, Faculty for Computer Science, University of Tübingen, 1999.

• The Ring of Integers, Euclidean Rings and Modulo Integers
  in: Journal of Formalized Mathematics, vol.8(1), pp. 29-34, 1999.

• Introduction to Concept Lattices
  in: Journal of Formalized Mathematics, vol.7(2), pp. 233-242, 1998.

• The Field of Quotients over an Integral Domain
  in: Journal of Formalized Mathematics, vol.7(1), pp. 69-80, 1998.

• Mizar Verification of Generic Algebraic Algorithms
  PhD thesis, Wilhelm-Schickard-Institute for Computer Science, University of Tübingen, 1997.

• The Correctness of the Generic Algorithms of Brown and Henrici Concerning Addition and Multiplication in Fraction Fields
  in: Journal of Formalized Mathematics, vol.6(3), pp. 381-388, 1997.

• Using Mizar to Prove Generic Algebraic Algorithms Correct
  unpublished manuscript, 1997.

• On the Complexity of Computing Gröbner Bases in Monoid and Group Rings   (in German)
  Diploma Thesis, University of Kaiserslautern, 1995.

• On Convergent Representations of Monoids and Groups   (in German)
  Minor Thesis, University of Kaiserslautern, 1993.