Parallel algorithms for inference and researching of their effectiveness on computer systems

This article presents the results of research on cluster systems with multicore nodes to create a method and algorithm implementing parallel output in the proof of formulas in first order logic. The algorithm is based on the operative method of J. Robinson and the proposed procedure for its parallelization, which allows to dynamically control the uniform division of the set of resolvents distributed to the components of a computer system for infering. A number of heuristics are also introduced to significantly reduce the time to implement the decisions of the infering control. Experiments have shown that the effect on acceleration is higher than the previously studied parallel output algorithms.