Back Satisfiability modulo theories English Teorías de satisfacibilidad módulo Spanish صدقپذیری در پیمانه نظریات Persian Kielégíthetőségi modulo elméletek Hungarian Բանաձևերի լուծելիություն տեսություններում Armenian Задача выполнимости формул в теориях Russian Satisfierbarhet modulo teorier Swedish Satisfiability Modulo Theories Ukrainian
Cet article ne cite pas suffisamment ses sources ().
Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références ».
En pratique : Quelles sources sont attendues ? Comment ajouter mes sources ?
En informatique et en logique mathématique, un problème de satisfiabilité modulo des théories[1] (SMT) est un problème de décision pour des formules de logique du premier ordre avec égalité (sans quantificateurs), combinées à des théories dans lesquelles sont exprimées certains symboles de prédicat et/ou certaines fonctions. Des exemples de théories incluent la théorie des nombres réels, la théorie de l’arithmétique linéaire, des théories de diverses structures de données comme les listes, les tableaux ou les tableaux de bits, ainsi que des combinaisons de celles-ci.
- ↑ (en) Barrett, Clark W and Sebastiani, Roberto and Seshia, Sanjit A and Tinelli, Cesare, « Satisfiability Modulo Theories. », Handbook of Satisfiability, , p. 825-885.