Alan Robinson

On August 5, 2016 John Alan Robinson died. In him, a great scientist departed, and I mourn a dear friend. His great discovery was the resolution principle in mathematical logic, a discovery that capped two decades of development. In its turn, it spawned a plethora of new developments in computer programming. It became important enough in Artificial Intelligence to become controversial.

A breakthrough in mathematical logic comes with a venerable pedigree. I remember reading about some pundit in the early 19th century reviewing the status of Aristotle’s contributions. Until the 16th century the teachings of Aristotle reigned supreme. Then the Copernican revolution demolished Aristotle’s cosmology. Galileo’s experiments and philosophy demolished Aristotle’s physics. The chemists had debunked Earth-Water-Air-Fire. Reviewing the wreckage, the pundit wondered whether anything survived. The answer was, yes, Aristotle’s logic had remained unassailed. Moreover there was no prospect of the new scientific method adding anything to it. Not surprising, the pundit concluded, because logic concerns nothing less than the laws of thought, and we moderns have no better access to these than Aristotle did.

It was ironic that around the same time Boole published The Laws of Thought [1]. This book not only added to Aristotle’s logic, but it also made further development less inconceivable. For example, although Aristotle and Boole made it possible to reason about Greekness and mortality, it was not clear how formal logic could help with statements such as “for every number there is one that is greater.” For an account of this next step I will follow Robinson’s own account [2] of the history of the field to which he made his contribution.

In 1879 Gottlob Frege published a booklet containing an exposition [3] of “Begriffsschrift”, a German neologism that translates to “concept writing”. Begriffsschrift was not only expressive enough for “for every number there exists one that is greater”, but had as goal nothing less than to analyze completely the formal structure of pure thought and to represent such analysis in a systematic and mathematically precise way. In acknowledging all these achievements we need to see through Frege’s idiosyncratic presentation of formulas, which he defends by the observation that the comfort of the typesetter is not the summum bonum. Whitehead and Russell steered the notation back to an algebraic style, as Boole had first done.

Frege’s work opened two lines of research: semantics and proof theory. Semantics inquired into the nature of the concepts themselves—it asks questions like “what is a number?” or “what is infinity?”, much debated around the turn of the century. This line led to Whitehead and Russell’s Principia Mathematica and to Zermelo’s axiomatic set theory. The proof-theoretical effects of Frege’s work led to formalization of processes of deduction, leading to what we now call “algorithms”.

As far as Robinson’s work is concerned we can restrict our attention to proof theory. In this line of research not much was happening between 1879 and the work of Löwenheim in 1915. This began a fruitful period of exploration culminating in the fundamental theorem of predicate calculus: the fact, which Frege took on faith, that his concept notation is a complete system, that it actually can do everything it was intended to do. The intention behind the predicate calculus was that it should provide a formal proof of every sentence in the language that is logically valid and that this proof should be systematically constructible, given the sentence. This was proved independently around 1930 by Kurt Gödel, Jacques Herbrand, and Thoralf Skolem. It is to these investigators that we owe today’s predicate calculus proof procedures.

Of course, in the 1930s no computers existed that could execute these proof procedures. In 1953 the mere existence of computers prompted a philosophy professor, Hao Wang, to start writing programs to prove theorems. Computers had struck him as conceptually elegant and a proper home for the obsessive formal precision that characterised mathematical logic, something that mathematicians find irrelevant, pedestrian, and an obstacle to creativity.

Probably the very first program was the one Davis wrote in 1954 to prove theorems in Presburger arithmetic. Other early work included Gilmore’s program implementing Beth tableaus and a new algorithm implemented in 1960 by Davis and Putnam. This early work launched the new area of Automated Theorem Proving, which attracted many new entrants by its novel combination of psychology (how do humans do it?), logic (to tell us what counts as a proof), mathematics (where to find things to be proved), and technology (how to get a computer to do the work).

Wang and the other pioneers found that the proof procedures of the 1930s contained steps that were seen as do-able “in principle”, which was all that was considered necessary. Only when computers were available, people were forced to reduce such steps to algorithms that could be executed by computers in a reasonable amount of time. A campaign of improvement started with Prawitz in 1960 and culminated in the mid-seventies.

This campaign naturally divides into two periods: pre-Robinson and post-Robinson. These periods are separated by Robinson’s “A machine-oriented logic” written in the summer of 1963 [4]. The pre-Robinson contributions of Prawitz and of Davis/Putnam concerned the avoidance of superfluous instantiations. This line of research was closed by Robinson’s resolution inference step which incorporated the unification algorithm with the property of yielding most general substitutions. This property implied that all superfluous instantiations had been avoided. “A machine-oriented logic” was published as [5]. It described resolution logic and gave the main results.

The elegance and simplicity of resolution logic allowed one to see a whole new vista of redundancies. This started the search for restrictions of resolution opportunities that would not compromise completeness of the resolution proof system. An early step in this direction was taken by Robinson himself. He called it hyperresolution and wrote the paper on it later in 1963. I quote from [4]:

During these same months [summer 1963], back at Rice [University], I wrote my paper on hyper-resolution, which appeared in 1964—a year before the resolution paper itself, which it presupposed! It turned out that the 1963 resolution paper had lain, waiting to be refereed, for almost a whole year at MIT. I gather Marvin Minsky had been asked by the JACM to referee it. It was indeed being discussed openly in his group and they had even written about it in their internal reports. The first I knew about all this was about a year after submitting the paper, when I received a phone call from Minsky to ask my permission to use it as one of the source materials in his AI seminar! I thought (and still think) that this long delay in refereeing the paper was very bad, and so did the Editor of the JACM, Richard Hamming. I complained to him, and he got on to Minsky, and my paper was finally returned to me with a request for some small revisions. I quickly sent Hamming a revised version, and it appeared in January 1965.

Robinson had started working in automated theorem-proving during a summer visit to the Argonne National Laboratory, where he built up a group for research in this area in the summer of 1961 and several subsequent summers. Though resolution logic was adopted by some workers in automated theorem-proving elsewhere, it remained one of several alternative methods. Its role in automated theorem-proving remained uneventful in comparison with the role resolution logic was to play in artificial intelligence. There it was embraced, then rejected, and went on to spawn the new research area that came to be called Logic Programming.

Of course the first to know about resolution logic was the Argonne group. Because of Hamming’s irregular choice of Minsky as referee for [5] (irregular because there were several reputable workers in automated theorem proving at the time), it became known at MIT.

The second escape of resolution logic beyond automated theorem proving came about as follows. Quoting Robinson [6]:

It was Cordell [Green] who was a very early adopter [of resolution logic]—in fact it was in late 1963 at Rice [University], in his final undergraduate year there, when resolution figured prominently in my lectures (in 1964 I thought and talked about little else!). I think Cordell probably thought of his QA idea [using resolution logic for a question-answering system] about that time. Off he went to Stanford in mid 1964 to join McCarthy and start his PhD program.

John McCarthy was Mr Artificial Intelligence himself: he had invented the term in 1956. In 1959 he published a paper [7] in which he proposed theorem proving by computer to implement an intelligent agent. This was very different from and independent of what the automated theorem proving people had in mind. The kind of theorem McCarthy had in mind was “I can get to the airport” to be inferred from a body of premisses including such as “I am at my desk” and “From my desk one can get to the airport”. Of course other premisses were needed. McCarthy was interested in what would constitute an adequate set.

In [8] and in his thesis [9] Green works out these ideas of McCarthy’s. He goes on to establish the beginnings of what has since become known as “logic programming”. However the state of resolution logic at the time of Green’s work prevented it from gaining the recognition it deserved. Two reactions were possible. The first was to conclude that the very idea of solving problems by resolution logic is flawed. This was the reaction of Minsky and his entourage at MIT. The second possible reaction was that the resolution logic needed further development.

This development indeed took place. Although resolution had eliminated vast swaths of redundancy in the earlier theorem provers, the simplicity and elegance of resolution revealed new sources of redundancy. Independently of Green’s work several workers had found this a worthwhile challenge [10]. Loveland and Luckham achieved improvement by the introduction of the linear format. Kowalski and Kuehner achieved further restriction (maintaining completeness) with the introduction of a selection function.

With Boyer and Moore, Kowalski studied the representation by logic clauses of formal grammars. In this way the special role of Horn clauses became apparent. Meanwhile in Marseille, France, Colmerauer and Roussel were writing a program for question-answering in natural language [13]. The program was based on a grammar formalism developed by Colmerauer under the name of Q-systems. Resolution had come to their attention via Jean Trudel, a Canadian student, in Marseille with a scholarship. The group invited Kowalski for a visit. He instructed them in SL-resolution and the fact that ancestor resolution is not needed for completeness when all clauses are Horn clauses. This was enough for Colmerauer and Roussel to produce a successor to Q-systems which had the attributes of a programming language, yet was an SL-theorem prover for Horn clauses. They called it Prolog, from programmation en logique, a name suggested by Roussel’s wife Jacqueline [11].

As Prolog and Kowalski’s work became widely known, the term “logic programming” was often confused. Kowalski [11] defines “logic programming” as

Logic programming shares with mechanical theorem proving the use of [resolution] logic to represent knowledge and the use of deduction to solve problems by deriving logical consequences. However, it differs from mechanical theorem proving in two distinct but complementary ways: (1) It exploits the fact that [resolution] logic can be used to express definitions of computable functions and procedures; and (2) it exploits the use of proof procedures that perform deductions in a goal-directed manner, to run such definitions as programs.

This emphasis on the use of resolution logic for knowledge representation makes logic programming into a paradigm within artificial intelligence. In spite of the antagonism from MIT, it has been acknowledged as such elsewhere.

Independently of logic programming, resolution logic has given rise to interesting developments in programming languages. The first and biggest step is represented by the very existence of Prolog as early as 1973. Kowalski described the use of resolution logic as a programming language [12] in a way that can be regarded as the essence of Prolog. To emphasize its status as a programming language it can be characterized as the most extreme procedure-oriented programming language, one where everything apart from the definition and calling of procedures has been stripped away. Iterative constructs have been omitted because iteration is the tail-recursive special case of procedure call. Branching has been omitted because it is a special case of non-determinism. Non-determinism does not need a specific operator: the procedure call can serve as such an operator in the presence of multiple procedure declarations. Finally, by using unification for the replacement of formal by actual parameters in procedure calls, assignment statements are rendered superfluous. Keith Clark showed how an analysis of unification leads to several modes of parallelism. With a succession of collaborators he implemented such variants of Prolog. For Colmerauer unification provided the starting point of what became known as constraint logic programming, also represented by variants of Prolog.

Thus Robinson’s discovery of resolution logic not only made an impact in its native land of automatic theorem-proving, but it also escaped its home to become a significant force in artificial intelligence and in programming languages.

Acknowledgements

My thanks to Paul McJones for his comments and suggestions for improvement.

References

[1] George Boole: An Investigation of the Laws of Thought on Which are Founded the Mathematical Theories of Logic and Probabilities. Macmillan, 1854.
[2] J.A. Robinson: “Logic programming—past, present and future”, New Generation Computing, vol. 1, 107-124. Ohmsha and Springer-Verlag, 1983.
[3] Gottlob Frege: Begriffsschrift, eine der Arithmetischen nachgebildete Formelsprache des reinen Denkens, Verlag von Louis Nebert, Halle, 1879. (Special thanks to Wikipedia for including a facsimile of the title page.)
[4] Letter of Robinson to Wolfgang Bibel approximately 2010.
[5] J.A. Robinson: “A machine-oriented logic based on the resolution principle”. Journal of the ACM, vol. 12, pp 23-41, 1965.
[6] Robinson, personal communication January 14, 2016.
[7] J. McCarthy: “Programs with common sense” in Proceedings of the Teddington conference on the mechanization of thought processes pp 75-91, Her Majesty’s Stationery Office, 1959.
[8] C. Cordell Green: “Application of theorem-proving to problem-solving”. In Proceedings IJCAI, pages 219–231, 1969.
[9] Cordell Green: “The Application of Theorem-Proving to Question-Answering Systems”. Technical Note no. 8, June 1969, Artificial Intelligence Group, Stanford Research Institute.
[10]. D.W. Loveland: “Automated Theorem Proving: a quarter-century review” in Contemporary Mathematics, vol. 29, pp 1–48, American Mathematical Society, 1984.
[11] R.A. Kowalski: “The early days of logic programming”. Comm. ACM, vol. 31(1988), pp 38–43.
[12] R.A. Kowalski: “Predicate logic as programming language”. Information Processing 74, 569–574. North Holland, 1974.
[13] Alain Colmerauer and Philippe Roussel: “The birth of Prolog”. SIGPLAN Notices vol.28 (1993), no. 3, pp. 1–31. Also: History of programming languages—II, pp 331–367, published by ACM, New York 1996.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s


%d bloggers like this: