九州大学理学部 3 号館 (箱崎) Room 3109, Faculty of Science, Kyushu University (Hakozaki).
Abstract
The method of Groebner bases allows to solve arbitrary nonlinear systems of
algebraic (polynomial) equations exactly. The method can be learned easily
by anybody who can do simple manipulations with polynomials, e.g. add and
multiply polynomials. In the talk we will, first, explain the method step
by step. Then we will give an overview on the surprisingly many
applications of the method that go far beyond systems solving. Although the
method is simple, the proof of its correctness is difficult. Thus, towards
the end of the talk, we will give some indication about the theory behind
the method. The talk will be accompanied by live demos.
The talk will also have two links to - but is not a prerequisite for - the
second talk of B. Buchberger on Tue, July 3: Groebner bases can also be
applied for the automated proof of geometrical theorems and a formal theory
of Groebner is a possible motivation for the Theorema software system.
九州大学理学部 1 号館 (箱崎) Room 1434, Faculty of Science, Kyushu University (Hakozaki).
Abstract
Formal mathematics, i.e. mathematics done on the basis of formal logic
systems, will soon become a practical reality. A couple of decades ago, the
motivation for formal mathematics mainly came from important foundational
questions about the consistency, correctness, completeness etc. of
mathematics but had hardly any practical impact. In contrast, in the
future, we believe that formal mathematics will be crucial for expanding
the relevance of mathematics as a practical tool at the basis of all
science and engineering. Formal mathematics is the condensed thinking
technology of the computer age.
In the talk we will present the Theorema software systems that aims at
providing a uniform logic and software technologic frame for future formal
mathematics. The Theorema system is currently being developed by the
speaker's Theorema Working Group. It is programmed in Mathematica and,
hence, is available on basically all platforms. The presentation will be
mainly done by providing live demo examples of formalizations of notions
and propositions in Theorema and of proofs automatically generated by the
system. The emphasis of the talk will be on the theory exploration paradigm
as opposed to the traditional isolated theorem proving paradigm.
http://www.math.kobe-u.ac.jp/seminars.html