Adding New Rules to an LCF-style Logic
By encapsulating the primitive rules of inference as the constructors of
the abstract type of theorems, LCF-style systems provide a successful
answer to the problem of how to soundly add derived inference rules to a
theorem prover. We suggest a supplementary method which uses formal
proof of program equivalence to justify the dynamic addition of new
primitive rules. The method does not increase the strength of the logic;
rather, it is a means of increasing the computational strength of the
implementation. The method can be used to enforce rigour in the process
of iteratively improving the performance of a system. This work uses
first class environments, a recent addition to the SML/NJ compiler.
paper