|
Proof Theory and Logic Programming: Computation as Proof Search I gave the final draft of this book to Cambridge University Press in Spring 2025. They should publish it in December 2025. Pre-ordering is possible. The most recent version of this book is available as a PDF: ptlp-2025-06-27.pdf (317 pages, 3.3 MB). Comments are welcome. |
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.
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.
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.
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.
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: 27 June 2025
