Computability in Europe 2006
Logical Approaches to Computational Barriers


Special Session Talk:
Using reflection to prove the Four Colour Theorem


Speaker: Georges Gonthier

Abstract

In the context of mechanical theorem proving, reflection means using theorems
about symbolic representations. Despite its trivial logical underpinnings, the
generalised use of reflection has a deep impact on the practice of computer
proofs. Proof scripts, while not readable in the traditional sense, become more
stylised and organised. Paradoxically, while the average size of individual
proofs grows sharply, the global size of theories shrinks considerably. We will
describe the design principles of the scritpting language that supports this new
style of proof, and illustrate its use through examples drawn from the Four
Colour Theorem and the PoplMark benchmark.


websites: Arnold Beckmann 2006-04-28