Completeness of Synthesis under Realizability Assumptions using Superposition
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914580372914176 |
|---|---|
| author | Hajdu, Márton Hozzová, Petra Kovács, Laura Wagner, Eva Maria |
| author_facet | Hajdu, Márton Hozzová, Petra Kovács, Laura Wagner, Eva Maria |
| contents | Program synthesis is the task of automatically deriving a program that has been specified by a user in advance. Combining automated theorem proving with program synthesis enables the automated construction of proven-to-be-correct programs, thereby ensuring software reliability. In this paper, we consider the superposition-based calculus extended to support synthesis of recursion-free programs allowing reasoning with uncomputable symbols. We present cases where the calculus fails and refine it to solve them. We prove that the refined calculus is sound. Finally, we also prove completeness in the following sense: if at least one computable program satisfying the given specification exists, we show that the modified calculus finds one. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_19683 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Completeness of Synthesis under Realizability Assumptions using Superposition Hajdu, Márton Hozzová, Petra Kovács, Laura Wagner, Eva Maria Logic in Computer Science Program synthesis is the task of automatically deriving a program that has been specified by a user in advance. Combining automated theorem proving with program synthesis enables the automated construction of proven-to-be-correct programs, thereby ensuring software reliability. In this paper, we consider the superposition-based calculus extended to support synthesis of recursion-free programs allowing reasoning with uncomputable symbols. We present cases where the calculus fails and refine it to solve them. We prove that the refined calculus is sound. Finally, we also prove completeness in the following sense: if at least one computable program satisfying the given specification exists, we show that the modified calculus finds one. |
| title | Completeness of Synthesis under Realizability Assumptions using Superposition |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.19683 |