Abstract: Completeness of the inductive assertion method for logic programs is shown under an assumption that the assertion metalanguage of the method is expressive enough.
Abstract: We present an example of applying inductive assertion method of [Drabent, W. and Małuszyński, J. (1988). Inductive Assertion Method for Logic Programs. Theoretical Computer Science, 59:133-155]. 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.