Information Technology Reference
In-Depth Information
1.6 Automated Reasoning
Reasoning is the cognitive process of logically inferring a new judgment
(conclusion) from one or more already known judgments (precondition). It is the
reflection of the objective relationships in mind. People usually solve problems
based on prior knowledge and make conclusions through reasoning. Theories and
technologies of automated reasoning are important bases for research fields of
program derivation, proof of program correctness, expert systems, intelligent
robots, etc.
Early works of automated reasoning focused on automated theorem proving.
Pioneer work includes the Logic Theorist developed by Herbert Simon and Allen
Newell. In 1956, Alan Robinson proposed the Resolution Principle, making a
great progress in research on automated reasoning. The resolution principle is
easily applicable and logically complete, thus it becomes the computing model
for the logic programming language Prolog. Though some methods
outperforming the Resolution Principle in some aspects appeared later, e.g.
natural deductive reasoning and term rewriting systems, yet they are limited due
to the combination problem and the computational intractability essentially.
For a practical system, there always exist some non deductive cases. Thus,
various reasoning algorithms have been proposed, which even weakens the
attempt of finding a universal fundamental principle for AI. From the practical
perspective of view, each reasoning algorithm conforms to its specific, domain
related strategies based on different knowledge representation techniques. On the
other hand, it is undoubtedly useful to find a universal reasoning theory. In fact,
an important impetus for AI theoretical research is to find more general and
universal reasoning algorithms.
An important achievement of automated reasoning research is nonmonotonic
reasoning, a pseudo induction system. The so called nonmonotonic reasoning is
the reasoning process in which adding new positive axioms to the system may
invalidate some already proved theorems. Obviously, nonmonotonic reasoning is
more complex than monotonic reasoning. In nonmonotonic reasoning, first
hypotheses are made; then standard logical reasoning is carried out; if
inconsistence appeared, then backtrack to eliminate inconsistence, and establish
new hypothesis.
Raymond Reiter first set forth the closed world assumption (CWA) for
nonmonotonic reasoning in 1978 (Reiter, 1978), and proposed the Default
Reasoning (Reiter, 1980). In 1979, Jon Doyle developed the truth maintenance
