Termination of Well-Typed Logic Programs

We consider an extended definition of well-typed programs to general logic programs, i.e. logic programs with negated literals in the body of the clauses. This is a quite large class of programs which properly includes all the well-moded ones. We study termination properties of well-typed general programs while employing the Prolog's left-to-right selection rule. We introduce the notion of typed acceptable program and provide an algebraic characterization for the class of well-typed programs whic hterminate on all well-typed queries.