返回Google圖書搜尋

A Constructive Proof for Prime Factorization Theorem

其他書名	A Result of Putting it Together in Constructive Matching Methodology
出版	Université de Paris-Sud. Centre d'Orsay. Laboratoire de Recherche en Informatique [LRI], 1992
URL	http://books.google.com.hk/books?id=KM8eHAAACAAJ&hl=&source=gbs_api

註釋Abstract: "Constructive Matching (CM) is a methodology developed to automate proving theorems by induction. It means that it describes problems, their links and proposes methods (deductive as well as inductive) to solve these problems. In other words, it provides a self-guidedcontrol over inductive proofs. CM is 'formally creative' in the sense that it really guides the process of proving a theorem. At any moment it knows what to do, it is able to discover missing knowledge, and to propose experiments. It is able to control proofs for non-trivialtheorems. If implemented on a parallel machine, in many cases, it may provide different proofs even starting from the same set of definitions.