30 September 2023
VU scientists Visa Nummelin, Jasmin Blanchette (now mainly in Munich), and Sander Dahmen, from the Departments of Mathematics and Computer science, developed new methods to automatically prove summation identities. For their joint work, presented by Nummelin at the 14th International Symposium on Frontiers of Combining Systems, they received one of the two best paper awards.
Many problems in mathematics and computer science involve summations. In the paper, Recurrence-driven summations in automated deduction (published in the Springer series Lecture Notes in Artificial Intelligence) a new procedure is presented that automatically proves equations involving finite summations. It applies a delicate mix of techniques from computer science and mathematics. The procedure is designed to be interleaved with the activities of a higher-order automatic theorem prover and an implementation is underway. It should ultimately contribute to practical software tools that can automatically generate proofs for a very wide class of summation identities.