Robotics Reference
In-Depth Information
The Resolution Principle and Beyond
It is easy to see from the above description of the Logic Theory Machine
that when searching for a proof of a particular theorem, the process of
generating more and more intermediate theorems can easily get out of
hand. The British Museum Algorithm is the extreme example of this
syndrome. Researchers in this field have therefore attempted to reduce
the search space by means of various heuristic techniques. One very ef-
fective rule for achieving this is the Resolution Principle devised by Alan
Robinson in 1965. Put simply, this principle enables the elimination of
redundant and conflicting statements.
Although Alan Robinson's Resolution Principle achieved a certain
measure of success at improving the efficiency of the theorem-proving
process, researchers in the late 1960s and the 1970s were unable to de-
velop programs that could solve difficult problems or prove difficult the-
orems. For any non-trivial theorems the tree of intermediate expressions
was enormous and little success was achieved in finding powerful heuris-
tics to reduce the magnitude of the problem. It was also discovered that
purely deductive logic was not up to the task of solving many problems.
What
did
advance this particular niche within AI was the advent of com-
puters that were much more powerful and had much larger memories
than those used during the 1950s, 1960s and even the 1970s. The use
of faster, bigger computers has since enabled some notable successes in
automatic theorem proving, including one that has been of great interest
to mathematicians.
8
Problem Solving
Most of the early work on deduction by computer was focussed on au-
tomatic theorem proving, a highly specialized task that of itself is of
little interest outside the rather rarified world of higher mathematics.
But the real promise of this work, in terms of AI, a promise created by
the similarities between theorem proving and problem solving, was the
8
In 1996 there was an announcement from the Argonne National Laboratory in Illinois that
a famous open conjecture in mathematics had been proved by a theorem proving program called
EQP, developed by William McCune. The wording of the announcement from Argonne was “The
Robbins problem—are all Robbins Algebras Boolean?—has been solved: Every Robbins algebra is
Boolean.” In itself this statement may not engender much excitement in those who do not have the
benefit of a PhD in mathematics, but the fact that this conjecture had first been stated in the 1930s,
but had lain unproved for 60 years, was a great triumph for AI.
