Notes on resolution

  • J. A. Robinson
Conference paper
Part of the NATO ASI Series book series (volume 79)


These notes are a revised and extended version of [18]. They offer a brief but reasonably complete account of the main ideas underlying the resolution formulation of first order predicate logic, with computational issues receiving the lion’s share of attention. The unification algorithm is discussed in considerable detail, with logical formulas regarded simply as certain data structures. The aim is to explain resolution in general in such a way that the important special case of Horn clause resolution can be properly understood within the broader setting. Horn clause resolution is the theoretical framework for the kind of logic programming which is done by users of PROLOG. However, although many of the ideas we shall discuss are concretely realized in various versions of that programming language, we shall not be explicitly concerned with it. Surface details differ markedly from version to version and often obscure the relatively simple underlying conceptual system. We therefore try to present that system directly.


Assure Prefix 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Boyer, R.S. and Moore, J S. The sharing of structure in theorem proving programs. Machine Intelligence 7, Edinburgh University Press, 1972, 101–116.Google Scholar
  2. [2]
    Clark, K.L. Negation as failure. In Logic and Databases, edited by Gallaire and Minker, Plenum Press, 1978, 293–322.Google Scholar
  3. [3]
    Clark, K.L. Predicate logic as a computational formalism. Ph.D. Thesis, Imperial College, London, 1979.Google Scholar
  4. [4]
    Colmerauer, A., et al. Un systeme de communication homme-machine en francais. Groupe d’Intelligence Artificielle, U.E.R. de Luminy, Universite d’Aix-Marseille, Luminy, 1972.Google Scholar
  5. [5]
    Green, C.C. Application of theorem proving to problem solving. Proceedings of First IntemationalJointConference on Artificial Intelligence, Washington D.C., 1969, 219–239.Google Scholar
  6. [6]
    Hill, R. LUSH resolution and its completeness. DCL Memo 78, University of Edinburgh Department of Artificial Intelligence, August 1974.Google Scholar
  7. [7]
    Huet, G. Resolution d’equations dans les langages d’ordre 1, 2,...,ω. These d’Etat, Universite Paris VII (1976).Google Scholar
  8. [8]
    Kowalski, R.A. Predicate logic as programming language. Proceedings of IFIP Congress 1974, North Holland, 1974, 569–574.Google Scholar
  9. [9]
    Knuth, D. E. The Art of Computer Programming, Volume 1, Addison-Wesley 1969, 258–268.Google Scholar
  10. [10]
    Martelli, A. and Montanari, U. Unification in linear time and space. Technical Report B76–16, University of Pisa, Italy, 1976.Google Scholar
  11. [11]
    Paterson, M. S., and Wegman, M. N. Linear unification. Journal of Computer and Systems Sciences 16, 1978, 158–167.CrossRefMATHMathSciNetGoogle Scholar
  12. [12]
    Robinson, J. A. A machine-oriented logic based on the resolution principle. Journal of the Association for Comp[uting Machinery 12, 1965, 23–41.CrossRefMATHGoogle Scholar
  13. [13]
    Robinson, J. A. Automatic deduction with hyper-resolution. International Journal of Computer Mathematics 1, 1965, 227–234.MATHGoogle Scholar
  14. [14]
    Tarjan, R.E. Efficiency of a good but not linear set union algorithm. Journal of the Association for Computing Machinery 22, 1975, 215–225.CrossRefMATHMathSciNetGoogle Scholar
  15. [15]
    van Emden, M.H., and Kowalski, R.A. The semantics of predicate logic as a programming language. Journal of the Association for Computing Machinery 23, 1976, 733–742.CrossRefMATHMathSciNetGoogle Scholar
  16. [16]
    Vitter, J. S., and Simmons, R. A. New classes for parallel complexity: a study of unification and other complete problems for P. I.E.E.E. Transactions on Computers, Vol C-35, May 1986, 403–417.Google Scholar
  17. [17]
    Lloyd, J. W. Foundations of logic programming. Springer-Verlag, 1984. Second, extended edition, 1987.CrossRefMATHGoogle Scholar
  18. [18]
    Robinson, J. A. Notes on Logic Programming. Logic of Programming and Calculi of Discrete Design, Springer-Verlag, 1987, 109–144.Google Scholar
  19. [19]
    Robinson, J. A. Logic: form and function. Edinburgh University Press, 1979.MATHGoogle Scholar
  20. [20]
    Morris, F.L. On list structures and their use in the programming of unification. School of Computer and Information Science Report 4–78, Syracuse University, 1978.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • J. A. Robinson
    • 1
  1. 1.Syracuse UniversityUSA

Personalised recommendations