Proof Theory and Logic Programming:
Computation as Proof Search

17 March 2025: I have given Cambridge University Press the final draft of the book Proof Theory and Logic Programming: Computation as Proof Search by Dale Miller. This book should be be published by CUP during Spring 2025. In addition to being published by CUP, I will also be able to post the PDF of the full book on my web pages. The most recent version of this book is available as ptlp-2025-03-17.pdf (317 pages). Comments are welcome.

Summary:

This book develops a modern perspective on logic programming by viewing computation-as-proof-search (where program execution is seen as the search for proof). It reveals how programs can be naturally and declaratively expressed as logical formulas and their execution as a systematic search for proofs within classical, intuitionistic, and linear logics. It employs sequent calculus as the essential tool for analyzing the operational reading of logic programs. It introduces and applies advanced techniques like focused proofs to expose the underlying mechanisms of goal-directed search and backchaining. A key feature is its in-depth coverage of higher-order quantification and its implications for logic programming. Beyond theory, the book explores practical applications, including encoding security protocols, specifying operational semantics, and static analysis of Horn clauses, demonstrating the versatility and power of this proof-theoretic approach.

Some key features of this book

• Computation as Proof Search: This book develops the idea that computation can be based on the search for proofs in various logical systems. This perspective offers a declarative understanding of programming, where the logic formulas themselves are the programs, and their execution is the process of finding proofs. This approach provides a principled and logical foundation for understanding how logic programs work. It moves away from purely operational descriptions and allows for reasoning about programs based on the properties of the underlying logic.
• A Spectrum of Logics for Programming
The book explores how different logics—namely, classical, intuitionistic, and linear logic, as well as first-order and higher-order versions—can be the foundation for designing logic programming languages. Many examples are provided that show how the choice of logic influences the expressiveness and operational behavior of the resulting programming language.
• Emphasis on Sequent Calculus and Focused Proofs
The book uses sequent calculus as the primary proof system for formalizing logic programming. In particular, it developed the notion of focused proof systems, which provide a structured approach to proof search by organizing inference rule applications into distinct phases. This use of sequent calculus and its focused variants provides concrete tools for analyzing the operational semantics of logic programs.
• Over 90 exercises are proposed in the text, with many given full or partial solutions.
The exercises are designed to help the reader explore definitions and proof techniques.

The cover artwork is by Nadia Miller (LinkedIn, ArtStation and WiX).

Last updated: 15 April 2025