Why automated Reasoning?
Automated reasoning has many practical applications. For example,
it is useful in safety and security ritical applications where we
want to prove that some design meets its specification (the related
CoLogNet area of formal methods is thus an user of automated reasoning).
However, automated reasoning also has many other applications in
artificial intelligence in particular and computing in general.
For instance, many areas of decision support (like planning, scheduling,
routing, assignment) involve reasoning about constraints, resources,
goals, preferences, etc. In addition, automated reasoning can be
used to automate many parts of mathematics. Indeed, automated reasoning
tools have been used to prove a number of open results in mathematics
(like the 60 year old conjecture that all Robbins Algebras are Boolean).
http://www-unix.mcs.anl.gov/~mccune/papers/robbins/
A number of fundamental areas of computer science have "spun
out" of automated reasoning. For example, logic programming
came out of Colmerauer and Kowalski's work implementing Robinson's
resolution rule of inference.
Sponsored by:
