## 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. 