返回Google圖書搜尋

Direct, Dual and Contrapositive Proofs by Induction

出版	Linköping University, Department of Computer and Information Science, 1994
URL	http://books.google.com.hk/books?id=XQjhHAAACAAJ&hl=&source=gbs_api

註釋Abstract: "In the context of imperative programming several methods of inductive reasoning have been proposed. In [2] and [3], these methods are surveyed and systematized, and it is shown that all of these methods are equivalent in the sense that a lemma that works for any one method, immediately yields a lemma for any other. In this paper we transpose these results to a restricted class of constraint logic programs. The main result that follows from this investigation is the notion of a 'dual' program whose least fixpoint yields a lemma for proving the correctness of the 'direct' program."