Implementing Metamathematics as an Approach to Automatic Theorem Proving

Abstract

A simple but important algorithm used to support automated reasoning is called matching: given two terms it produces a substitution, if one exists, that maps the first term to the second. In this paper the matching algorithm is used to illustrate the approach to automating reasoning suggested in the title. In Section 3 the algorithm is derived and verified in the Nuprl proof development system following exactly an informal presentation of it in Section 2. The example serves to introduce a particular automated reasoning system, Nuprl, as well as the idea of deriving programs from constructive proofs. The treatment of this example also suggests how these systems can be soundly extended by the addition of constructive metatheorems about themselves to their libraries of results.