Resolution
Abstract
These notes form a brief but reasonably complete account of the ideas underlying resolution. We try to give equal emphasis not only to the logical principles involved but also to the computational issues which arise. We therefore study in some detail the most useful symbolic algorithms (in particular, since it is of greatest importance, the unification algorithm) and treat logical formulas explicity as carefully engineered data structures. One of our aims is to explain resolution in general in such a way that the importance 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. Indeed many of the ideas we shall discuss are concretely realized although not always in the purest form, in various versions of PROLOG. We shall not be concerned specifically with PROLOG, however, since the surface details often vary considerably from version to version and are often complex enough to hide the relatively simple conceptual system which lies just below the surface. (KR)
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1989
- Accession Number
- ADA213956
Entities
People
- J. A. Robinson