Information Technology Reference
In-Depth Information
then asking if they entail some mathematical conjecture of interest. In 1996 an auto-
mated theorem-proving program written by William McCune and colleagues was able
to prove Robbins' Conjecture, a statement in algebra whose status had remained open
for sixty years.
All the reasoning in this topic comes out as a special case of first-order reasoning.
This means (in theory) leaving Prolog behind and continuing the work using a first-
order logic instead. Prolog is a conceptual ladder of great value, but now one can kick
the ladder away and explore along different paths.
