b'\n_START_ARTICLE_\nTseitin-transformatie\n_START_PARAGRAPH_\nIn de logica is de Tseitin-transformatie (ook Tseitin-afgeleide genoemd) een manier om een propositie in lineaire tijd om te zetten naar een vervulbaarheidsequivalente propositie in conjunctieve normaalvorm. De Tseitin-transformatie kan bijvoorbeeld worden gebruikt bij het DPLL-algoritme en resolutie, bewijstechnieken in automatische stellingbewijzers._NEWLINE_De Tseitin-transformatie is vernoemd naar G.S. Tseitin die het publiceerde in 1968.\n_START_SECTION_\nBelang\n_START_PARAGRAPH_\nMet behulp van de regels van De Morgan en distributiviteit kan elke propositie naar een equivalente propositie in conjunctieve normaalvorm worden omgezet. Hierbij is het echter mogelijk dat de lengte van de propositie exponentieel stijgt. Met de Tseitin-transformatie kan een propositie naar conjunctieve normaalvorm omgezet worden die slechts een bepaalde factor langer is dan de oorspronkelijke propositie, wat voor veel toepassingen een belangrijke eigenschap is. Hierbij verkijgt men echter geen equivalente propositie, maar slechts een vervulbaarheidsequivalente.\n_START_SECTION_\nOptimalisatie\n_START_PARAGRAPH_\nEr kunnen enkele optimalisaties uitgevoerd worden als subformules meerdere keren voorkomen, zoals bij . De CNF-clausulen die behoren bij de tweede subformule  kunnen weggelaten worden door de variabele die toegekend is aan de eerste subformule te hergebruiken. Uitgewerkt wordt dit:  wat vereenvoudigd kan worden tot . Deze formule kan vervolgens omgezet worden naar conjunctieve normaalvorm.'