ON OPTIMIZATION OF MONADIC LOGIC PROGRAMS

Abstract

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{'}$ and $G{'}$, such that $P{'}$ is terminating with respect to $G{'}$ and $P\models G$ if and only if $P{'}\models G{'}$.  Note that the transformed program $P{'}$ is the same for all goals.