У даній роботі описано підхід до автоматизованого пошуку доведень математичних теорем, особливістю якого є те, що пошук доведення здійснюється на базі цілісного математичного тексту, який записано формальною мовою першого порядку, близькою до мови математичних публікацій, що дає можливість використовувати формальні аналоги таких природних способів доведення як застосування означень понять та допоміжних тверджень у поєднанні з процедурами пошуку виводу у логічних численнях (а саме, з добре відомою процедурою негативної гіперрезолюції). Особливості підходу створюють можливість для оптимізації перебору при пошукові доведень математичних теорем.
