About Tseitin transformation in logical equations

The paper is devoted to the applications of Tseitin transformations in some propositional logics areas connected with the systems of logical equations. It is shown that Tseitin transformations of the system of logical equations do not change the number of its solutions and a bijection is pointed between the solutions of the system and its transformation result. Some results related to the usage of Tseitin transformations in obtaining bounds for the complexity of the propositional proof systems are given. By using Tseitin transformations, the simplest proofs of the NP-completeness problem for the solvability of a 2-degree logical equations system and of the $\#P$-completeness problem for counting the number of satisfying assignments for any Horne CNF are constructed too. By using Tseitin transformations, it is also shown that the ROBDD for any Boolean function given in a Horne CNF or in a CNF with 2-literal disjuncts may not be build for a polynomial time if $P\neq NP$.