(LMU Munich)

We overview the refined A-Translation method for uncovering thecomputational content in the classical proofs, thus enabling the extraction of

algorithms from them. We will briefly present the successful application of

A-Translation on the base case proof for Dickson's Lemma and then suggest a

generalisation of the lemma. This later part refers to work in progress, since

we aim at extensions of the conditions which the refined A-Translation imposes,

such that the method becomes applicable to a larger scale of proofs.

Board Room

Department of Computer Science