A PROOF USING THE INDUCTIVE ASSERTION METHOD

W.\ Drabent, 1994-11-24

We present an example of applying inductive assertion method of
\cite{drm88}.  The method makes it possible to express and prove
run-time properties of logic programs.  Such properties are
inexpressible in terms of the declarative semantics.  We present
a proof of  Theorem 5.2 of [Apt, Pellegrini 1994, ACM ToPLaS, 16(3)].
concerning correctness of executing a program without occur-check.
Our proof is simpler than the original one due to using an
inductive assertion method.