Computability in Europe 2006
Logical Approaches to Computational Barriers

Print current page  Print this page

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

Speaker: Georges Gonthier


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 Valid HTML 4.01! Valid CSS! eXTReMe Tracker hit counters by