Logic and Computation

The book Logic and Computation presents a comprehensive study of techniques for formal theorem-proving, focusing particularly on Cambridge LCF (Logic for Computable Functions). It is designed for graduate students and researchers in the field of theoretical computer science, offering insights into the intersection of mathematical logic and computation. Cambridge LCF serves as a pivotal computer program that facilitates reasoning about computation, integrating methods from mathematical logic with domain theory, which underpins the denotational approach to understanding program statements.

Logic and Computation delves into the history and evolution of theorem-proving systems, tracing its roots back to Edinburgh LCF. This earlier system introduced a design framework that empowers users with the flexibility to utilize and expand upon the existing system. One of the primary objectives of the book is to elucidate this design, which has been influential in the development of various other theorem-proving systems.

The content of Logic and Computation is divided into two main parts. The first part outlines essential mathematical preliminaries, elementary logic, and domain theory, presenting these concepts at an intuitive level while providing references for more advanced studies. The second part offers detailed information that can serve as a reference manual for Cambridge LCF, making it a valuable resource for those implementing other programs based on the LCF methodology.