Abstract FR:

Ce travail porte sur l'etude de mecanismes d'inference appropries a l'implementation d'un type de systemes de maintien de la coherence dans les bases de clauses introduit par j. De kleer: les atms. Faisant suite aux recherches de m. Cayrol et p. Tayrac, il apporte une semantique operationnelle au fonctionnement en chainage-avant de l'atms tel qu'il avait ete implemente dans le cadre de la logique propositionnelle, l'etendant a l'etude de bases infinies (logique des predicats). La calculabilite des processus est alors analysee. Partant de cette semantique et en inversant l'ordre d'execution du processus, un fonctionnement en chainage arriere est presente, debouchant sur l'ecriture d'un prouveur propositionnel. Un processus dit de reduction est ajoute a cet algorithme pour en ameliorer l'efficacite par la detection de coupures dans les arbres de deduction. De plus, l'information obtenue dans les cas d'echec de preuve est exploitee. On montre comment calculer grace a elle toutes les fonctionnalites usuelles des atms, plus certains concepts qui ne figurent pas dans l'arsenal classique de ces systemes. L'incrementalite, aspect indissociable des atms, est egalement traitee. Ce travail s'acheve sur la donnee des resultats d'implementation