Theory Exploration in Theorema: Recent Approaches to Gröbner Bases [TETRA-GB]

Project Lead

Project Duration

01/01/2017 - 30/04/2019

Project URL

Go to Website

Software

Theorema

A Mathematical Assistant System implemented in Mathematica

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. ...

MoreSoftware Website

Publications

2021

[Maletzky]

A generic and executable formalization of signature-based Gröbner basis algorithms

Alexander Maletzky

J. Symb. Comput. 106, pp. 23-47. 2021. Elsevier, ISSN 0747-7171. arXiv:2012.02239 [cs.SC], https://doi.org/10.1016/j.jsc.2020.12.001. [url]
[bib]
@article{RISC6225,
author = {Alexander Maletzky},
title = {{A generic and executable formalization of signature-based Gröbner basis algorithms}},
language = {english},
journal = {J. Symb. Comput.},
volume = {106},
pages = {23--47},
publisher = {Elsevier},
isbn_issn = {ISSN 0747-7171},
year = {2021},
note = {arXiv:2012.02239 [cs.SC], https://doi.org/10.1016/j.jsc.2020.12.001},
refereed = {yes},
length = {25},
url = {https://arxiv.org/abs/2012.02239}
}

2019

[Maletzky]

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

Gröbner Bases and Macaulay Matrices in Isabelle/HOL

A. Maletzky

RISC, JKU Linz. Technical report, 2019. Submitted to Formal Aspects of Computing. [pdf]
[bib]
@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}
}
[Maletzky]

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, Austria. ISSN 2791-4267 (online). June 2019. [pdf]
[bib]
@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 = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

2018

[Maletzky]

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

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

Gröbner Bases and Macaulay Matrices in Isabelle/HOL

A. Maletzky

RISC. Technical report, December 2018. [pdf]
[bib]
@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}
}
[Maletzky]

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

A. Maletzky

RISC. Technical report, September 2018. Submitted. [pdf]
[bib]
@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

[Maletzky]

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

Loading…