Technical reports

• Drabent, W. (1988). On Completeness of the Inductive Assertion Method for Logic Programs. Unpublished note, Institute of Computer Science, Polish Academy of Sciences. Click here.

  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.

• Drabent, W. (1994). A Proof Using the Inductive Assertion Method. Unpublished report. (PDF)

  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.
  1994-11-24