Geodesic
About tseitin's transformation in logical equations
Prikladnaâ diskretnaâ matematika, no. 10 (2009), pp. 12-13 
A. A. Semenov. About tseitin's transformation in logical equations. Prikladnaâ diskretnaâ matematika, no. 10 (2009), pp. 12-13. http://geodesic.mathdoc.fr/item/PDM_2009_10_a4/
@article{PDM_2009_10_a4,
     author = {A. A. Semenov},
     title = {About tseitin's transformation in logical equations},
     journal = {Prikladna\^a diskretna\^a matematika},
     pages = {12--13},
     year = {2009},
     number = {10},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDM_2009_10_a4/}
}
TY  - JOUR
AU  - A. A. Semenov
TI  - About tseitin's transformation in logical equations
JO  - Prikladnaâ diskretnaâ matematika
PY  - 2009
SP  - 12
EP  - 13
IS  - 10
UR  - http://geodesic.mathdoc.fr/item/PDM_2009_10_a4/
LA  - ru
ID  - PDM_2009_10_a4
ER  - 
%0 Journal Article
%A A. A. Semenov
%T About tseitin's transformation in logical equations
%J Prikladnaâ diskretnaâ matematika
%D 2009
%P 12-13
%N 10
%U http://geodesic.mathdoc.fr/item/PDM_2009_10_a4/
%G ru
%F PDM_2009_10_a4

Voir la notice de l'article provenant de la source Math-Net.Ru

The report is supposed to touch upon a number of theoretical and applied issues of propositional logic. The issues share the common methodology which includes in its basis rather easy conversions of logical equations. Today science calls this kind of conversions ‘`Tseitin’s transformation’’.

[1] Tseitin G. S., “O slozhnosti vyvoda v ischislenii vyskazyvanii”, Zapiski nauchnykh seminarov LOMI AN SSSR, 8, 1968, 234–259

[2] Dantsin E. Ya., “Algoritmika zadachi vypolnimosti”, Voprosy kibernetiki. Problemy sokrascheniya perebora, AN SSSR, M., 1987, 7–29 | MR

[3] Waisberg M., “Untersuchungen uber den Aussagen kalkul von Heyting”, Wiadomosci Matematyczne, 46 (1938), 45–101

[4] Tseitin G., “On the complexity of derivation in propositional calculus”, Automat. Reasoning, 2 (1983), 466–483

[5] Plaisted D., Greenbaum S., “A Structure-preserving Clause Form Translation”, J. Symbolic Computation, 2 (1986), 293–304 | DOI | MR | Zbl

[6] Groote J. F., Zantema H., “Resolution and binary decision diagrams cannot simulate each other polynomially”, J. Discrete Appl. Mathematics, 130:2 (2003), 157–171 | DOI | MR | Zbl

[7] Een N., Sorensson N., “Translating Pseudo-Boolean Constraints into SAT”, J. Satisfiability, Boolean Modeling and Computation, 2006, no. 2, 1–25

[8] Semenov A. A., Zaikin O. S., Bespalov D. V., Ushakov A. A., “SAT-podkhod v kriptoanalize nekotorykh sistem potochnogo shifrovaniya”, Vychislitelnye tekhnologii, 13:6 (2008), 134–150