Lambda the Ultimate

Resolution, Planner, Edinburgh LCF, Prolog, and the Japanese Fifth Generation Project arXiv:0904.3036

Logic Programming can be broadly defined as “using logic to infer computational steps from existing propositions” (although this has been opposed by Kowalski; see below). The focus of this article is on the middle period of the development of this idea from the advent of uniform proof procedures using resolution to the Japanese Fifth Generation Project.

Kowalski [1988] stated “Looking back on our early discoveries, I value most the discovery that computation could be subsumed by deduction.” According to Hewitt et. al. and contrary to Kowalski, computation in general cannot be subsumed by deduction. Hewitt and Agha [1991] and other published work argued that mathematical models of concurrency did not determine particular concurrent computations as follows: The Actor Model makes use of arbitration for determining which message is next in the arrival order of an Actor that is sent multiple messages concurrently. For example Arbiters can be used in the implementation of the arrival order of messages sent to an Actor which are subject to indeterminacy in their arrival order. Since arrival orders are in general indeterminate, they cannot be inferred from prior information by mathematical logic alone. Therefore mathematical logic cannot implement concurrent computation in open systems. Consequently, Procedural Embedding of Knowledge [Hewitt 1971] is strictly more general than Logic Programming.

Over the course of history, the term “functional programming” has grown more precise and technical as the field has matured. Logic Programming should be on a similar trajectory. Accordingly, “Logic Programming” should have a more precise characterization, e.g., “the logical inference of computational steps.” Kowalski's approach has been to advocate Logic Programming in terms of backward-chaining only inference building on the resolution uniform proof procedure paradigm for proving theorems. In contrast, our approach was to reject the resolution uniform proof procedure paradigm and to explore Logic Programming defined by a principled criterion, namely, “the logical inference of computational steps”.

Note: This article is about the middle history of Logic Programming. See ArXiv:0901.4934 for conceptual development of the role of Logic Programming from its origins to the present.