Paper Info
Title
Predicate Synthesis from Formal Specifications: Using Mathematical Induction for Finding the Preconditions of Theorems
Abstract
Predicate synthesis from examples (PreSE) becomes nowadays an acknowledged topic in Machine Learning (ML). Less known in ML (and in 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 x A(x) may specify a predicate P such that 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 a tool 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.
Year
DOI
Venue
1991
10.1007/BFb0030394
Nonmonotonic and Inductive Logic
Keywords
Field
DocType
formal specifications,mathematical induction,predicate synthesis,theorem proving,formal specification,artificial intelligent,first order,machine learning
Discrete mathematics,Of the form,Program synthesis,First order,Mathematical induction,Formal specification,Predicate (grammar),Formal methods,Mathematics,Formal verification
Conference
ISBN
Citations 
PageRank 
3-540-56433-0
1
0.35
References 
Authors
10
2
Name
Order
Citations
PageRank
Marta Franová1225.53
Yves Kodratoff2581172.25