On optimization of monadic logic programs

The article is devoted to the optimization of monadic logic programs and goals (programs and goals, which do not use functional symbols of arity $\ > 1$ and use only predicate symbols of arity $1$). A program $P$ is terminating with respect to a goal $G$, if an SLD-tree of $P$ and $G$ is finite. In general, monadic programs are not terminating. Program and goal transformations are introduced, by which a monadic program $P$ and a variable-free monadic goal $G$ are transformed into $P^{\prime}$ and $G^{\prime}$, such that $P^{\prime}$ is terminating with respect to $G^{\prime}$ and $P \models G$, if and only if $P^{\prime}\models G^{\prime}$. Note that the transformed program $P^{\prime}$ is the same for all goals.