九州大学理学部 3 号館 (箱崎) Room 3109, Faculty of Science, Kyushu University (Hakozaki).
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).
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.