Название: Proof Theory and Logic Programming: Computation as Proof SearchАвтор: Dale Miller
Издательство: Cambridge University Press
Год: 2026
Страниц: 335
Язык: английский
Формат: pdf (true), epub
Размер: 10.1 MB
This book offers a principled view of programming, showing how computation arises from logic. It explores different logical and proof-theoretic systems as foundations for programming, providing a deeper understanding for readers interested in the theoretical underpinnings of computation and the logic programming paradigm.
This book develops a modern perspective on logic programming by viewing computation as proof search, whereby 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 such as 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.
We establish a proof-theoretic foundation using Gentzen’s sequent calculus for logic programming languages based on first-order and higher-order classical, intuitionistic, and linear logics. This approach provides the basis for the well-known languages Prolog (employing first-order Horn clauses in classical logic) and λProlog (utilizing higher-order hereditary Harrop formulas in intuitionistic logic), as well as the linear logic programming languages Lolli and Forum. As we will illustrate, these increasingly expressive logic programming languages enable the logic programming paradigm to capture essential aspects of modular programming, higher-order programming, abstract data-types, state encapsulation, and concurrency.
This book assumes a basic understanding of the syntactic properties of first-order logic and the (simply typed) λ. -calculus as a prerequisite. While prior experience with formal proof representations (such as natural deduction and sequent calculus) is not required, it would be beneficial. We will occasionally include examples of logic programs, presented using the syntactic conventions of λProlog, to illustrate proof-theoretic concepts. Although familiarity with Prolog or λProlog may aid in understanding these examples, readers without such prior knowledge should still be able to follow them, as λProlog program elements correspond directly to formulas within the logics being discussed.
"An excellent exposition of proof search as a vehicle for realizing computations that, in the process, provides a novel view of structural proof theory through the prism of logic programming. Another strength is the presentation of linear logic and its use in modelling computational systems. Ideal for a graduate-level course on logic and its role in specification and programming." Gopalan Nadathur, University of Minnesota
"Proof Theory and Logic Programming: Computation as Proof Search by Dale Miller is a refreshing look at the role that logic, specifically proof theory, plays in the foundation of computation. The book takes the perspective of a less-traveled route of applications of proof theory to computation - through the lens of proof search, a systematic and disciplined approach for searching for proofs of logical propositions. The book assumes minimal prerequisites, which makes it accessible to novices and experts alike. Its comprehensive coverage of decades of work in the field should make this an excellent reference textbook." Alwen Tiu, The Australian National University
"This book is a clear and elegant journey through the connections between proof theory and programming. With a rigorous treatment of logic programming via sequent calculus and focused proof systems, Miller shows how logic can shape the way we think about computation without losing sight of practical relevance. Proof Theory and Logic Programming is a great resource for students, researchers, and anyone interested in exploring the theoretical foundations of logic-based programming languages." Elaine Pimentel, University College London
Скачать Proof Theory and Logic Programming: Computation as Proof Search