Алгоритмы параллельного логического вывода и исследование их эффективности на компьютерных системах

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