登入選單

返回Google圖書搜尋

Synthesis of Formal Specifications of Predicates

Marta FraňováLubomir Popelinsky

出版	Université de Paris-Sud, Centre d'Orsay, Laboratoire de Recherche en Informatique, 1993
URL	http://books.google.com.hk/books?id=UenFOAAACAAJ&hl=&source=gbs_api

註釋

Abstract: "The paper presents a method, Synthesis of formal specifications of predicates (SpecS), for finding non-recursive definitions of predicates from the initially given recursive ones. To the obtained non-recursive definition of a predicate one may then apply a method, such as Predicate Synthesis from formal specifications developed in Constructive Matching methodology, to construct another recursive definition of this predicate. SpecS may provide a more suitable definition than the initially given recursive one. In other words, this task is interesting for a user- independent automization of inductive theorem proving, since it enables to change the definitions given when they are unsuitable for handling by the theorem prover."