Completeness of Synthesis Under Realizability Assumptions Using Superposition

Hajdu, Márton; Hozzová, Petra; Kovács, Laura; Wagner, Eva Maria

doi:10.1007/978-3-032-32589-1_2

Record link:

http://hdl.handle.net/20.500.12708/230139

Title:

Completeness of Synthesis Under Realizability Assumptions Using Superposition

Citation:

Hajdu, M., Hozzová, P., Kovács, L., & Wagner, E. M. (2026). Completeness of Synthesis Under Realizability Assumptions Using Superposition. In A. Biere, C. Lutz, & S. Negri (Eds.), Automated Reasoning : 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I (pp. 22–40). Springer Cham. https://doi.org/10.1007/978-3-032-32589-1_2

CatalogPlus:

AC17985303

Publisher DOI:

10.1007/978-3-032-32589-1_2

Publication Type:

Inproceedings - Full-Paper Contribution

Language:

English

Authors:

Hajdu, Márton
Hozzová, Petra
Kovács, Laura
Wagner, Eva Maria

Organisational Unit:

E192-04 - Forschungsbereich Formal Methods in Systems Engineering
E056-10 - Fachbereich SecInt-Secure and Intelligent Human-Centric Digital Technologies
E056-13 - Fachbereich LogiCS
E056-17 - Fachbereich Trustworthy Autonomous Cyber-Physical Systems
E056-26 - Fachbereich Automated Reasoning

Published in:

Automated Reasoning : 13th International Joint Conference, IJCAR 2026, Lisbon, Portugal, July 26–29, 2026, Proceedings, Part I

ISBN:

978-3-032-32589-1

Volume:

16688

DOI of the book:

10.1007/978-3-032-32589-1

Date (published):

24-Jul-2026

Event name:

13th International Joint Conference Automated Reasoning (IJCAR 2026)

Event date:

26-Jul-2026 - 29-Jul-2026

Event place:

Lissabon, Portugal

Number of Pages:

Publisher:

Springer Cham, Cham, Switzerland

Peer reviewed:

Yes

Keywords:

Program Synthesis; Saturation; Superposition; Theorem Proving

Abstract:

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.

Project title:

Structured Doctoral Program on Automated Reasoning: DOC1345324 (FWF - Österr. Wissenschaftsfonds)

Project (external):

European Research Council (ERC)

Project ID:

101002685

Link (external):

https://arxiv.org/abs/2605.19683

Research Areas:

Mathematical and Algorithmic Foundations: 50%
Computer Science Foundations: 50%

Science Branch:

1020 - Informatik: 80%
1010 - Mathematik: 20%