Details

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

This article introduces a novel multiprocessing methodology tailored for the Inverse Method, a critical component of Automated Theorem Provers (ATPs), aimed at optimizing theorem proving efficiency. Our approach utilizes multiple running units, each operating as a distinct prover equipped with specific heuristic options, collaborating to explore conjectures and verify theorems. Central to our methodology is the integration of shared memory, enabling seamless communication and data exchange among the processing units, facilitating collaborative problem-solving. We delve into the implementation details of our multiprocessing prover, highlighting the incorporation of heuristic options customized to diverse problem domains and efficient memory sharing mechanisms for formulas. Through rigorous experimentation and benchmarking across various theorem proving tasks, we evaluate the performance and scalability of our approach.