Nesta disseratção apresentamos uma metodologia para a síntese de programas lógicos definidos sem functores a partir de especificações incompletas, conhecimento de fundo e conhecimento de programação. A metodologia foi implementada no sistema SKILit e nos sub-sistemas SKIL e MONIC. A especificação consiste em exemplos positivos e negativos (átomos fechados) e na declaração de entrada/saída do predicado a sintetizar. Pode também incluir a declaração de tipo do predicado e restrições de integridade. O conecimento de fundo contém predicados auxiliares que podem ser utilizados na definição do predicado pretendido. O conhecimento de programação pode ser expresso sob a forma de uma gramática de estrutura clausal. Esta define a estrutura das cláusulas a sintetizar em termos de sequências amissíveis de predicados. O utilizador pode também descrever parcialmente a computação de determinados exemplos positivos. Esta informação é dada ao sistema através de esboços.

A contrução de cada cláusula é feita procurando uma ligação relacional entre os argumentos de entrada e os argumentos de saída de um exemplo positivo. Os exemplos são tratados de maneira uniforme quer tenham ou não um esboço associado. Mostra-se que o operador de refinamento do SKIL é completo sob os pressupostos adequados. A nossa metodologia é capaz de sintetizar programas recursivos a partir de conjuntos pequenos e esparsos de exemplos positivos usando a técnica da indução iterativa. Este é um resultado importante considerando que não são impostas fortes condições sintáticas aos programas (a técnica sintetiza com sucesso programas com várias cláusulas recursivas e cláusulas com vários literais recursivos). A metodologia também é capaz de fazer síntese múltipla de predicados.

Devido à sua expressividade, uma restrição de integridade pode substituir um grande número de exemplos negativos fechados. Tipicamente, verificar restrições é computacionalmente pesado. Na nossa metodologia, as restrições são tratadas usando uma estratégia de Monte Carlo (MONIC). Embora incompleta, a abordagem de Monte Carlo proporciona uma solução eficiente à verificação de restrições, o que é importante no contexto de síntese de programas.

A metodologia de síntese foi avaliada empiricamente de uma forma sistemática mostrando que é robusta na síntese de definições recursivas a partir de exemplos gerados aleatoriamente e que consegue competir com outras técnicas estado-da-arte.