By

Martin Davis,
Dept. of Mathematics, University of California, Berkeley, CA and
Courant Institute of Mathematical Sciences, New York University, NY.

Eugenio Omodeo
DMG/DMI, Università di Trieste, Italy

Alan Robinson, whose highly influential method of resolution revolutionized efforts to create computer programs for finding proofs of valid formulas of first order logic, came to this field via a rather circuitous route. His dissertation in Philosophy at Princeton University in 1957 under Carl Hempel was entitled  Causation, Probability and Testimony and included discussion of the ideas of David Hume. It was only after working for DuPont as an operations analyst that he began his work on automated theorem proving at Argonne National Laboratory in the 1960s.

A number of people had already been working on proof procedures for first order logic at this time, and there were a number of computer implementations. The context in which Robinson worked was one in which a sentence whose validity was to be proved was presented in the form of its negation pre-processed into a conjunction of disjunctions of literals (i.e. atomic formulas and negations of such) as in the work of Davis-Putnam. The significance of unifying complementary literals had been emphasized in an influential paper by Dag Prawitz and developed further by Davis. (Jacques Herbrand had already called attention to this in his famous dissertation.)

In his very influential paper  A Machine Oriented Logic Based on the Resolution Principle, Robinson provided a succinct algorithm for “unifying” complementary literals. He introduced the operation of  resolution which eliminated complementary literals after they had been unified. And he proved that this operation alone could provide the basis for a complete proof procedure for first order logic. The elegance and simplicity of this made it very attractive, and it has been incorporated in many computer implementations to the present day. Robinson’s own effort to tame the combinatory explosion of bare resolution in his hyperresolution operation was certainly elegant, although much more in the way of heuristics was needed. Robinson was later much involved with the logic programming movement which attempted to make first order logic itself the basis for such programming languages as Prolog (he was the founding editor of the Journal of Logic Programming). His advocacy of logic programming extended to considering applying not only first order logic but also higher order logic as well.

Robinson’s many honors include a Guggenheim Foundation Fellowship, the American Mathematical Society Milestone Award in Automatic Theorem Proving, and the Herbrand Award for Distinguished Contributions to Automatic Reasoning. He has been awarded honorary doctorates from Katholieke Universiteit Leuven, Uppsala University, and Universidad Politécnica de Madrid.

Robinson died on 5 August 2016 at the age of 86.

 

BIBLIOGRAPHY

[1] J. A. Robinson. Causation, Probability and Testimony. PhD thesis, Princeton University, 1957.
[2] J. A. Robinson. Theorem-Proving on the Computer. J. ACM, 10(2):163-174, April 1963.
[3] J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. J. ACM, 12(1):23-41, January 1965.
[4] J. A. Robinson. Automatic Deduction with Hyper-Resolution. Int. J. Comput. Math., 1, 1965.
[5] J. A. Robinson. A review of automatic theorem-proving. Proc. Symp. Appl. Math., Amer. Math. Soc., Providence, R.I., 19:1-18, 1967.
[6] J. A. Robinson. The Generalized Resolution Principle. Machine Intelligence, 3:77-93, 1968.
[7] J. A. Robinson. A note on mechanizing higher-order logic. Machine Intelligence, 5:123-133, 1969.
[8] J. A. Robinson. Computational logic: the unification computation. Machine Intelligence, 6:63-72, 1971.
[9]  J. A. Robinson. Logic, Form and Function — The Mechanization of Deductive Reasoning. Edinburgh University Press, Scotland, 1979.
[10]  J. A. Robinson. Logic programming —Past, present and future—. New Generation Computing, 1(2):107–124, June 1983.
[11]  J. A. Robinson. Beyond LOGLISP: combining functional and relational programming in a reduction setting. Machine Intelligence, 11:57–68, 1988.
[12]  M. A. Arbib and J. A. Robinson. Introduction: Natural and Artificial Parallel Computation. In M. A. Arbib and J. A. Robinson, editors, Natural and Artificial Parallel Computation, pages 1–10. The MIT Press, Cambridge, MA, 1990.
[13]  J. A. Robinson. Logic and Logic Programming. Commun. ACM, 35(3):40–65, March 1992.
[14]  J. A. Robinson. Logic Computers, Turing, and von Neumann. Machine Intelligence, 13:1–35, 1994.
[15]  D. M. Gabbay, C. J. Hogger, J. A. Robinson, and J. Siekmann, editors.
Handbook of Logic in Artificial Intelligence and Logic Programming. Vol- ume 1. Logical Foundations. Clarendon Press, Oxford, 1993.
[16]  D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors. Handbook of Logic in Artificial Intelligence and Logic Programming. Volume 5. Logic Programming. Clarendon Press, Oxford, 1998.
[17]  A. Voronkov and J. A. Robinson, editors. Handbook of Automated Rea- soning. The MIT Press, 2001.