A mechanism of uncovering of quantifiers in boolean variables

The problem of equivalent transformations of logical expressions with quantifiers finds wide applications when the engineer uses logical models for the solution of practical problems; here the engineer has to deal with an extensive parenthesis form of logical functions of a large number of variables. In this paper, a description is given of an algebraic system of the uncovering of quantifiers, in which use is made of a componentwise uncovering method combined with a developed block of theorems of equivalent transformations not only at the level of variables, but also at the level of logical functions. Results of the program implementation of the system are set out in examples with a large number of variables.