Invited Talks |

Auckland, New Zealand
In 1931 K. Gödel proved his famous incompleteness theorem which states that "no consistent axiomatic system whose theorems can be listed by an algorithm is capable of proving all true relations between natural numbers". In such a system one can effectively construct true statements that are unprovable (within the system). In 1936 A. Turing proved the undecidability of the halting problem, showing that "no algorithm can decide from a description of an arbitrary program and an input, whether the program will finish running or not". These negative results are intimately related and they form the basis of a largely accepted thesis that mathematics cannot be relegated to computers. The advent of powerful computers and proof assistants -- programs that assist the development of formal proofs by human-machine collaboration -- has revived the interest in formal proofs and diminished considerably the relevance of the above thesis for the working mathematician. In this talk we will discuss some relations between the incompleteness and undecidability problems in a formal framework, using for illustrations the generic proof assistant Isabelle.
Munich, Germany
Paper and pencil are no longer sufficient to obtain the predictions mandated by modern colliders. This is due to the required precision, the number of final-state particles, and also the number of particles in the model. More than any other collider, the LHC has to rely on precise theoretical predictions to even look in the right place, let alone test measurements at a quantitative level. The methods of perturbative quantum field theory, Feynman diagrams, have not changed much over time, and their application remains a formidable, though fully algorithmic, calculational problem. The talk focusses on how Computer Algebra plays an essential role in this programme and shows by a few examples how the methods are actually implemented in a Computer Algebra system. |