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)
Nearby terms:
Requirements Engineering « Research Systems, Inc. «
reserved memory « resolution » resolver »
Resource Access Control Facility » Resource
Description Framework
|