Computability in Europe 2006
Logical Approaches to Computational Barriers

Special Session Talk:
New (un)decidability results from the formalization of mathematics

Speaker: John Harrison


Formalizing mathematics is challenging in several ways, and one difficulty in particular is often identified as the single greatest obstacle to its more widespread adoption. This is the problem of making a proof assistant understand in a reasonably automatic way many arguments that a human mathematician can quickly see to be valid. Although in recent years, mainstream proof assistants have acquired more powerful automation, they still require many low-level details that are generally ignored in human proofs. However, this very difficulty provides the motivation to search for new approaches to automation, including new logical decision procedures. In my talk I will give some examples of how, inspired by real formalization projects, new decidability results have been obtained. I will also describe how the attempt to delimit the scope of such results has led to some attractive undecidability results, apparently not hitherto considered in the logical literature.

websites: Arnold Beckmann 2008-05-14