The Refiner as the Inference Mechanism of Nuprl Proof Development System

by Roderick Moten
1994-1995

The refiner is the inference mechanism of the Nuprl proof development system. For several months I have been rewriting the refiner in SML from Lisp. Much of this effort has been spent writing an informal, but rigorous, specification for the refiner. In today's seminar, I will be giving a high level description of the design of the SML implementation of the refiner based on the specification. New and potential users of Nuprl may find this discussion as a helpful overview of Nuprl.

The Refiner as the Inference Mechanism of Nuprl Proof Development System

by Roderick Moten 1994-1995

by Roderick Moten
1994-1995