From Proofs to Programs in the Minlog System - The Warshall Algorithm and Higman's Lemma

. The Warshall algorithm computing the transitive closure of a relation is extracted from a constructive proof that repetitions in a path can always be avoided. Secondly a nonconstructive proof of a special case of Higman's lemma is transformed into a constructive proof. From the latter an efficient program is extracted. Both examples are implemented in the interactive theorem prover Minlog developed at the University of Munich. 1. Introduction In this paper we discuss two examples of program extraction from proofs, implemented in the interactive theorem prover Minlog. The first example starts from a constructive proof of the following Proposition. For every two points j; k in the finite field of a given relation R we can either find a repetition-free R-path leading from j to k or else find that there is no such R-path. Given this proof, we can -- using Minlog -- extract a very short and readable program that corresponds to the Warshall algorithm. This is remarkable, since the nai..