Formal Theory and Algorithmics of Noncommutative Gröbner Bases [DK1]

Project Lead

Project Duration

01/10/2010 - 31/12/2017

Project URL

Project Website

Software

Publications

2017

Gröbner Bases Computation by Triangularizing Macaulay Matrices

Bruno Buchberger

Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases) 75, pp. 1-9. 2017. Mathematical Society of Japan, 0.
[bib]
@article{RISC5586,
author = {Bruno Buchberger},
title = {{Gröbner Bases Computation by Triangularizing Macaulay Matrices}},
language = {english},
journal = {Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases)},
volume = {75},
pages = {1--9},
publisher = {Mathematical Society of Japan},
isbn_issn = {0},
year = {2017},
refereed = {no},
length = {9}
}

Satisfiability Checking and Symbolic Computation

Abraham Erika , Abbott John , Becker Bernd , Bigatti Anna Maria , Brain Martin , Buchberger Bruno , Cimatti Alessandro , Davenport James , England Matthew , Fontaine Pascal , Forrest Stephen , Griggio Alberto , Kröning Daniel , Seiler Werner M. , Sturm

ACM Communications in Computer Algebra 50(4), pp. 145-147. 2017. 0.
[bib]
@article{RISC5587,
author = { Abraham Erika and Abbott John and Becker Bernd and Bigatti Anna Maria and Brain Martin and Buchberger Bruno and Cimatti Alessandro and Davenport James and England Matthew and Fontaine Pascal and Forrest Stephen and Griggio Alberto and Kröning Daniel and Seiler Werner M. and Sturm },
title = {{Satisfiability Checking and Symbolic Computation}},
language = {english},
journal = {ACM Communications in Computer Algebra},
volume = {50},
number = {4},
pages = {145--147},
isbn_issn = {0},
year = {2017},
refereed = {no},
length = {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]
[bib]
@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]
[bib]
@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]
[bib]
@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}
}

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]
[bib]
@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}
}

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]
[bib]
@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}
}

Gröbner Bases and Generalized Sylvester Matrices

Manuela Wiesinger-Widi

Johannes Kepler University Linz. PhD Thesis. 07 2015. [url]
[bib]
@phdthesis{RISC5170,
author = {Manuela Wiesinger-Widi},
title = {{Gröbner Bases and Generalized Sylvester Matrices}},
language = {english},
year = {2015},
month = {07},
translation = {0},
school = {Johannes Kepler University Linz},
length = {116},
url = {http://epub.jku.at/obvulihs/content/titleinfo/776913}
}

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]
[bib]
@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]
[bib]
@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}
}

Rational solutions and beyond

Winkler Franz

Southeast Asian Bulletin of Mathematics(38), pp. 153-162. 2014. 0129-2021.
[bib]
@article{RISC5103,
author = {Winkler Franz},
title = {{Rational solutions and beyond}},
language = {english},
journal = {Southeast Asian Bulletin of Mathematics},
number = {38},
pages = {153--162},
isbn_issn = {0129-2021},
year = {2014},
refereed = {yes},
length = {9}
}

Loading…