Program synthesis of provable recursive functions

Abstract

Wir studieren die Synthese von rekursiven Funktionen mithilfe eines sättigungsbasierten, automatisierten Theorembeweis-Tools. Wir verwenden das Superpositionsprinzip, um die Korrektheit der Spezifizierungen an die Funktionen zu beweisen und konstruieren währenddessen den Code, der genau diese Spezifizierung erfüllt. Die Spezifizierungen der Funktionen sind in Prädikatenlogik ausgedrückt mit induktiv definierten Datentypen. Wir stellen neue Folgerungsregeln für Induktion vor und verwenden sogenannte Beantwortungsliterale, um rekursive Funktionen aus der Beweisableitung zu synthetisieren. Wir zeigen die Herausforderungen von Synthetisierung rekursiver Funktionen anhand konkreter Beispiele und heben dabei unsere Lösungen hervor.

We study the synthesis of recursive functions using saturation-based first-order theorem proving. We use superposition reasoning to prove the correctness of function specifications while constructing code that satisfies the given specification. The function specifications are expressed as first-order formulas with inductively defined data types. We present new inference rules for induction in saturation and use answer literals to synthesize recursive functions from saturation-based proof search. We show the challenges of recursive synthesis using concrete examples, highlighting our solutions in this context.