返回Google圖書搜尋

Predicate Synthesis from Formal Specifications

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

註釋Abstract: "Predicate synthesis from examples (PreSE) becomes nowadays an acknowledged topic in Machine Learning (ML). Less known in ML (andin Artificial Intelligence as well), however, is predicate synthesis from formal specifications (PreS). The importance of PreS was pointed out by logicians (Skolem, Péter, ...) interested in recursive functions. It became clear that a false first order formula F of the form [for all] x A(x) may specify a predicate P such that [for all] x [P(x) => A(x)] is true, i.e., P describes the set S of all x for which A(x) is true. We say that F is a formal specification of P. Until now, automated construction of a definition of P for F has been partially tackled in program synthesis from incomplete specifications. However, as we illustrate in the paper, very often this approach succeeds to find a proper subset S' of S only. Therefore, a new method is necessary for PreS. In this paper we describe an algorithm and we show that this algorithm together with inductive theorem proving (ITP), i.e., proving theorems using mathematical induction principle can be considered as atool for PreS, because it provides a (recursive) definition of P. We will present also an application of PreS to simplifying proofs of implications, as well as an application of PreS to discovery of recursive calls which lead to synthesizing efficient programs."