Logical Approaches to Computational Barriers

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 |