Ebook: Edinburgh LCF: A Mechanised Logic of Computation

Edinburgh LCF is a computer system for doing formal proofs interactively. This book is both an introduction and a reference manual for the complete system (and its DECsystem-10 implementation). The acronym LCF stands for ''Logic for Computable Functions'' - a logic due to Dana Scott in which facts about recursively defined functions can be formulated and proved. The original system (developed at Stanford University) was a proof checker for this logic, based on the idea not of proving theorems automatically, but of using a number of commands to generate proofs interactively step by step. The emphasis then was on exploring the class of problems that could conveniently be represented in the logic, and on discovering the kinds of patterns of inference that arose when solving these problems. It was found that, by and large, the original logic was expressive enough, although a few useful extensions were suggested. However, the fixed repertoire of proof-generating commands often required long and very tedious interactions to generate quite simple proofs; furthermore these long interactions often consisted of frequent repetitions of essentially the same sequence of inferences.