Automatic theorem proving

Fig 1: HAL: artificial intelligence in the movies. 
The use of
logic
and automation for mathematical demonstrations is another field of application where AI has found success. Logic is certainly one of the most ancient, stable and rigorous instruments used to formalise and explain human reasoning. It is semantically well defined, highly declarative, and it has an extremely broadbased deductive apparatus. All this explains why classical logic (especially of the first order)
is used so much in AI to represent knowledge on a problem, even though
this choice does have evident limitations and does not enjoy unanimous
consensus. In this regard, Minsky states that logical formulae and deduction methods are not the most natural way of thinking, nor are they methods the human mind uses to organise his knowledge and to act with intelligent behavior. In this case the knowledge basis becomes a collection of statements of predicates of first order logics. Inference rules allow to deduce new statements (theorems) not explicitly contained in the starting knowledge basis. The sequence of inference rules used in the derivation of the theorem is called theorem proving.
Most of the logicusing programs in AI are based on studies of the automatic demonstration of logical theorems, and especially on the resolution method defined by J.A. Robinson in the
1960s and the development of strategies implemented to improve the efficacy of
demonstrations. The product of this study are also
programming in logic and
language called
Prolog (from PROgramming in LOGic), which is becoming one of the most interesting and innovative programming paradigms for the development of intelligent applications.
The following example shows a simple case of automatic proof (very similar to the ones produced in Prolog). We have to prove a well known syllogism: Socrates is mortal.
The knowledge base:
 X is mortal or X is not a human (i.e., if X is human, then X is mortal)
 Socrates is a human
More formally::
 mortal(X) OR NOT human(X)
 human(Socrates)
We prove the theorem by following the reductio ad absurdum: we suppose that Socrates is not mortal and we show that this leads to a contradiction.
The Webweavers: Last modified Wed, 09 Mar 2005 11:04:58 GMT
