Skip to main content
PRL Project

The Refiner as the Inference Mechanism of Nuprl Proof Development System

by Roderick Moten

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.