Resolution de contraintes du premier ordre dans des théories dites décomposables.

National audienceNous présentons dans ce papier un algorithme général pour la résolution de contraintes du premier ordre dans des théories dites décomposables. Tout d'abord, en utilisant des quantificateurs spéciaux, nous donnons une caractérisation formelle des théories décomposables et montrons quelques unes de leurs propriétés. Nous présentons en suite un algorithme général pour la résolution de contraintes du premier ordre dans une théorie décomposable T quelconque. L'algorithme est donné sous forme d'un ensemble de cinq règles de réécriture. Il transforme une formule !, qui bien entendu peut contenir des variables libres, en une conjonction " de formules résolues, équivalente dans T et ne faisant pas intervenir d'autre variables libres que celle de !. Cette conjonction de formules résolues soit est la formule vrai , soit est la formule ¬vrai , soit a au moins une variable libre. En particulier, si ! n'a pas de variables libres alors " est soit la formule vrai soit la formule ¬vrai . La correction de notre algorithme démontre la complétude des théories décomposables. Enfin, nous montrons que la théorie T des arbres finis ou infinis est une théorie décomposable et terminons par une série de benchmarks réalisées par une implantation de notre algorithme, résolvant des formules sur des jeux à deux partenaires dans T qui font intervenir des imbrications de plus de 160 quantificateurs alternés