This article generalises the refined A-translation method for extracting programs from classical proofs [U. Berger,W. Buchholz, H. Schwichtenberg, Refined program extraction from classical proofs, Annals of Pure and Applied Logic 114 3–25] to the scenario where additional assumptions such as choice principles are involved. In the case of choice principles, this is done by adding computational content to the ‘translated’ assumptions, an idea which goes back to [S. Berardi, M. Bezem, T. Coquand, On the computational content of the axiom of (...) choice, JSL 63 600–622] and has been further elaborated in [U. Berger, P. Oliva, Modified bar recursion and classical dependent choice, in: M. Baaz, S.D. Friedman, J. Kraijcek , Logic Colloquium ’01, in: Lecture Notes in Logic, vol. 20, Springer, Berlin, 2005, pp. 89–107]. We further investigate the applicability of this extension by means of a small but non-trivial example, and discuss the formalisation as well as some optimisations necessary in order to extract terminating programs. Both formalisation and term extraction have been implemented in the interactive proof assistant Minlog. (shrink)

This is a tutorial for the Minlog Proof Assistant, version 5.0.

This book bridges the gaps between logic, mathematics and computer science by delving into the theory of well-quasi orders, also known as wqos. This highly active branch of combinatorics is deeply rooted in and between many fields of mathematics and logic, including proof theory, commutative algebra, braid groups, graph theory, analytic combinatorics, theory of relations, reverse mathematics and subrecursive hierarchies. As a unifying concept for slick finiteness or termination proofs, wqos have been rediscovered in diverse contexts, and proven to be (...) extremely useful in computer science. The book introduces readers to the many facets of, and recent developments in, wqos through chapters contributed by scholars from various fields. As such, it offers a valuable asset for logicians, mathematicians and computer scientists, as well as scholars and students. (shrink)