Commit 5b2351bd authored by nipkow's avatar nipkow
Browse files

New entry Groebner_Bases

parent f34e6fe900de
......@@ -3646,3 +3646,19 @@ abstract =
reported in Stannett & Németi (2014) "Using Isabelle/HOL to verify
first-order relativity theory", Journal of Automated Reasoning 52(4),
pp. 361-378.
[Groebner_Bases]
title = Gröbner Bases Theory
author = Fabian Immler <http://www.in.tum.de/~immler/>, Alexander Maletzky <http://www.risc.jku.at/home/amaletzk>
date = 2016-05-02
topic = Mathematics/Algebra, Computer Science/Algorithms
abstract =
This formalization is concerned with the theory of Gröbner bases in
(commutative) multivariate polynomial rings over fields, originally
developed by Buchberger in his 1965 PhD thesis. Apart from the
statement and proof of the main theorem of the theory, the
formalization also implements Buchberger's algorithm for actually
computing Gröbner bases as a tail-recursive function, thus allowing to
effectively decide ideal membership in finitely generated polynomial
ideals. Furthermore, all functions can be executed on a concrete
representation of multivariate polynomials as association lists.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
chapter AFP
session Groebner_Bases (AFP) = HOL +
options [timeout = 600]
theories [document = false]
"../Abstract-Rewriting/Abstract_Rewriting"
"~~/src/HOL/Library/AList"
theories
"Poly_Lists"
document_files
"root.tex"
"root.bib"
@PhdThesis{Buchberger1965,
Title = {{Ein Algorithmus zum Auffinden der Basiselemente
des Restklassenringes nach einem nulldimensionalen Polynomideal (An Algorithm
for Finding the Basis Elements in the Residue Class Ring Modulo a Zero
Dimensional Polynomial Ideal)}},
Author = {Bruno Buchberger},
School = {Mathematical Institute, University of Innsbruck,
Austria},
Year = {1965},
Note = {English translation in \emph{Journal of Symbolic
Computation} 41(3--4):475--511, Special Issue on Logic, Mathematics, and
Computer Science: Interactions}
}
@Article{Buchberger1970,
Title = {{Ein algorithmisches Kriterium f\"ur die
L\"osbarkeit eines algebraischen Gleichungssystems (An Algorithmic Criterion for
the Solvability of an Algebraic System of Equations)}},
Author = {Bruno Buchberger},
Journal = {Aequationes Mathematicae},
Year = {1970},
Note = {(English translation in \emph{Gr\"obner Bases and
Applications (Proceedings of the International Conference ``33 Years of
Gr\"obner Bases'', 1998)}, London Mathematical Society Lecture Note Series 251,
Cambridge Univerity Press, 1998, pages 535--545)},
Pages = {374--383},
Publisher = {Birkh\"auser}
}
@InProceedings{Buchberger1979,
Title = {{A Criterion for Detecting Unnecessary Reductions
in the Construction of Gr\"obner Bases}},
Author = {Bruno Buchberger},
Booktitle = {{Symbolic and Algebraic Computation
(Proceedings of EUROSAM'79, Marseille, June 26-28)}},
Year = {1979},
Editor = {Edward W. Ng},
Pages = {3--21},
Publisher = {Springer},
Series = {Lecture Notes in Computer Science},
Volume = {72},
Doi = {10.1007/3-540-09519-5_52}
}
@inproceedings{Winkler1983,
title = {{A Criterion for Eliminating Unnecessary Reductions in the
Knuth-Bendix Algorithm}},
author = {Franz Winkler and Bruno Buchberger},
booktitle = {{Proceedings of Algebra and Logic in Computer Science,
Gy\H{o}r, Hungary}},
series = {Colloquia Mathematica Societatis Janos Bolyai},
volume = {42},
pages = {849--869},
publisher = {North Holland},
year = {1983},
editor = {J. Demetrovics and G. Katona and A. Salomaa},
url = {http://www.risc.jku.at/publications/download/risc_231/1983-09-00-A.pdf}
}
@Article{Robbiano1985,
Title = {{On the Theory of Graded Structures}},
Author = {Lorenzo Robbiano},
Journal = {Journal of Symbolic Computation},
Year = {1985},
Pages = {138--170},
Volume = {2},
Publisher = {Elsevier},
Doi = {10.1016/S0747-7171(86)80019-0}
}
@Book{Adams1994,
Title = {{An Introduction to Gr\"obner Bases}},
Author = {William W. Adams and Philippe Loustaunau},
Publisher = {American Mathematical Society},
Year = {1994},
Month = {July}
}
@InCollection{Buchberger1998a,
Title = {{Introduction to Gr\"obner Bases}},
Author = {Bruno Buchberger},
Editor = {Bruno Buchberger and Franz Winkler},
Publisher = {Cambridge University Press},
Year = {1998},
Series = {London Mathematical Society Lectures Notes
Series},
Number = {251},
Booktitle = {Gr\"obner Bases and Applications},
Pages = {3 - 31}
}
@Book{Kreuzer2000,
Title = {{Computational Commutative Algebra 1}},
Author = {Martin Kreuzer and Lorenzo Robbiano},
Publisher = {Springer-Verlag},
Year = {2000}
}
@article{Thery2001,
author = {Laurent Th\'ery},
title = {{A Machine-Checked Implementation of Buchberger's Algorithm}},
journal = {Journal of Automated Reasoning},
year = {2001},
volume = {26},
number = {2},
pages = {107--137},
publisher = {Springer},
doi = {10.1023/A:1026518331905}
}
@TechReport{Buchberger2003,
Title = {{Gr\"obner Rings in Theorema: A Case Study in Functors and Categories}},
Author = {Bruno Buchberger},
Institution = {Johannes Kepler University Linz, Spezialforschungsbereich F013},
Year = {2003},
Month = {November},
Number = {2003-49},
HowPublished = {SFB Report}
}
@inproceedings{Schwarzweller2006,
author = {Christoph Schwarzweller},
title = {{Gr\"obner Bases -- Theory Refinement in the Mizar System}},
booktitle = {Mathematical Knowledge Management (4th International Conference,
Bremen, Germany, July 15--17)},
year = {2006},
editor = {Michael Kohlhase},
volume = {3863},
series = {Lecture Notes in Artificial Intelligence},
pages = {299--314},
publisher = {Springer},
doi = {10.1007/11618027_20}
}
@INPROCEEDINGS{Chaieb2007,
author = {Amine Chaieb and Makarius Wenzel},
title = {{Context aware Calculation and Deduction: Ring Equalities via
{Gr\"obner Bases} in Isabelle}},
booktitle = {{Towards Mechanized Mathematical Assistants (Proceedings of
Calculemus'2007, Hagenberg, Austria, June 27--30)}},
year = {2007},
editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang
Windsteiger},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
volume = {4573},
pages = {27--39}
}
@article{Jorge2009,
author = {J. Santiago Jorge and Victor M. Guilas and Jose L. Freire},
title = {{Certifying properties of an efficient functional program for
computing Gr\"obner bases}},
journal = {Journal of Symbolic Computation},
year = {2009},
volume = {44},
pages = {571--582},
number = {5},
publisher = {Elsevier},
doi = {10.1016/j.jsc.2007.07.016}
}
@article{Medina-Bulo2010,
author = {Inmaculada Medina-Bulo and Francisco Palomo-Lozano and Jose-Luis
Ruiz-Reina},
title = {{A verified \textsc{Common Lisp} implementation of Buchberger's
algorithm in ACL2}},
journal = {Journal of Symbolic Computation},
year = {2010},
volume = {45},
pages = {96--123},
number = {1},
publisher = {Elsevier},
doi = {10.1016/j.jsc.2009.07.002}
}
@article{Sternagel2010,
author = {Christian Sternagel and Ren\'e Thiemann},
title = {{Executable Multivariate Polynomials}},
journal = {Archive of Formal Proofs},
year = {2010},
note = {\url{http://afp.sf.net/entries/Polynomials.shtml},
Formal proof development},
ISSN = {2150-914x}
}
@article{Sternagel2012,
author = {Christian Sternagel},
title = {{Well-Quasi-Orders}},
journal = {Archive of Formal Proofs},
year = {2012},
note = {\url{http://afp.sf.net/entries/Well_Quasi_Orders.shtml},
Formal proof development},
ISSN = {2150-914x}
}
@phdthesis{Maletzky2016b,
title = {{Computer-Assisted Exploration of Gr\"obner
Bases Theory in Theorema}},
author = {Alexander Maletzky},
school = {Research Institute for Symbolic Computation
(RISC), Johannes Kepler University Linz, Austria},
year = {2016},
month = {May},
note = {To appear}
}
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym,latexsym}
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
%\usepackage{amssymb}
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
%\usepackage{eurosym}
%for \<euro>
%\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
%\usepackage{eufrak}
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%\usepackage{textcomp}
%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
%\<currency>
% this should be the last package used
\usepackage{pdfsetup}
% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}
% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}
\begin{document}
\title{Gr\"obner Bases Theory}
\author{Fabian Immler and Alexander Maletzky\thanks{Supported by the Austrian
Science Fund (FWF): grant no. W1214-N15, project DK1}}
\maketitle
\begin{abstract}
This formalization is concerned with the theory of Gr\"obner bases in
(commutative) multivariate polynomial rings over fields, originally developed
by Buchberger in his 1965 PhD thesis. Apart from the statement and proof of the
main theorem of the theory, the formalization also implements Buchberger's
algorithm for actually computing Gr\"obner bases as a tail-recursive function,
thus allowing to effectively decide ideal membership in finitely generated
polynomial ideals. Furthermore, all functions can be executed on a concrete
representation of multivariate polynomials as association lists.
\end{abstract}
\tableofcontents
% sane default for proof documents
\parindent 0pt\parskip 0.5ex
\newpage
\section{Introduction}
The theory of Gr\"obner bases, invented by Buchberger in
\cite{Buchberger1965,Buchberger1970}, is ubiquitous in many areas of
computer algebra and beyond, as it allows to effectively solve a multitude of
interesting, non-trivial problems of polynomial ideal theory. Since its
invention in the mid-sixties, the theory has already seen a whole range of
extensions and generalizations, so the present formalization must be understood
as some kind of ``preliminary'' work that is merely about the most basic
concepts and results.
For further information about Gr\"obner bases theory one may consult the
introductory paper \cite{Buchberger1998a} or literally any book on
commutative/computer algebra, e.\,g. \cite{Adams1994,Kreuzer2000}.
\subsection{Related Work}
The theory of Gr\"obner bases has already been formalized in a couple of other
proof assistants, listed below in alphabetical order:
\begin{itemize}
\item ACL2 \cite{Medina-Bulo2010},
\item Coq \cite{Thery2001,Jorge2009},
\item Mizar \cite{Schwarzweller2006}, and
\item Theorema \cite{Buchberger2003,Maletzky2016b}.
\end{itemize}
Please note that this formalization must not be confused with the
\textit{algebra} proof method based on Gr\"obner bases \cite{Chaieb2007}, which
is a completely independent piece of work: our results could in principle be
used to formally prove the correctness and, to some extent, completeness of
said proof method.
\subsection{Future Work}
This formalization can be extended in several ways:
\begin{itemize}
\item \emph{Criteria} for avoiding useless reductions in Buchberger's
algorithm (i.\,e. function \textit{gb}) may be implemented, thus making the
algorithm much more efficient. See \cite{Buchberger1979} for details.
\item The degree-reverse-lexicographic term order might be added,
complementing the existing purely lexicographic and degree-lexicographic term
orders.
\item One could establish the connection to \emph{elimination theory},
exploiting the well-known \emph{elimination property} of Gr\"obner bases
w.\,r.\,t. certain term-orders (e.\,g. the purely lexicographic one). This
would allow one to effectively simplify (and even solve, in some sense)
systems of algebraic equations.
\end{itemize}
% generated text of all theories
\input{session}
% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
......@@ -99,6 +99,7 @@ GoedelGod
GPU_Kernel_PL
GraphMarkingIBP
Graph_Theory
Groebner_Bases
Group-Ring-Module
HRB-Slicing
Heard_Of
......
<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<table width="100%">
<tbody>
<tr>
<td width="20%" align="center" valign="top">
<!-- navigation -->
<!--#include file="nav.html"-->
</td>
<td width="80%" valign="top">
<!-- content -->
<div align="center">
<p>&nbsp;</p>
<h1><font class="first">G</font>röbner
<font class="first">B</font>ases
<font class="first">T</font>heory
</h1>
<p></p>
<table width="80%" class="data">
<tbody>
<tr><td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">Gröbner Bases Theory</td></tr>
<tr><td class="datahead">Author:</td>
<td class="data"><a href="http://www.in.tum.de/~immler/">Fabian Immler</a> and <a href="http://www.risc.jku.at/home/amaletzk">Alexander Maletzky</a></td></tr>
<tr><td class="datahead">Submission date:</td>
<td class="data">2016-05-02</td></tr>
<tr><td class="datahead" valign="top">Abstract:</td>
<td class="abstract">
This formalization is concerned with the theory of Gröbner bases in
(commutative) multivariate polynomial rings over fields, originally
developed by Buchberger in his 1965 PhD thesis. Apart from the
statement and proof of the main theorem of the theory, the
formalization also implements Buchberger's algorithm for actually
computing Gröbner bases as a tail-recursive function, thus allowing to
effectively decide ideal membership in finitely generated polynomial
ideals. Furthermore, all functions can be executed on a concrete
representation of multivariate polynomials as association lists.
</td></tr>
<tr><td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Groebner_Bases-AFP,
author = {Fabian Immler and Alexander Maletzky},
title = {Gröbner Bases Theory},
journal = {Archive of Formal Proofs},
month = may,
year = 2016,
note = {\url{http://isa-afp.org/entries/Groebner_Bases.shtml},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td></tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Abstract-Rewriting.shtml">Abstract-Rewriting</a></td></tr>
<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
<!---INCLUDE- file="devel-warning.shtml"-->
</tbody>
</table>
<p></p>
<!--#set var="name" value="Groebner_Bases" -->
<!--#set var="binfo" value="../browser_info/current/AFP/${name}" -->
<!--#set var="doc" value="${binfo}/document.pdf" -->
<!--#set var="outline" value="${binfo}/outline.pdf" -->
<!--#set var="browse" value="${binfo}/index.html" -->
<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="<!--#echo var="outline" -->">Proof outline</a><br>
<a href="<!--#echo var="doc" -->">Proof document</a>
</td>
<!-- link to README.hmtl if no document exists -->
</tr>
<tr>
<td class="links">
<a href="<!--#echo var="browse" -->">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="<!--#echo var="tar" -->">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None </td></tr>
</tbody>
</table>
<!-- entry data end -->
</td> </tr> </table>
</body>
</html>
......@@ -49,6 +49,14 @@ A <a href="devel.shtml">development version</a> of the archive is available as w
<td class="head">2016</td>
</tr>
<tr><td class="entry">
2016-05-02:
<a href="entries/Groebner_Bases.shtml">Gröbner Bases Theory</a>
<br>Author:
<a href="http://www.in.tum.de/~immler/">Fabian Immler</a> and
<a href="http://www.risc.jku.at/home/amaletzk">Alexander Maletzky</a>
</td></tr>
<tr><td class="entry">
2016-04-28:
<a href="entries/No_FTL_observers.shtml">No Faster-Than-Light Observers</a>
......
......@@ -88,6 +88,7 @@
<a href="entries/Imperative_Insertion_Sort.shtml">Imperative_Insertion_Sort</a> &nbsp;
<a href="entries/Formal_SSA.shtml">Formal_SSA</a> &nbsp;
<a href="entries/ROBDD.shtml">ROBDD</a> &nbsp;
<a href="entries/Groebner_Bases.shtml">Groebner_Bases</a> &nbsp;
<strong>Distributed:</strong>&nbsp;<a href="entries/DiskPaxos.shtml">DiskPaxos</a> &nbsp;
<a href="entries/GenClock.shtml">GenClock</a> &nbsp;
......@@ -346,6 +347,7 @@
<a href="entries/Algebraic_Numbers.shtml">Algebraic_Numbers</a> &nbsp;
<a href="entries/Polynomial_Interpolation.shtml">Polynomial_Interpolation</a> &nbsp;
<a href="entries/Polynomial_Factorization.shtml">Polynomial_Factorization</a> &nbsp;
<a href="entries/Groebner_Bases.shtml">Groebner_Bases</a> &nbsp;
</div>
<h3>Analysis</h3>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment