ISSN 2071-8594

Russian academy of sciences


Gennady Osipov

V.N. Vagin, A.V. Derevyanko, V.P. Kutepov 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.


parallel inference, resolution principle, parallel computing, logic.

PP. 3-9


1. Vagin V.N., Golovina E.Iu., Zagorianskaia A.A., Fomina M.V. Dostovernyi i pravdopodobnyi vyvod v intellektual'nykh sistemakh Moscow, Fizmatlit, 2008. 712 p.
2. Chen, C., Li, R. Mathematical logic and automatic theorem proving Moscow, Nauka. 1983
3. Bonacina Maria Paola. A taxonomy of parallel strategies for deduction. AMAI. 2000. P. 1-36.
4. Kutepov V.P., Kumachev M. M. Parallel'nyy logicheskiy vyvod na komp'yuternykh sistemakh [Iskusstvennyy intellekt i prinyatiye resheniy] 2012, N2.
5. Vagin V.N., Kutepov V.P., Xotimcuk K. Iu. Parallel'nyy logicheskiy vyvod na mnogoyadernom komp'yutere [Vestnik Moskovskogo energeticheskogo instituta.] 2011. № 3. 82-87 p.
6. Zaretskiy D.S., Parallel'naya realizatsiya printsipa rezolyutsii s ispol'zovaniyem upravlyayushchikh evristik [Sbornik trudov mezhdunarodnoy superkomp'yuternoy konferentsii «Nauchnyy servis v seti Internet: superkomp'yuternyye tsentry i zadachi»], Novorossiysk, 2010. 611-618 p.