Механизм раскрытия кванторов по булевым переменным

Задача эквивалентных преобразований логических выражений с кванторами является массовой, когда инженер использует логические модели для решения практических задач; при этом инженеру приходится иметь дело с глубокой скобочной формой логических функций от большого числа переменных.
Приводится описание алгебраической системы раскрытия кванторов, в которой применен покомпонентный метод раскрытия, совмещенный с развитым блоком теорем эквивалентных преобразований не только на уровне переменных, но и на уровне логических функций; приводятся результаты программной реализации системы на примерах с большим числом переменных.

Статья представлена к публикации членом редколлегии: О. П. Кузнецов