resolution

n 1: a formal expression by a meeting; agreed to by a vote [syn:

{declaration}, {resolve}]

2: the ability of a microscope or telescope to measure the

angular separation of images that are close together [syn:

{resolving power}]

3: the trait of being resolute; firmness of purpose; "his

resoluteness carried him through the battle"; "it was his

unshakeable resolution to finish the work" [syn: {resoluteness},

{firmness}, {resolve}] [ant: {irresoluteness}]

4: finding a solution to a problem [syn: {solving}]

5: something settled or resolved; the outcome of decision

making; "the finally reached a settlement with the union";

"they never did achieve a final resolution of their

differences" [syn: {settlement}]

6: analysis into clear-cut components [syn: {resolving}]

7: (computer science) the number of pixels per square inch on a

computer-generated display; the greater the resolution,

the better the picture

8: a dissonant chord is followed by a consonant chord

9: a statement that solves a problem or explains how to solve

the problem; "they were trying to find a peaceful

solution"; "the answers were in the back of the book"; "he

computed the result to four decimal places" [syn: {solution},

{answer}, {result}]

resolution

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.

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

See also {modus ponens}, {SLD Resolution}.

3. {address resolution}.

(1996-02-09)