ISSN 2071-8594

Российская академия наук

 

В.Н. Вагин, А.В. Деревянко, В.П. Кутепов "Алгоритмы параллельного логического вывода и исследование их эффективности на компьютерных системах"

Аннотация.

В статье приведены результаты исследования на кластерных системах с многоядерными узлами, созданных метода и алгоритма, реализующих параллельный вывод при доказательстве формул в логике первого порядка. Алгоритм основан на резолютивном методе вывода Дж. Робинсона и для его распараллеливания предложена процедура, позволяющая динамически управлять равномерным разделением множества резольвируемых дизъюнктов, распределяемых для вывода на узлы компьютерной системы. Также введен ряд эвристик, позволяющих существенно уменьшить время на реализацию управляющих решений. Экспериментами показано, что достигаемый эффект по ускорению выше, чем у ранее исследованных алгоритмов параллельного вывода.

Ключевые слова:

параллельный логический вывод, принцип резолюции, параллельные вычисления, логика.

Стр. 3-9.

Полная версия статьи в формате pdf.

REFERENCES

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.