History of the Development of Logic Programming (http://logicprogramminghistory.wikicensored.info)

Carl Hewitt

MIT EECS (Emeritus)

Logic Programming can be broadly defined as “using logic to deduce computational steps from existing propositions” (although this is somewhat controversial). The focus of this paper is on the development of this idea. Consequently, it does not treat any other associated topics related to Logic Programming such as constraints, abduction, etc.

    The idea has a long development that went through many twists in which important questions turned out to have surprising answers including the following:

       Is computation reducible to logic?

       Are the laws of thought consistent?

Church’s Foundation of Logic

Arguably, Church’s Foundation of Logic was the first Logic Programming language [Church 1932, 1933]. It attempted to avoid the known logical paradoxes by using partial functions and disallowing proof by contradiction.

The system was very powerful and flexible.[i] Unfortunately, it was so powerful that it was inconsistent [Kleene and Rosser 1935][ii] and consequently the logic was removed leaving only the functional lambda calculus [Church 1941].

Logicist Programme

McCarthy [1958] proposed the Logicist Programme for Artificial Intelligence which included the Advice Taker with the following main features:

1.    There is a method of representing expressions in the computer. These expressions are defined recursively as follows: A class of entities called terms is defined and a term is an expression. A sequence of expressions is an expression. These expressions are represented in the machine by list structures [Newell and Simon 1957].

2.    Certain of these expressions may be regarded as declarative sentences in a certain logical system which will be analogous to a universal Post canonical system. The particular system chosen will depend on programming considerations but will probably have a single rule of inference which will combine substitution for variables with modus ponens. The purpose of the combination is to avoid choking the machine with special cases of general propositions already deduced.

3.    There is an immediate deduction routine which when given a set of premises will deduce a set of immediate conclusions. Initially, the immediate deduction routine will simply write down all one-step consequences of the premises. Later, this may be elaborated so that the routine will produce some other conclusions which may be of interest. However, this routine will not use semantic heuristics; i.e., heuristics which depend on the subject matter under discussion.

4.    The intelligence, if any, of the advice taker will not be embodied in the immediate deduction routine. This intelligence will be embodied in the procedures which choose the lists of premises to which the immediate deduction routine is to be applied. Of course, the program should never attempt to apply the immediate deduction routine simultaneously to the list of everything it knows. This would make the deduction routine take too long.

5.    The program is intended to operate cyclically as follows. The immediate deduction routine is applied to a list of premises and a list of individuals. Some of the conclusions have the form of imperative sentences. These are obeyed. Included in the set of imperatives which may be obeyed is the routine which deduces and obeys.

The above quotation shows that McCarthy originated many of the fundamental principles, methods and concerns of the Logicist Programme for AI. Fischer Black [1964] did early work implementing some of McCarthy's ideas.

However, McCarthy's definition of Logical Artificial Intelligence [September 1, 2007] states as its requirement: “What a program knows about the world in general, the facts of the specific situation in which it must act, and its goals are all represented by sentences of some mathematical logical language.” So the Logicist Programme must be regarded as distinct from Logic Programming because it does not require the logical deduction of computational steps.

Uniform Proof Procedures based on Resolution

John Alan Robinson [1965] developed a deduction method called resolution which was proposed as a uniform proof procedure for proving theorems which

1.   Converted everything to clausal form  Converting all information to clausal form is problematic because it hides the underlying structure of the information.

2.   and then used a method analogous to modus ponens to attempt to obtain a proof by contradiction by the adding clausal form of the negation of the theorem to be proved. Using resolution as the only rule of inference is problematical because it hides the underlying structure of proofs.  Also using proof by contradiction is problematical because the axiomatizations of all practical domains of knowledge are inconsistent in practice.  And proof by contradiction is not a sound rule of inference for inconsistent axiomatizations.

Its first use was in computer programs to prove mathematical theorems and in the synthesis of simple sequential programs from logical specifications. [Wos 1965; Green 1969; Waldinger and Lee 1969; Anderson and 1970; 1971, etc.]. However, in the resolution uniform proof procedure theorem proving paradigm, the use of procedural knowledge was considered to be “cheating” [Green 1969].

Procedural Embedding of Knowledge

The two major paradigms for constructing semantics software systems were procedural and logical. The procedural paradigm was epitomized by Lisp [McCarthy et. al. 1962] which featured recursive procedures that operated on list structures. The logical paradigm was epitomized by uniform resolution theorem provers [Robinson 1965].

Planner [Carl Hewitt 1969] was a kind of hybrid between the procedural and logical paradigms in that it featured a procedural interpretation of logical sentences in that an implication of the form (P implies Q) can be procedurally interpreted in the following ways [Hewitt 1969]:

Forward chaining

When assert P, assert Q

When assert not Q, assert not P

Backward chaining

When goal Q, goal P

When goal not P, goal not Q

Planner was the first programming language based on the pattern-directed invocation of procedural plans from assertions and goals. The development of Planner was inspired by the work of Karl Popper [1935, 1963], Frederic Fitch [1952], George Polya [1954], Allen Newell and Herbert Simon [1956], John McCarthy [1958, et. al. 1962], and Marvin Minsky [1958]. Planner represented a rejection of the resolution uniform proof procedure paradigm.

A subset called Micro-Planner was implemented by Gerry Sussman, Eugene Charniak and Terry Winograd. Micro-Planner was used in Winograd's natural-language understanding program SHRDLU [Winograd 1971], Eugene Charniak's story understanding work, work on legal reasoning [McCarty 1977], and some other projects. This generated a great deal of excitement in the field of AI. Being a hybrid language, Micro Planner had two different syntaxes, variable binding mechanisms, etc. So it lacked a certain degree of elegance. In fact, after Hewitt's lecture at IJCAI'71, Allen Newell rose from the audience to remark on the lack of elegance in the language!

Backtracking

Computers were expensive. They had only a single slow processor and their memories were very small by comparison with today. So Planner adopted the then common expedient of using backtracking [Golomb and Baumert 1965]. In this way it was possible to economize on the use of time and storage by working on and storing only one possibility at a time in exploring alternatives.

Control structure controversy

One implementation decision in Micro Planner had unfortunate consequences. Lisp had adopted the programming pun of identifying NIL, the empty list with logical false (at memory location 0) because testing for 0 was faster than anything else. Because of the pun, testing for NIL was extremely common in Lisp programs. The implementers of Micro Planner extended this pun also to use NIL as a signal to begin backtracking. In Micro Planner, it was common to write programs to perform some operation on every element of a list by using a loop to process the first element of a list, take the rest of the list, and then jump back to the top of the loop to test if the list was empty. If the list tested empty, then the program would go on to do other things. Such a program never made it to testing the empty list after processing all the elements because when the last element was processed and the rest of the list was taken, NIL was returned as a value. The Micro Planner interpreter took this as the signal to begin backtracking and began undoing all the work of processing the elements of the list! People were dumbfounded. [Fahlman 1973]

In this and several other ways, backtracking proved unwieldy helping to fuel the great control structure debate. Hewitt investigated some preliminary alternatives in his thesis. Using program schemas, Hewitt in collaboration with Mike Paterson proved that recursion is more powerful than iteration and parallelism more powerful than sequential recursion [Patterson and Hewitt 1970].

Hairy control structure

Peter Landin had introduced an even more powerful control structure using his J (for Jump) operator that could perform a nonlocal goto into the middle of a procedure invocation [Landin 1965]. In fact the J operator enabled a program to jump back into the middle of a procedure invocation even after it had already returned! Drew McDermott and Gerry Sussman called Landin's concept “Hairy Control Structure” and used it in the form of a nonlocal goto for the Conniver programming language [McDermott and Sussman 1972].

Pat Hayes [1974] remarked:

Their [Sussman and McDermott] solution, to give the user access to the implementation primitives of Planner, is however, something of a retrograde step (what are Conniver's semantics?), although pragmatically useful and important in the short term. A better solution is to give the user access to a meaningful set of primitive control abilities in an explicit representational scheme concerned with deductive control.

However, there was there germ of a good idea in Conniver; namely, using co-routines to computationally shift focus to another branch of investigation while keeping alive the one that has been left. Scott Fahlman used this capability of Conniver to good effect in his in his planning system for robot construction tasks [Fahlman 1973] to introduce a set of higher-level control/communications operations for its domain. However, the ability to jump back into the middle of procedure invocations didn’t seem to be what was needed as the foundation to solve the difficulties in communication that were a root cause of the control structure difficulties

Conniver was also useful in that it provoked further research into control structures for Planner-like languages.

 

Control structures are patterns of passing messages

In 1972 Alan Kay visited MIT and gave an inspiring lecture that explained some of his ideas for Smalltalk-72 building on the message-passing of Planner and Simula [Dahl and Nygaard 1967] as well as the Logo work of Seymour Papert with the “little person” model of computation used for teaching children to program (cf. [Whalley 2006]). However, the message passing of Smalltalk-72 was quite complex [Ingalls 1983]. Also, as presented by Kay, Smalltalk-72 (like Simula before it) was based on co-routines rather than true concurrency.

The Actor model [Hewitt, Bishop, and Steiger 1973] was a new model of computation that differed from previous models of computation in that it was inspired by the laws of physics. It took some time to develop programming methodologies for the Actor model. Hewitt reported

... we have found that we can do without the paraphernalia of "hairy control structure" (such as possibility lists, non-local gotos, and assignments of values to the internal variables of other procedures in CONNIVER.)... The conventions of ordinary message-passing seem to provide a better structured, more intuitive foundation for constructing the communication systems needed for expert problem-solving modules to cooperate effectively.

The Genesis of Prolog

Gerry Sussman and Seymour Papert visited Edinburgh spreading the news about Micro-Planner and SHRDLU casting doubt on the resolution uniform proof procedure approach that had been the mainstay of the Edinburgh Logicists. According to Maarten van Emden [2006]

The run-up to the workshop [Machine Intelligence 6 organized by Donald Michie in 2001] was enlivened by telegrams from Seymour Papert at MIT announcing on alternating days that he was (was not) coming to deliver his paper entitled "The Irrelevance of Resolution", a situation that caused Michie to mutter something about the relevance of irresolution. The upshot was that a student named Gerry Sussman appeared at the appointed time. It looked as if this was going to be his first talk outside MIT. His nervousness was compounded by the fact that he had been instructed to go into the very bastion of resolution theorem proving and tell the assembled experts how totally misguided they were in trying to get anything relevant to AI with their chosen approach.

    I had only the vaguest idea what all this was about. For me theorem proving was one of the things that some people (including Kowalski) did, and I was there for the programming. If Bob and I had anything in common, it was search. Accordingly I skipped the historic Sussman lecture and arrived late for the talk scheduled to come after Sussman's. Instead, I found an unknown gentleman lecturing from a seat in the audience in, what I thought a very English voice. It turned out that a taxi from the airport had delivered Seymour Papert after all, just in time for the end of Sussman's lecture, which was now being re-done properly by the man himself.

    The effect on the resolution people in Edinburgh of this frontal assault was traumatic. For nobody more so than for Bob Kowalski. Of course there was no shortage of counter objections, and the ad hoc creations of MIT were not a pretty sight. But the occasion hit hard because there was a sense that these barbarians had a point.

According to Donald MacKenzie,

Pat Hayes recalled the impact of a visit from Papert to Edinburgh, which had become the "heart of [[artificial intelligence's] Logicland," according to Papert's MIT colleague, Carl Hewitt.

Papert eloquently voiced his critique of the resolution approach dominant at Edinburgh, "and at least one person upped sticks and left because of Papert." [MacKenzie 2001 pg 82.]

Pat Hayes visited Stanford where he learned about Planner. When he returned to Edinburgh, he tried to influence his friend Bob Kowalski to take Planner into account in their joint work on automated theorem proving. Kowalski recalls that he was not convinced that Planner was so radically different from some existing resolution theorem-provers, such as SL resolution, which he had been developing with Donald Kuehner, and which was similar to Donald Loveland’s model elimination theorem-prover.

At the University of Edinburgh, Bruce Anderson implemented a subset of Micro-Planner called PICO-PLANNER [Anderson 1972] and Julian Davies [1973] implemented essentially all of Planner. The above developments generated tension among the Logicists at Edinburgh. These tensions were exacerbated when the UK Science Research Council commissioned Sir James Lighthill to write a report on the AI research situation. The resulting report [Lighthill 1973; McCarthy 1973] was highly critical although SHRDLU [Winograd 1971] was favorably mentioned. “Resolution theorem-proving was demoted from a hot topic to a relic of the misguided past. Bob [Kowalski] doggedly stuck to his faith in the potential of resolution theorem proving. He carefully studied Planner.” [Bruynooghe, Pereira, Sickmann, and van Emden 2004] Kowalski [1988] states “I can recall trying to convince Hewitt that Planner was similar to SL-resolution.” But Planner was invented for the purposes of the procedural embedding of knowledge and was a rejection of the resolution uniform proof procedure paradigm for proving theorems. Furthermore, Planner’s use of forward chaining reasoning did not fit within SL resolution. However, although pragmatically useful for interfacing with the underlying Lisp system, the syntax of Planner was not a pretty sight.

 

van Emden [2006] recalls

Kowalski's apparent research program narrowed to showing that the failings so far of resolution inference were not inherent in the basic mechanism. He took great pains to carefully study PLANNER and CONNIVER. And painful it was. One of the features of the MIT work was that it assumed the audience consisted of LISP programmers. For anybody outside this circle (Kowalski most definitely was not a LISP programmer), the flavour is repellent.

 

In an attempt to better understand the relationship between Winograd’s procedural use of Micro-Planner and resolution logic, Kowalski collaborated with Alain Colmerauer in Marseille in the summer of 1971 on the logical representation and parsing of formal grammars. Colmerauer and Roussel recalled their reaction to learning about Planner in the following way:

While attending an IJCAI convention in September ‘71 with Jean Trudel, we met Robert Kowalski again and heard a lecture by Terry Winograd on natural language processing. The fact that he did not use a unified formalism left us puzzled. It was at this time that we learned of the existence of Carl Hewitt’s programming language, Planner [Hewitt, 1969]. The lack of formalization of this language, our ignorance of Lisp and, above all, the fact that we were absolutely devoted to logic meant that this work had little influence on our later research. [Colmerauer and Roussel 1996]

Kowalski developed SLD resolution at Marseille in the summer of 1972, which he maintains provides a logical framework for the backward chaining of Micro-Planner. On the other hand, the direct procedural interpretation of implication originally developed for Planner [Hewitt 1969, 1971] provides a simpler logical framework for backward chaining.

When Kowalski wrote back to Edinburgh about his increasing insight on how logic could be used for programming, Pat Hayes felt that his ideas were being unfairly appropriated by Kowalski and complained to the head of their unit Bernard Meltzer. Feeling that he wasn’t getting satisfaction, Hayes wrote a paper for the proceedings of a summer school in Czechoslovakia in which he did not fully acknowledge the work of Kowalski [Hayes 1973]. In retaliation, Kowalski published a paper about his ideas for using logic as a programming language in which he only briefly alluded to the work by Hayes [Kowalski 1974]. Many years later Kowalski and Hayes patched things up, e.g., see [Kowalski 1988].

In the fall of 1972, Roussel implemented a language called Prolog (an abbreviation for "PROgrammation en LOGique” (French for programming in logic)). Prolog programs are generically of the following form (which is a special case of the backward-chaining in Planner):

When goal Q, goal P1 and ... and goal Pn

Prolog was basically a subset of Planner that restricted programs to clausal form using backward chaining and consequently had a simpler more uniform syntax. (But Prolog did not include the forward chaining of Planner.) Like Planner, Prolog provided the following:

o   An indexed data base of pattern-directed procedures and ground sentences.

o   The Unique Name Assumption, by means of which different names are assumed to refer to distinct entities, e.g., Peking and Beijing are assumed to be different.

Prolog implemented a number of non-logical computational primitives for input-output, etc. Like Planner, for the sake of efficiency, it used backtracking. Prolog also had non-logical computational primitives to control backtracking including the use of negation as failure. Negation As Failure is the assumption that that negation of a sentence holds if attempting to prove it fails. It is a form of the closed world assumption and could be used in Micro-Planner because its conditional statement could be used to catch failures. (A standing joke among skeptics of its use in Planner was that programs using Negation As Failure were based on the principle that “The less the robot knows, the more that it can prove!”) Prolog extended Planner by using unification (but not necessarily soundly because for efficiency reasons it omitted use of the “occurs” check).

Both SLD resolution and Prolog omitted a number of logical features of Micro-Planner including:

o   Pattern-directed invocation of procedural plans from assertions (i.e., “forward chaining”)

o   Logical negation, e.g., (not (human Socrates)).

 

A consequence of the above shortcuts and compromises was that Prolog, like Planner, lacked elegance. McCarthy [2000] noted “Micro-Planner was a rather unsystematic collection of tools, whereas Prolog relies almost entirely on one kind of Logic Programming, but the main idea is the same.”  Abelson and Sussman [1996] provided their version of the history as follows:

Logic programming has grown out of a long history of research in automatic theorem proving. Early theorem-proving programs could accomplish very little, because they exhaustively searched the space of possible proofs. The major breakthrough that made such a search plausible was the discovery in the early 1960s of the unification algorithm and the resolution principle (Robinson 1965). Resolution was used, for example, by Green and Raphael (1968) (see also Green 1969) as the basis for a deductive question-answering system. During most of this period, researchers concentrated on algorithms that are guaranteed to find a proof if one exists. Such algorithms were difficult to control and to direct toward a proof. Hewitt (1969) recognized the possibility of merging the control structure of a programming language with the operations of a logic-manipulation system…. At the same time that this was being done, Colmerauer, in Marseille, was developing rule-based systems for manipulating natural language (see Colmerauer et al. 1973). He invented a programming language called Prolog for representing those rules. Kowalski (1973; 1979), in Edinburgh, recognized that execution of a Prolog program could be interpreted as proving theorems (using a proof technique called linear Horn-clause resolution). The merging of the last two strands led to the logic-programming movement. Thus, in assigning credit for the development of logic programming, the French can point to Prolog's genesis at the University of Marseille, while the British can highlight the work at the University of Edinburgh. According to people at MIT, logic programming was developed by these groups in an attempt to figure out what Hewitt was talking about in his brilliant but impenetrable Ph.D. thesis. For a history of logic programming see Robinson 1983.

In summary, Prolog was basically a subset of Planner that restricted programs to clausal form using backward chaining.

 

In 1980, Drew McDermott gave his take on the situation as follows:

At about the time the [Planner-like] AI languages were dying here, several Europeans, notably Alain Colmerauer [Roussel 75] and Robert Kowalski [van Emden 76], rediscovered the procedural interpretation of deduction. This was embodied in a language called PROLOG (for PROgramming in LOGic") that seemed remarkably like PLANNER. Most Americans probably thought this was just the beginning of a delayed version of the events here, and expected disillusionment to set in fairly quickly.

This has not happened. PROLOG has attracted and held a user community that is as fanatically devoted as most Americans are to LISP.

Paraconsistent Logic Programming

Logic Programming can proceed even in the face of inconsistency, which is fortunate because consistency testing is recursively undecidable even in first order logic. Because of this difficulty, it is usually not known whether or not large theories of practical domains are consistent.

PrediCalc [Kassoff, Zen, Garg, and Genesereth 2005] is paraconsistent Constraint Logic Programming for spreadsheets. PrediCalc allows for inconsistency between the value assignments and the constraints. This approach differs from the traditional consistency-maintaining techniques [Orman 2001, Mayol and E. Teniente 1999]. In addition, PrediCalc shows the consequences of the value assignments, even when the assignments are inconsistent with the constraints. PrediCalc’s notion of consequence differs from current notions based on minimal repairs [Bertossi and Chomicki 2003].

Contexts were used to implement Fitch-style natural deduction (Fitch [1952]) in QA-4 [Rulifson, Derksen, and Waldinger 1973]. Contexts have the advantage that they can be used to modularize information so that it doesn’t have to be globally consistent.  However, the contexts of QA-4 had to be pushed and popped in a strictly hierarchical fashion. This limitation was removed in the viewpoint mechanism of Ether [Kornfeld and Hewitt 1981]. In order to prove a goal of the form V (P implies Q) for a viewpoint V, it is sufficient to create a new viewpoint V' that inherits from V, assert V’ P, and then prove V’ Q.

Controversies

There are a number of controversies involved in the history of logic programming including "What is logic programming?", "Is Logic Programming computationally universal?" and "Did Logic Programming contribute to the failure of the Japanese Fifth Generation Project (ICOT)?"

What is logic programming?

Kowalski recalls that

The term “logic programming” was first used at a workshop organized by Robert Kowalski at Imperial College London in 1976. It was subsequently used to describe the general area associated with the use of logic as a programming language, extending the procedural interpretation of Horn clauses with negation as failure, and their implementation in languages such as Prolog. This was followed by workshops of the same title in Debrecen Hungary in 1980, Syracuse University and Los Angeles in 1981. The First International Conference on Logic Programming (ICLP) was held in Marseille in 1982, followed by the Second ICLP in Uppsala in 1984.

The Association for Logic Programming (ALP) was founded in 1986 at the 3rd ICLP conference, held at Imperial College London, and was set up initially to organize ICLP and related conferences. The Journal of Logic Programming (JLP) was founded by Alan Robinson in 1984 and was eventually adopted as the official journal of the ALP. JLP was replaced as the official journal of the ALP in 2000 by the journal Theory and Practice of Logic Programming published by Cambridge University Press.

The ALP has provided the following Background statement:

Logic Programming was born circa 1972, presaged by related work by Ted Elcock, Cordell Green, Pat Hayes and Carl Hewitt on applying theorem proving to problem solving and to question-answering systems. It blossomed from Alan Robinson's seminal contribution, the Resolution Principle, all the way into a practical programming language with automated deduction at its core, through the vision and efforts of Alain Colmerauer and Bob Kowalski. Their work was followed up by the Pioneers of the field and many others, until it took strong hold in the academic community and became the basis of important scientific projects such as Fifth Generation Computing.

On the other hand, Hewitt et. al. have sought to use the term “logic programming” in the more general sense of this article, namely, "The logical deduction of computational steps." If the more general definition of Logic Programming (i.e. "the logical deduction of computational steps") is accepted, then the field has a very long history with contributions by Bruce Anderson, Bruce Baumgart, Fischer Black, Eugene Charniak, Alonzo Church, Alain Colmerauer, Julian Davies, Jan Derksen, Ted Elcock, Scott Fahlman, Richard Fikes, Frederick Fitch, Gerhard Gentzen, Cordell Green, Pat Hayes, Carl Hewitt, Robert Kowalski, Bill Kornfeld, Drew McDermott, Zohar Manna, John McCarthy, Nils Nilsson, Alan Robinson, Philippe Roussel, Jeff Rulifson, Earl Sacerdoti, Erik Sandewall, Gerry Sussman, Richard Waldinger, Terry Winograd, etc. It might seem that this is not so different from the [Kowalski 1999] definition for the MIT Encyclopedia of Cognitive Science:

Logic Programming is the use of logic to represent programs and of deduction to execute programs in logical form. To this end, many different forms of logic and many varieties of deduction have been investigated.

The inventors of Actors [Hewitt, Bishop, and Steiger 1973] intuitively knew from their inception that logical deduction was insufficient for concurrent programming and consequently that programming in logic was not computationally universal. Clinger [1981] developed the first denotational model of concurrency building on the work of [Greif 1975] and [Hewitt and Baker 1977]. The gauntlet was officially thrown in The Challenge of Open Systems [Hewitt 1985] to which [Kowalski 1988b] replied in Logic-Based Open Systems. This was followed up with Guarded Horn clause languages: are they deductive and logical? [Hewitt and Agha 1988] in the context of the Japanese Fifth Generation Project (see section below). All of this was against Kowalski who stated “Looking back on our early discoveries, I value most the discovery that computation could be subsumed by deduction.” [Kowalski 1988a]

Keith Clark, Alain Colmerauer, Pat Hayes, Robert Kowalski, Alan Robinson, Philippe Roussel, etc.  deserve a lot of credit for promoting the concept of logic programming and helping to build the logic programming community. And the traditions of this community should not be disrespected. At the same time, the term "logic programming" (like "functional programming") is highly descriptive and should mean something.  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 deduction of computational steps"

It seems that Kowalski is now trying to fuzz the definition of Logic Programming in order to avoid conclusions which would result from greater precision that he considers to be unflattering to Logic Programming, e.g., the conclusion that Logic Programming is not computationally universal (see section below).[iii] This is analogous to trying to fuzz the definition of computation to avoid Undecidability.

In summary, Kowalski's approach is to define Logic Programming in terms of the traditions of a community centered around the Association of Logic Programming building on the resolution uniform proof procedure paradigm for proving theorems. In contrast, the Hewitt et. al. approach is to reject the resolution uniform proof procedure paradigm and to define Logic Programming by a principled criterion, namely, “the logical deduction of computational steps”.

Is Computation Subsumed by Deduction?

Kowalski developed the thesis that “computation could be subsumed by deduction” [Kowalski 1988a] which he states was first proposed by Hayes [1973] in the form “Computation = controlled deduction.” [Kowalski 1979]. This thesis was also implicit in one interpretation of Cordell Green’s earlier work.

According to Hewitt et. al. and contrary to Kowalski and Hayes, computation in general cannot be subsumed by deduction and contrary to the quotation (above) attributed to Hayes computation in general is not controlled 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 deduced from prior information by mathematical logic alone. Therefore mathematical logic cannot implement concurrent computation in open systems.

In concrete terms for Actor systems, typically we cannot observe the details by which the arrival order of messages for an Actor is determined. Attempting to do so affects the results and can even push the indeterminacy elsewhere. Instead of observing the internals of arbitration processes of Actor computations, we await outcomes. Indeterminacy in arbiters produces indeterminacy in Actors. The reason that we await outcomes is that we have no alternative because of indeterminacy.

It is important to be clear about the basis for the published claim about the limitation of mathematical logic. The claim is that because of the indeterminacy of the physical basis of communication in the Actor model, that no kind of deductive mathematical logic can deduce future computational steps.

What does the mathematical theory of Actors have to say about this? A closed system is defined to be one which does not communicate with the outside. Actor model theory provides the means to characterize all the possible computations of a closed Actor system in terms of the Representation Theorem [Hewitt 2006]: The denotation DenoteS of an Actor system S represents all the possible behaviors of S as

DenoteS = i