The OASys Resolution: Parallel Execution of Logic Programs

H.Sakelariou, P. Kefalas, I.Vlahavas
This paper presents an alternative parallel refutation procedure for logic programs as an extension to the well known SLD-refutation procedure. The procedure is based on the OASys-resolution in which the substitutions produced by the unification of the goal atoms with the heads of program clauses can be postponed to the end of the resolution path. The aim of the refutation procedure, called OASys-refutation, is twofold: to allow parallel execution of unifications belonging to paths of the proof tree, giving in effect AND-parallel execution and to exploit OR-parallelism by assigning alternative resolution paths to different processing elements giving in effect OR-parallel execution. The overall effect is the full AND/OR parallel execution of logic programs in OASys, an abstract architecture and implementation for parallel Prolog. This work formally describes the OASys-resolution and proves its soundness and completeness.

Keywords:  Logic Programming, AND/OR-Parallelism, Unification, Resolution Algorithms

Submitted to: 2nd Panhellenic Logic Symposium

Available: Hardcopy on request from the authors. .

Back to Dept. of Computer Science, CITY Liberal Studies
Back to Petros Kefalas home page