On termination of functional symbol-free logic programs

Статья посвящена проблеме завершимости логических программ, не использующих функциональные символы ($FSF$-программы). Программа $P$ считается завершаемой по отношению к запросу $G$, если $SLD$-дерево программы $P$ и запроса $G$ конечно. В общем случае $FSF$-программы незавершаемые. Описана трансформация, с помощью которой любая $FSF$-программа преобразовывается в другую не $FSF$-программу, и показано, что последняя является завершаемой по отношению к допустимым запросам первичной программы. Программа, полученная такой трансформацией, и первичная программа $\Delta$-эквивалентны.