Personal tools
You are here: Home / Events / PhD Defence: Computer-Assisted Exploration of Gröbner Bases Theory in Theorema

PhD Defence: Computer-Assisted Exploration of Gröbner Bases Theory in Theorema

Filed under:
DI Alexander Maletzky (Doctoral Program, Johannes Kepler University Linz), 14 September 2016, 1:00 p.m., S3 058
When Sep 14, 2016
from 01:00 PM to 02:30 PM
Where S3 058
Add event to calendar vCal
iCal

In this thesis we present the formal, computer-supported exploration of the theory of Gröbner bases in the mathematical assistant system Theorema 2.0. The core component of the our formalization are so-called reduction rings, introduced by Buchberger more than 30 years ago, which generalize the original setting of Gröbner bases in polynomial rings over fields to a much wider class of algebraic structures, namely commutative rings with identity and a couple of further functions and relations, satisfying a handful of non-trivial axioms. We represented the main definitions, theorems and algorithms of this theory in Theorema and proved all results formally correct using the automated- and interactive reasoning capabilities of the system. Although the mathematical theories we considered in the frame of our studies are by no means novel, we nevertheless managed to contribute to them as well, by (drastically) simplifying one proof, generalizing various definitions and results, and, most importantly, detecting and correcting a subtle error related to reduction rings.