\input zb-basic
\input zb-ioport
\iteman{io-port 00096003}
\itemau{Sato, Taisuke}
\itemti{Equivalence-preserving first-order unfold/fold transformation systems.}
\itemso{Theor. Comput. Sci. 105, No.1, 57-84 (1992).}
\itemab
Summary: Two unfold/fold transformation systems for first-order programs, one basic and the other extended, are presented. The systems comprise an unfolding rule, a folding rule and a replacement rule. They are intended to work with a first-order theory $\Delta$ specifying the meaning of primitives, on top of which new relations are built by programs. They preserve the provability relationship $\Delta\cup \Gamma \vdash G$ between a call-consistent program $\Gamma$ and a goal formula $G$ such that $\Gamma$ is strict with respect to $G$. They also preserve the logical consequence relationship in three-valued logic.
\itemrv{~}
\itemcc{}
\itemut{logic programming; unfold/fold transformation systems; first-order programs; three-valued logic}
\itemli{doi:10.1016/0304-3975(92)90287-P}
\end