The OASys Resolution: Parallel Execution of Logic Programs
H.Sakelariou,
P. Kefalas, I.Vlahavas
Abstract: 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