# DI Dr. Alexander Maletzky

### Research Area

Gröbner Bases, Automated Reasoning, Theorema## Ongoing Projects

## Software

The present prototype version of the Theorema software system is implemented in Mathematica . The system consists of a general higher-order predicate logic prover and a collection of special provers that call each other depending on the particular proof situations. ...

## Publications

### 2019

### Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOL

#### A. Maletzky

In: Intelligent Computer Mathematics (Proceedings of CICM 2019, Prague, Czech Republic, July 8-12), Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti-Coen (ed.), Proceedings of CICM 2019, Lecture Notes in Computer Science , pp. ?-?. 2019. Springer, to appear. [pdf]**inproceedings**{RISC5919,

author = {A. Maletzky},

title = {{Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOL}},

booktitle = {{Intelligent Computer Mathematics (Proceedings of CICM 2019, Prague, Czech Republic, July 8-12)}},

language = {english},

series = {Lecture Notes in Computer Science},

pages = {?--?},

publisher = {Springer},

isbn_issn = {?},

year = {2019},

note = {to appear},

editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti-Coen},

refereed = {yes},

length = {16},

conferencename = {CICM 2019}

}

### Gröbner Bases and Macaulay Matrices in Isabelle/HOL

#### A. Maletzky

RISC, JKU Linz. Technical report, 2019. Submitted to Formal Aspects of Computing. [pdf]**techreport**{RISC5929,

author = {A. Maletzky},

title = {{Gröbner Bases and Macaulay Matrices in Isabelle/HOL}},

language = {english},

year = {2019},

note = {Submitted to Formal Aspects of Computing},

institution = {RISC, JKU Linz},

length = {14}

}

### Theorema-HOL: Classical Higher-Order Logic in Theorema

#### A. Maletzky

Technical report no. 19-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. June 2019. [pdf]**techreport**{RISC5930,

author = {A. Maletzky},

title = {{Theorema-HOL: Classical Higher-Order Logic in Theorema}},

language = {english},

number = {19-03},

year = {2019},

month = {June},

length = {24},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

### 2018

### Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL

#### A. Maletzky, F. Immler

In: Intelligent Computer Mathematics (Proceedings of CICM 2018, Hagenberg, Austria, August 13-17), Florian Rabe and William Farmer and Grant Passmore and Abdou Youssef (ed.), Proceedings of CICM 2018, Lecture Notes in Computer Science 11006, pp. 178-193. 2018. Springer, ISBN 978-3-319-96811-7. The final publication is available at Springer via https://doi.org/10.1007/978-3-319-96812-4_16. [url]**inproceedings**{RISC5733,

author = {A. Maletzky and F. Immler},

title = {{Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL}},

booktitle = {{Intelligent Computer Mathematics (Proceedings of CICM 2018, Hagenberg, Austria, August 13-17)}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {11006},

pages = {178--193},

publisher = {Springer},

isbn_issn = {ISBN 978-3-319-96811-7},

year = {2018},

note = {The final publication is available at Springer via https://doi.org/10.1007/978-3-319-96812-4_16},

editor = {Florian Rabe and William Farmer and Grant Passmore and Abdou Youssef},

refereed = {yes},

length = {16},

conferencename = {CICM 2018},

url = {https://doi.org/10.1007/978-3-319-96812-4_16}

}

### Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL (extended version)

#### A. Maletzky, F. Immler

RISC, JKU Linz. Technical report, May 2018. arXiv:1805.00304 [cs.LO]. [url]**techreport**{RISC5734,

author = {A. Maletzky and F. Immler},

title = {{Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL (extended version)}},

language = {english},

year = {2018},

month = {May},

note = {arXiv:1805.00304 [cs.LO]},

institution = {RISC, JKU Linz},

length = {28},

url = {https://arxiv.org/abs/1805.00304}

}

### Gröbner Bases and Macaulay Matrices in Isabelle/HOL

#### A. Maletzky

RISC. Technical report, December 2018. [pdf]**techreport**{RISC5814,

author = {A. Maletzky},

title = {{Gröbner Bases and Macaulay Matrices in Isabelle/HOL}},

language = {english},

year = {2018},

month = {December},

institution = {RISC},

length = {15}

}

### A Generic and Executable Formalization of Signature-Based Gröbner Basis Algorithms

#### A. Maletzky

RISC. Technical report, September 2018. Submitted. [pdf]**techreport**{RISC5815,

author = {A. Maletzky},

title = {{A Generic and Executable Formalization of Signature-Based Gröbner Basis Algorithms}},

language = {english},

year = {2018},

month = {September},

note = {Submitted},

institution = {RISC},

length = {31}

}

### 2017

### A New Reasoning Framework for Theorema 2.0

#### A. Maletzky

RISC, Johannes Kepler University Linz. Technical report, May 2017. Accepted as work-in-progress paper at CICM 2017 (10th Conference on Intelligent Computer Mathematics, Edinburgh, UK, July 17-21). [pdf]**techreport**{RISC5461,

author = {A. Maletzky},

title = {{A New Reasoning Framework for Theorema 2.0}},

language = {english},

year = {2017},

month = {May},

note = {Accepted as work-in-progress paper at CICM 2017 (10th Conference on Intelligent Computer Mathematics, Edinburgh, UK, July 17-21)},

institution = {RISC, Johannes Kepler University Linz},

length = {15}

}

### The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema

#### A. Maletzky, W. Windsteiger

In: Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, H. Geuvers, M. England, O. Hasan, F. Rabe, O. Teschke (ed.), Lecture Notes in Computer Science 10383, pp. 25-39. 2017. Springer, ISBN 978-3-319-62075-6. doi 10.1007/978-3-319-62075-6_3. [url] [pdf]**inproceedings**{RISC4536,

author = {A. Maletzky and W. Windsteiger},

title = {{The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema}},

booktitle = {{Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {10383},

pages = {25--39},

publisher = {Springer},

isbn_issn = {ISBN 978-3-319-62075-6},

year = {2017},

note = {doi 10.1007/978-3-319-62075-6_3},

editor = {H. Geuvers and M. England and O. Hasan and F. Rabe and O. Teschke},

refereed = {yes},

length = {15},

url = {https://link.springer.com/chapter/10.1007/978-3-319-62075-6_3}

}

### 2016

### Theorema 2.0: Computer-Assisted Natural-Style Mathematics

#### Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky, Wolfgang Windsteiger

JFR 9(1), pp. 149-185. 2016. ISSN 1972-5787. [url]**article**{RISC5243,

author = {Bruno Buchberger and Tudor Jebelean and Temur Kutsia and Alexander Maletzky and Wolfgang Windsteiger},

title = {{Theorema 2.0: Computer-Assisted Natural-Style Mathematics}},

language = {english},

abstract = {The Theorema project aims at the development of a computer assistant for the working mathematician. Support should be given throughout all phases of mathematical activity, from introducing new mathematical concepts by definitions or axioms, through first (computational) experiments, the formulation of theorems, their justification by an exact proof, the application of a theorem as an algorithm, until to the dissemination of the results in form of a mathematical publication, the build up of bigger libraries of certified mathematical content and the like. This ambitious project is exactly along the lines of the QED manifesto issued in 1994 (see e.g. http://www.cs.ru.nl/~freek/qed/qed.html) and it was initiated in the mid-1990s by Bruno Buchberger. The Theorema system is a computer implementation of the ideas behind the Theorema project. One focus lies on the natural style of system input (in form of definitions, theorems, algorithms, etc.), system output (mainly in form of mathematical proofs) and user interaction. Another focus is theory exploration, i.e. the development of large consistent mathematical theories in a formal frame, in contrast to just proving single isolated theorems. When using the Theorema system, a user should not have to follow a certain style of mathematics enforced by the system (e.g. basing all of mathematics on set theory or certain variants of type theory), rather should the system support the user in her preferred flavour of doing math. The new implementation of the system, which we refer to as Theorema 2.0, is open-source and available through GitHub.},

journal = {JFR},

volume = {9},

number = {1},

pages = {149--185},

isbn_issn = {ISSN 1972-5787},

year = {2016},

refereed = {yes},

keywords = {Mathematical assistant systems, Theorema, automated reasoning, theory exploration, unification},

length = {37},

url = {http://dx.doi.org/10.6092/issn.1972-5787/4568}

}

### Mathematical Theory Exploration in Theorema: Reduction Rings

#### A. Maletzky

In: Intelligent Computer Mathematics (Proceedings of CICM 2016, Bialystok, Poland, July 25-29), Michael Kohlhase, Moa Johansson, Bruce Miller, Leonardo de Moura, Frank Tompa (ed.), Proceedings of CICM 2016, Lecture Notes in Artificial Intelligence 9791, pp. 3-17. July 2016. Springer-Verlag, ISBN 978-3-319-42546-7. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-42547-4_1. Preprint on arXiv: 1602.04339 [cs.SC]. [url]**inproceedings**{RISC5265,

author = {A. Maletzky},

title = {{Mathematical Theory Exploration in Theorema: Reduction Rings}},

booktitle = {{Intelligent Computer Mathematics (Proceedings of CICM 2016, Bialystok, Poland, July 25--29)}},

language = {english},

series = {Lecture Notes in Artificial Intelligence},

volume = {9791},

pages = {3--17},

publisher = {Springer-Verlag},

isbn_issn = {ISBN 978-3-319-42546-7},

year = {2016},

month = {July},

note = {The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-42547-4_1. Preprint on arXiv: 1602.04339 [cs.SC]},

editor = {Michael Kohlhase and Moa Johansson and Bruce Miller and Leonardo de Moura and Frank Tompa},

refereed = {yes},

length = {15},

conferencename = {CICM 2016},

url = {http://dx.doi.org/10.1007/978-3-319-42547-4_1}

}

### Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0

#### A. Maletzky

In: Mathematical Software - ICMS 2016, Gert-Martin Greuel and Peter Paule and Andrew Sommese (ed.), Proceedings of 5th International Congress on Mathematical Software, Berlin, Germany, July 11-14, Lecture Notes in Computer Science 9725, pp. 59-66. 2016. Springer-Verlag, ISBN 978-3-319-42432-3. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-42432-3_8. [url] [pdf]**inproceedings**{RISC5282,

author = {A. Maletzky},

title = {{Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0}},

booktitle = {{Mathematical Software - ICMS 2016}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {9725},

pages = {59--66},

publisher = {Springer-Verlag},

isbn_issn = {ISBN 978-3-319-42432-3},

year = {2016},

note = {The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-42432-3_8},

editor = {Gert-Martin Greuel and Peter Paule and Andrew Sommese},

refereed = {yes},

length = {8},

conferencename = {5th International Congress on Mathematical Software, Berlin, Germany, July 11--14},

url = {http://dx.doi.org/10.1007/978-3-319-42432-3_8}

}

### Computer-Assisted Exploration of Gröbner Bases Theory in Theorema

#### A. Maletzky

Technical report no. 16-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. May 2016. PhD thesis. [pdf]**techreport**{RISC5291,

author = {A. Maletzky},

title = {{Computer-Assisted Exploration of Gröbner Bases Theory in Theorema}},

language = {english},

number = {16-04},

year = {2016},

month = {May},

note = {PhD thesis},

length = {197},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

### Computer-Assisted Exploration of Gröbner Bases Theory in Theorema

#### A. Maletzky

RISC, Johannes Kepler University Linz. PhD Thesis. May 2016.**phdthesis**{RISC5361,

author = {A. Maletzky},

title = {{Computer-Assisted Exploration of Gröbner Bases Theory in Theorema}},

language = {english},

year = {2016},

month = {May},

translation = {0},

school = {RISC, Johannes Kepler University Linz},

length = {197}

}

### 2015

### Automated Reasoning in Reduction Rings using the Theorema System

#### A. Maletzky

In: Computer Algebra in Scientific Computing, Vladimir P. Gerdt and Wolfram Koepf and Werner M. Seiler and Evgenii V. Vorozhtsov (ed.), Proceedings of CASC 2015 (September 14-18, Aachen, Germany), LNCS 9301, pp. 305-319. 2015. Springer-Verlag Berlin Heidelberg, ISSN 0302-9743. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-24021-3_23. [url] [pdf]**inproceedings**{RISC5151,

author = {A. Maletzky},

title = {{Automated Reasoning in Reduction Rings using the Theorema System}},

booktitle = {{Computer Algebra in Scientific Computing}},

language = {english},

series = {LNCS},

volume = {9301},

pages = {305--319},

publisher = {Springer-Verlag Berlin Heidelberg},

isbn_issn = {ISSN 0302-9743},

year = {2015},

note = {The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-24021-3_23},

editor = {Vladimir P. Gerdt and Wolfram Koepf and Werner M. Seiler and Evgenii V. Vorozhtsov},

refereed = {yes},

length = {15},

conferencename = {CASC 2015 (September 14-18, Aachen, Germany)},

url = {http://dx.doi.org/10.1007/978-3-319-24021-3_23}

}

### Exploring Reduction Ring Theory in Theorema

#### A. Maletzky

Technical report no. 15-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. July 2015. [pdf]**techreport**{RISC5162,

author = {A. Maletzky},

title = {{Exploring Reduction Ring Theory in Theorema}},

language = {english},

number = {15-11},

year = {2015},

month = {July},

length = {36},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

### Verifying Buchberger's Algorithm in Reduction Rings

#### A. Maletzky

In: Proceedings of the 4th International Seminar on Program Verification, Automated Debugging, and Symbolic Computation, Tudor Jebelean and Dongming Wang (ed.), Proceedings of PAS'2015, Beijing, China, October 21-23, pp. 16-23. October 2015. ??. arXiv:1604.08736 [cs.SC]. [url]**inproceedings**{RISC5283,

author = {A. Maletzky},

title = {{Verifying Buchberger's Algorithm in Reduction Rings}},

booktitle = {{Proceedings of the 4th International Seminar on Program Verification, Automated Debugging, and Symbolic Computation}},

language = {english},

pages = {16--23},

isbn_issn = {??},

year = {2015},

month = {October},

note = {arXiv:1604.08736 [cs.SC]},

editor = {Tudor Jebelean and Dongming Wang},

refereed = {yes},

length = {8},

conferencename = {PAS'2015, Beijing, China, October 21--23},

url = {http://arxiv.org/abs/1604.08736}

}

### 2014

### Complexity Analysis of the Bivariate Buchberger Algorithm in Theorema

#### A. Maletzky, B. Buchberger

In: Mathematical Software - ICMS 2014, Hoon Hong and Chee Yap (ed.), Proceedings of The 4th International Congress on Mathematical Software (ICMS'2014), Seoul, Korea, August 5-9, 2014, Lecture Notes in Computer Science 8592, pp. 41-48. 2014. Springer Berlin Heidelberg, ISBN 978-3-662-44198-5. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-44199-2_8. [url] [pdf]**inproceedings**{RISC4996,

author = {A. Maletzky and B. Buchberger},

title = {{Complexity Analysis of the Bivariate Buchberger Algorithm in Theorema}},

booktitle = {{Mathematical Software -- ICMS 2014}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {8592},

pages = {41--48},

publisher = {Springer Berlin Heidelberg},

isbn_issn = {ISBN 978-3-662-44198-5},

year = {2014},

annote = {2014-08-00-B},

note = {The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-44199-2_8},

editor = {Hoon Hong and Chee Yap},

refereed = {yes},

length = {8},

conferencename = {The 4th International Congress on Mathematical Software (ICMS'2014), Seoul, Korea, August 5-9, 2014},

url = {http://dx.doi.org/10.1007/978-3-662-44199-2_8}

}

### Groebner Bases in Theorema

#### B. Buchberger, A. Maletzky

In: Mathematical Software - ICMS 2014, Hoon Hong and Chee Yap (ed.), Proceedings of The 4th International Congress on Mathematical Software (ICMS'2014), Seoul, Korea, August 5-9, 2014, Lecture Notes in Computer Science 8592, pp. 374-381. 2014. Springer Berlin Heidelberg, ISBN 978-3-662-44198-5. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-44199-2_58. [url] [pdf]**inproceedings**{RISC4997,

author = {B. Buchberger and A. Maletzky},

title = {{Groebner Bases in Theorema}},

booktitle = {{Mathematical Software -- ICMS 2014}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {8592},

pages = {374--381},

publisher = {Springer Berlin Heidelberg},

isbn_issn = {ISBN 978-3-662-44198-5},

year = {2014},

annote = {2014-08-00-A},

note = {The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-44199-2_58},

editor = {Hoon Hong and Chee Yap},

refereed = {yes},

length = {8},

conferencename = {The 4th International Congress on Mathematical Software (ICMS'2014), Seoul, Korea, August 5-9, 2014},

url = {http://dx.doi.org/10.1007/978-3-662-44199-2_58}

}

### Complexity Analysis of the Bivariate Buchberger Algorithm in Theorema

#### A. Maletzky, B. Buchberger

Technical report no. 14-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. October 2014. [zip]**techreport**{RISC5063,

author = {A. Maletzky and B. Buchberger},

title = {{Complexity Analysis of the Bivariate Buchberger Algorithm in Theorema}},

language = {english},

number = {14-10},

year = {2014},

month = {October},

annote = {2014-10-00-A},

length = {0},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}