ARC : un ATMS basé sur la résolution CAT-correcte

La resolution CAT-correcte, definie dans le cadre de la logique propositionnelle, est une strategie de resolution autorisant l'inference de maniere efficace de clauses (CAT=clause a Antecedent Type) ne contenant que des donnees typees en partie antecedent. La resolution CAT-correcte peut etre utilisee dans un ATMS (Assumption-based Truth Maintenance System), dans la mesure ou la prise en compte des justifications est equivalente a la production de clauses a antecedent hypothese. ARC, un ATMS base sur la resolution CAT-correcte, garde les avantages d'un ATMS standard, tout en etendant ses fonctionnalites (generalisation des environnements, des nogoods et contextes)