Данная работа относится к исследованию применения автоматического доказательства теорем в решении задач фундаментальной математики. В ней описывается применение средств автоматического логического вывода в различных областях. Исследуются метод резолюций и стратегии оптимизации. Выбраны задачи из библиотеки TPTP. Программно реализованы алгоритмы стратегий и проведено тестирование на выбранных задачах. Даны рекомендации по использованию стратегий.