返回Google圖書搜尋

Constructive Matching Methodology

其他書名	A Step Toward Creative Automated Inductive Theorem Proving
出版	Université de Paris-Sud. Centre d'Orsay. Laboratoire de Recherche en Informatique [LRI], 1991
URL	http://books.google.com.hk/books?id=vrZ1HAAACAAJ&hl=&source=gbs_api

註釋Abstract: "It is known that inductive theorem proving (ITP) provides a way to construct programs from formal specifications, thus creating objects which are specified implicitly only. In this paper we are not concerned by this kind of creativity. We are interested in the question: To which extent the ability of a mathematician for proving theorems by induction can be formalized and thus implemented? In our previous papers we have pointed out the importance of explanations in ITP and we have shown that our ITP methodology provides suitable explanations of its failures. By suitable explanations we mean here explanations that can be further analyzed with the goal of a recovery.