Program Synthesis in Saturation
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913247937953792 |
|---|---|
| author | Hozzová, Petra Kovács, Laura Norman, Chase Voronkov, Andrei |
| author_facet | Hozzová, Petra Kovács, Laura Norman, Chase Voronkov, Andrei |
| contents | We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establish validity of this formula and discover program fragments satisfying the specification. As a result, when deriving a proof of program correctness, we also synthesize a program that is correct with respect to the given specification. We describe properties of the calculus that a saturation-based prover capable of synthesis should employ, and extend the superposition calculus in a corresponding way. We implemented our work in the first-order prover Vampire, extending the successful applicability of first-order proving to program synthesis.
This is an extended version of an Automated Deduction -- CADE 29 paper with the same title and the same authors. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_18962 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Program Synthesis in Saturation Hozzová, Petra Kovács, Laura Norman, Chase Voronkov, Andrei Logic in Computer Science We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establish validity of this formula and discover program fragments satisfying the specification. As a result, when deriving a proof of program correctness, we also synthesize a program that is correct with respect to the given specification. We describe properties of the calculus that a saturation-based prover capable of synthesis should employ, and extend the superposition calculus in a corresponding way. We implemented our work in the first-order prover Vampire, extending the successful applicability of first-order proving to program synthesis. This is an extended version of an Automated Deduction -- CADE 29 paper with the same title and the same authors. |
| title | Program Synthesis in Saturation |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2402.18962 |