Abstract FR:

Le formalisme de representation de la connaissance considere est decompose en plusieurs sous-formalismes allant du cas horn propositionnel au cas plus general de la forme clausale du premier ordre. Sont presentes: 1) des moteurs d'inference pour une classe des systemes de regles exprimes en logique propositionnelle; 2) une methode de demonstration de theoremes en logique propositionnelle; 3) un algorithme d'unification des termes de premier ordre; 4) un schema de controle de l'inference en logique des predicats du premier ordre