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

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

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

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]
[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…