АННОТАЦИЯ к статье Правильщикова П.А. «ДОКАЗАТЕЛЬСТВО ТЕОРЕМ С ПОМОЩЬЮ КВАНТОВОГО ГЕНЕРАТОРА ТЕСТОВ» В статье рассматривается проблема автоматического доказательства теорем с использованием такой модели вычислений как квантовый генератор тестов (КГТ), описание которого и приводится. Предложено использовать квантовый ускоритель, моделью которого является КГТ, для автоматического доказательства теорем. Показано, что автоматизация доказательства теорем является важным и неотъемлемым элементом верификации современных БИС и создания программных комплексов, к надѐжности которых предъявляются повышенные требования. Утверждается, что автоматическое доказательство теорем может быть сведено к решению задачи выполнимости некоторого логического уравнения.