In this thesis we present a methodology for the synthesis of function free definite logic programs from incomplete specifications, background knowledge and programming knowledge. The methodology is implemented as system SKILit and sub-systems SKIL and MONIC. The specification consists of positive and negative examples (ground atoms) of the predicate to synthesize, together with its input/output mode declaration. It can also include the predicate type declaration and integrity constraints. The background knowledge contains auxiliary predicates that may be used in the definition of the target predicate. Programming knowledge can be expressed in the form of a clause structure grammar that defines the structure of clauses to be synthesized in terms of admissible sequences of predicates. The user can also partially describe how some particular positive examples are computed. This information is given to the system in the form of sketches.

The construction of each clause is made by searching for a relational link between the input arguments and the output arguments of one positive example. Examples with or without associated sketches are handled in a uniform way using a unique sketch refinement operator. The sketch refinement operator of SKIL is shown to be complete under appropriate assumptions. Our methodology is capable of synthesizing recursive programs from small and sparse sets of positive examples using the technique of iterative induction. This is an important result considering that there is no strong language bias imposed (the technique is successful in synthesizing programs with multiple recursive clauses and clauses with multiple recursive literals). The methodology can also perform multiple predicate synthesis.

Due to its expressiveness, one integrity constraint can replace a large number of ground negative examples. Typically, constraint handling is computationally heavy. In our methodology, integrity constraints are handled using a Monte Carlo strategy (MONIC). Although incomplete, the Monte Carlo approach provides an efficient solution to constraint handling, which is very important in the context of program synthesis.

The whole synthesis methodology has been empirically evaluated in a systematic way showing that it is robust in the synthesis of recursive definitions from randomly generated examples and that it competes well with some state-of-the-art approaches.