Some Termination Properties of Linear Completion

Using predicate logic as a programming language is a nice paradigm. But usual execution mechanisms (namely SLD and SLDNF resolutions) may lead to divergence when executing logic programs. To maintain a proper correspondence between logical semantics and operational semantics, a solution is to add some extra-mechanisms like loop-checks. There is an other known possibility to solve this problem. The idea is to consider logic programs as rewrite programs and to execute them with Linear Completion. This method is "semantics preserving" and has a nice behaviour with regard to termination. In this paper, we investigate some termination properties of Linear Completion : we prove that this mechanism is always terminating over specific classes of programs. These results show that the pruning effects of the simplification in Linear Completion give to this method the full power of the more efficient loop-checks in Logic Programming. Keywords : logic programming - rewrite programs - linear complet..