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 broad-based 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 logic-using 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:

1. X is mortal or X is not a human (i.e., if X is human, then X is mortal)
2. Socrates is a human

1. mortal(X) OR NOT human(X)
2. 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