resolution

        1. <hardware> the maximum number of pixels that can be
        displayed on a monitor, expressed as (number of horizontal
        pixels) x (number of vertical pixels), i.e., 1024x768.  The
        ratio of horizontal to vertical resolution is usually 4:3, the
        same as that of conventional television sets.

        2. <logic> A mechanical method for proving statements of
        first order logic, introduced by J. A. Robinson in 1965.
        Resolution is applied to two clauses in a sentence.  It
        eliminates, by unification, a literal that occurs
        "positive" in one and "negative" in the other to produce a new
        clause, the resolvent.

        For example, given the sentence:

        	(man(X) => mortal(X))  AND  man(socrates).

        The literal "man(X)" is "negative".  The literal
        "man(socrates)" could be considered to be on the right hand
        side of the degenerate implication

        	True => man(socrates)

        and is therefore "positive".  The two literals can be unified
        by the binding X = socrates.

        The truth table for the implication function is

        	A | B | A => B
        	--+---+-------
        	F | F |   T
        	F | T |   T
        	T | F |   F
        	T | T |   T

        (The implication only fails if its premise is true but its
        conclusion is false).  From this we can see that

        	A => B   ==   (NOT A) OR B

        Which is why the left hand side of the implication is said to
        be negative and the right positive.  The sentence above could
        thus be written

        	((NOT man(socrates)) OR mortal(socrates))
        	AND
        	man(socrates)

        Distributing the AND over the OR gives

        	((NOT man(socrates)) AND man(socrates))
        	OR
        	mortal(socrates) AND man(socrates)

        And since (NOT A) AND A == False, and False OR A == A we can
        simplify to just

        	mortal(socrates) AND man(socrates)

        So we have proved the new literal, mortal(socrates).

        Resolution with backtracking is the basic control mechanism
        of Prolog.

        See also modus ponens, SLD Resolution.

        3. <networking> address resolution.

        (1996-02-09)