 ## resolution

<hardware>

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

<logic>

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