Notes on resolution
These notes are a revised and extended version of . 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.
Unable to display preview. Download preview PDF.
- 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
- Clark, K.L. Negation as failure. In Logic and Databases, edited by Gallaire and Minker, Plenum Press, 1978, 293–322.Google Scholar
- Clark, K.L. Predicate logic as a computational formalism. Ph.D. Thesis, Imperial College, London, 1979.Google Scholar
- 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
- 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
- Hill, R. LUSH resolution and its completeness. DCL Memo 78, University of Edinburgh Department of Artificial Intelligence, August 1974.Google Scholar
- Huet, G. Resolution d’equations dans les langages d’ordre 1, 2,...,ω. These d’Etat, Universite Paris VII (1976).Google Scholar
- Kowalski, R.A. Predicate logic as programming language. Proceedings of IFIP Congress 1974, North Holland, 1974, 569–574.Google Scholar
- Knuth, D. E. The Art of Computer Programming, Volume 1, Addison-Wesley 1969, 258–268.Google Scholar
- Martelli, A. and Montanari, U. Unification in linear time and space. Technical Report B76–16, University of Pisa, Italy, 1976.Google Scholar
- 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
- Robinson, J. A. Notes on Logic Programming. Logic of Programming and Calculi of Discrete Design, Springer-Verlag, 1987, 109–144.Google Scholar
- 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