Aller au contenu

Transformation de Tseitin

Un article de Wikipédia, l'encyclopédie libre.

En logique, la transformation de Tseitin prend un circuit logique et produit une formule booléenne équisatisfiable en forme normale conjonctive. La transformation est linéaire[1]. Elle a été développée par le mathématicien russe Grigori Tseitin.

Contexte[modifier | modifier le code]

Exemple[modifier | modifier le code]

Notes et références[modifier | modifier le code]

Grigori Tseitin est un mathématicien et informaticien russe.

  1. Tseitin, « On the complexity of derivations in the propositional calculus », Studies in Mathematics and Mathematical Logic, vol. Part II,‎ , p. 115–125 (lire en ligne, consulté le )