Talk announcement: Prof. Dr. Jasmin Blanchette

Wednesday, June 10, 18:00-19:00: Invited presentation 

Speaker: Prof. Dr. Jasmin Blanchette (Chair of Theoretical Computer Science, LMU München)

Title: Tao's Equational Proof Challenge Accepted

(Joint work with Lydia Kondylidou, LMU München, and Prof. Marijn J.H. Heule, CMU Pittsburgh)

In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover. We introduce a proof minimization tool called Krympa. Using a combination of brute force and heuristics, and exploiting both Vampire and the Twee equational prover, the tool reduces the 62-step proof to 20 steps, each corresponding to a rewrite. In an empirical evaluation, it also performs well on 1431 equational problems originating from the same project, reducing in particular a 151-step proof to only 10 steps.

There are two options for attending:

• in presence in room  WE5/05.017 (or WE5/05.003 if too small)
• online in Zoom at: https://uni-bamberg.zoom-x.de/j/66302997167

Meeting ID: 663 0299 7167
Passcode: AISE-SS26

Please send an email to christoph.benzmueller(at)uni-bamberg.de in case you want to attend in presence, so that I can plan for an appropriate room size.