JavaScript is disabled for your browser. Some features of this site may not work without it.
Implementing Metamathematics as an Approach to Automatic Theorem Proving

Author
Constable, Robert L.; Howe, Douglas J.
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.
Date Issued
1989-04Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR89-982
Type
technical report