On termination of functional symbol-free logic programs

The present article is devoted to the termination of logic programs, which do not use functional symbols ($FSF$ programs). A program $P$ is terminating with respect to a goal $G$, if the $SLD$-tree of $P$ and $G$ is finite. In general, $FSF$ programs are not terminating. A transformation is introduced, by which any $FSF$ program is transformed into another, not $FSF$ program, which is shown to be terminating with respect to the permitted goals of the original program. The program obtained via transformation and the original program are $\Delta$-equivalent.