pith. sign in

arxiv: 2605.19683 · v1 · pith:YVG64WUOnew · submitted 2026-05-19 · 💻 cs.LO

Completeness of Synthesis under Realizability Assumptions using Superposition

M\'arton Hajdu , Petra Hozzov\'a , Laura Kov\'acs , Eva Maria Wagner This is my paper

Pith reviewed 2026-05-20 01:55 UTC · model grok-4.3

classification 💻 cs.LO
keywords program synthesissuperposition calculuscompletenessrealizability assumptionsrecursion-free programsautomated theorem provingsoftware verification
0
0 comments X

The pith

A refined superposition calculus finds a computable recursion-free program whenever one satisfying the specification exists.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends a superposition calculus to synthesize recursion-free programs that are correct by construction, even when the specification involves uncomputable symbols. It identifies failure cases in the original rules, introduces refinements to address them, and proves the new rules are sound. The central result is a completeness theorem under realizability assumptions: if any computable program meets the specification, the calculus will derive one. A reader would care because this turns automated theorem proving into a reliable tool for generating verified software without missing existing solutions.

Core claim

The authors prove that their refined superposition calculus is sound and complete for the synthesis of recursion-free programs in the presence of uncomputable symbols. Completeness holds in the sense that, under the stated realizability assumptions, the calculus derives a computable program satisfying the input specification whenever at least one such program exists. The refinement consists of targeted modifications to the inference rules that overcome specific incompleteness exhibited by the base calculus on certain synthesis problems.

What carries the argument

The refined superposition calculus for program synthesis, obtained by modifying the original rules to correctly handle uncomputable symbols while preserving recursion-free program generation.

If this is right

  • Synthesis tasks for recursion-free programs become decidable in the sense that an existing solution is guaranteed to be found.
  • Automated theorem proving can directly output a verified program rather than only a proof of existence.
  • Uncomputable symbols can be used in specifications without breaking the ability to extract concrete programs.
  • Soundness of the refined rules ensures every synthesized program is correct with respect to the specification.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same refinement strategy might be tested on other superposition-based or resolution-based systems for synthesis.
  • If realizability assumptions can be checked or approximated automatically, the method could become fully push-button for a larger class of specifications.
  • The recursion-free restriction suggests a natural next step of layering this technique with inductive reasoning for programs that use recursion.

Load-bearing premise

The realizability assumptions on the specification and symbols that make it possible for the calculus to locate a computable program when one exists.

What would settle it

A concrete specification together with a known computable recursion-free program that satisfies it, yet the refined calculus returns no program after exhaustive search under the realizability assumptions.

Figures

Figures reproduced from arXiv: 2605.19683 by Eva Maria Wagner, Laura Kov\'acs, M\'arton Hajdu, Petra Hozzov\'a.

Figure 1
Figure 1. Figure 1: Rules of SUPRA, where all maximal literals in a clause [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper extends a superposition-based calculus to synthesize recursion-free programs while permitting reasoning over uncomputable symbols. It exhibits concrete failure cases of the unmodified calculus, introduces rule refinements to address them, proves soundness of the refined calculus, and establishes a conditional completeness theorem: under stated realizability assumptions, if at least one computable recursion-free program satisfying the specification exists, the calculus derives one.

Significance. If the realizability assumptions prove to be both necessary and sufficiently weak, and if the soundness and completeness arguments hold, the work supplies a non-trivial theoretical guarantee for synthesis via automated theorem proving. This strengthens the case for superposition as a foundation for verified program construction involving partial or uncomputable specifications.

major comments (2)
  1. [§4 and §6] §4 (Refined Calculus) and §6 (Completeness): The realizability assumptions that license reasoning with uncomputable symbols while preserving completeness are introduced but never given an explicit, self-contained definition. Without this formulation it is impossible to verify whether the assumptions are weak enough to cover typical synthesis specifications or whether they implicitly encode the existence of a computable solution, rendering the completeness result close to tautological.
  2. [§3 and §6] §3 (Failure Cases) and §6: The paper shows that the unmodified calculus can fail to derive a program even when one exists; the refinements are claimed to eliminate these failures under the realizability assumptions. However, no explicit argument is given that every failure case is covered by the assumptions or that the refinements do not introduce new incompleteness for recursion-free programs.
minor comments (2)
  1. [§4] The notation for the refined inference rules would benefit from a compact tabular summary or side-by-side comparison with the original rules.
  2. [§2] A brief discussion of how the realizability assumptions relate to existing notions in constructive logic or realizability theory would help situate the contribution.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review of our manuscript. We address the two major comments point by point below, indicating the revisions we intend to incorporate.

read point-by-point responses

  1. Referee: [§4 and §6] §4 (Refined Calculus) and §6 (Completeness): The realizability assumptions that license reasoning with uncomputable symbols while preserving completeness are introduced but never given an explicit, self-contained definition. Without this formulation it is impossible to verify whether the assumptions are weak enough to cover typical synthesis specifications or whether they implicitly encode the existence of a computable solution, rendering the completeness result close to tautological.

    Authors: We agree that a more explicit, self-contained formulation of the realizability assumptions would improve clarity. In the revised version we will insert a dedicated paragraph in §4 that defines them as a collection of first-order axioms asserting that each uncomputable symbol is realized by some computable function (possibly different for each symbol) that is consistent with the given specification. These axioms concern only the local behavior of individual symbols and do not assert the existence of a single recursion-free program satisfying the entire specification; the latter remains an explicit hypothesis of the completeness theorem in §6. Consequently the result is not tautological. We will also add a short discussion of the assumptions' strength relative to common synthesis scenarios involving oracles or abstract functions. revision: yes

  2. Referee: [§3 and §6] §3 (Failure Cases) and §6: The paper shows that the unmodified calculus can fail to derive a program even when one exists; the refinements are claimed to eliminate these failures under the realizability assumptions. However, no explicit argument is given that every failure case is covered by the assumptions or that the refinements do not introduce new incompleteness for recursion-free programs.

    Authors: We accept that an explicit linking argument is missing. In the revision we will add a subsection to §6 that (i) recalls each concrete failure case from §3, (ii) verifies that the realizability assumptions hold in that case, and (iii) shows how the refined rules derive a solution. We will also include a short lemma establishing that the refinements are conservative for recursion-free programs: any derivation possible with the original calculus remains possible after refinement. While we do not claim to have exhaustively enumerated every conceivable failure mode, the cases in §3 are representative of the incompleteness phenomena the refinements target. revision: partial

Circularity Check

0 steps flagged

Completeness proof is self-contained under realizability assumptions with no reduction to inputs

full rationale

The paper refines the superposition calculus to handle synthesis of recursion-free programs with uncomputable symbols, shows failure cases for the original rules, then proves soundness of the refined rules and conditional completeness: if at least one computable program satisfying the specification exists, the calculus finds one. These results are established via explicit formal proofs in the paper rather than by fitting parameters, self-defining terms, or load-bearing self-citations that reduce the claim to prior unverified work. The realizability assumptions are stated as enabling conditions for the calculus and are not shown to be equivalent to the target result by construction. Minor self-citation of prior superposition literature is present but does not carry the central completeness argument.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard mathematical axioms from first-order logic and superposition calculus. No free parameters are introduced. No new entities are postulated. The realizability assumptions function as domain assumptions specific to the synthesis setting.

axioms (2)
  • standard math Standard axioms and inference rules of the superposition calculus in first-order logic with equality.
    Invoked as the base for the extension to program synthesis.
  • domain assumption Realizability assumptions that link specifications to the existence of computable programs.
    These are required for the completeness statement and are referenced in the title and abstract.

pith-pipeline@v0.9.0 · 5637 in / 1354 out tokens · 29952 ms · 2026-05-20T01:55:39.317881+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

46 extracted references · 46 canonical work pages

  1. [1]

    In: CADE (2025), https://dl.acm.org/doi/10.1007/978-3-031-99984-0_27

    Achammer, F., Hetzl, S., Schmidt, R.: Computing Witnesse s Using the SCAN Algo- rithm. In: CADE (2025), https://dl.acm.org/doi/10.1007/978-3-031-99984-0_27

    work page doi:10.1007/978-3-031-99984-0_27 2025

  2. [2]

    In: Dependable Software Systems Engineering

    Alur, R., Bodík, R., Dallal, E., Fisman, D., Garg, P., Juni wal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Sy ntax-Guided Synthesis. In: Dependable Software Systems Engineering. I OS Press (2015). https://doi.org/10.3233/978-1-61499-495-4-1

    work page doi:10.3233/978-1-61499-495-4-1 2015

  3. [3]

    Alur, R., Fisman, D., Padhi, S., Reynolds, A., Singh, R., U dupa, A.: SyGuS-Comp

    work page

  4. [4]

    https://sygus.org/comp/2019/ Completeness of Synthesis under Realizability 17

    work page 2019

  5. [5]

    In: AAECC 5, 193–21 2 (1994)

    Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem prov- ing for hierarchic first-order theories. In: AAECC 5, 193–21 2 (1994). https://doi.org/10.1007/BF01190829

    work page doi:10.1007/bf01190829 1994

  6. [6]

    In: CADE (2023)

    Bhayat, A., Schoisswohl, J., Rawson, M.: Superposition w ith Delayed Unification. In: CADE (2023). https://doi.org/10.1007/978-3-031-38499-8_2

    work page doi:10.1007/978-3-031-38499-8_2 2023

  7. [7]

    In: IJCAR (2016)

    Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S ., Zivota, S.: System Descrip- tion: GAPT 2.0. In: IJCAR (2016). https://doi.org/10.1007/978-3-319-40229-1_20

    work page doi:10.1007/978-3-319-40229-1_20 2016

  8. [8]

    Machine Intelligence 4, 183–205 (1969)

    Green, C.: Theorem-Proving by Resolution as a Basis for Qu estion-Answering Systems. Machine Intelligence 4, 183–205 (1969)

    work page 1969

  9. [9]

    In: POPL (2011)

    Gulwani, S.: Automating string processing in spreadshee ts using input-output examples. In: POPL (2011). https://doi.org/10.1145/1926385.1926423

    work page doi:10.1145/1926385.1926423 2011

  10. [10]

    In: PLDI (2011)

    Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthes is of Loop-Free Programs. In: PLDI (2011). https://doi.org/10.1145/1993498.1993506

    work page doi:10.1145/1993498.1993506 2011

  11. [11]

    Gulwani, S., Jojic, N.: Probabilistic inference of prog rams from input/output examples (2006), https://api.semanticscholar.org/CorpusID:59650668

    work page 2006

  12. [12]

    In: Proc

    Hozzová, P.: Integrating Answer Literals with A V ATAR for Program Synthesis. In: Proc. of the 7th and 8th Vampire Workshop (2024). https://doi.org/10.29007/vmn9

    work page doi:10.29007/vmn9 2024

  13. [13]

    In: Automat ed Reasoning (2024)

    Hozzová, P., Amrollahi, D., Hajdu, M., Kovács, L., Voron kov, A., Wagner, E.M.: Synthesis of Recursive Programs in Saturation. In: Automat ed Reasoning (2024). https://doi.org/10.1007/978-3-031-63498-7_10

    work page doi:10.1007/978-3-031-63498-7_10 2024

  14. [14]

    In: FMCAD (2025)

    Hozzová, P., Bjørner, N.: Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols. In: FMCAD (2025). https://doi.org/10.34727/2025/isbn.978-3-85448-084-6_28

    work page doi:10.34727/2025/isbn.978-3-85448-084-6_28 2025

  15. [15]

    In: CADE (2023)

    Hozzová, P., Kovács, L., Norman, C., Voronkov, A.: Program Synthesis in Saturation. In: CADE (2023). https://doi.org/10.1007/978-3-031-38499-8_18

    work page doi:10.1007/978-3-031-38499-8_18 2023

  16. [16]

    In: PLDI (2020)

    Huang, K., Qiu, X., Shen, P., Wang, Y.: Reconciling Enume rative and Deductive Program Synthesis. In: PLDI (2020). https://doi.org/10.1145/3385412.3386027

    work page doi:10.1145/3385412.3386027 2020

  17. [17]

    In: CADE (2011)

    Kovács, L., Moser, G., Voronkov, A.: On Transfinite Knuth -Bendix Orders. In: CADE (2011). https://doi.org/10.1007/978-3-642-22438-6_29

    work page doi:10.1007/978-3-642-22438-6_29 2011

  18. [18]

    Communicatio ns of ACM (1974)

    Lee, R.C.T., Waldinger, R.J., Chang, C.L.: An Improved P rogram- Synthesizing Algorithm and Its Correctness. Communicatio ns of ACM (1974). https://doi.org/10.1145/360924.360967

    work page doi:10.1145/360924.360967 1974

  19. [19]

    In: CA V (2024)

    Li, Y., Parsert, J., Polgreen, E.: Guiding Enumerative P rogram Synthesis with Large Language Models. In: CA V (2024). https://doi.org/10.1007/978-3-031-65630-9_15

    work page doi:10.1007/978-3-031-65630-9_15 2024

  20. [20]

    TOPLAS (1980)

    Manna, Z., Waldinger, R.: A Deductive Approach to Progra m Synthesis. TOPLAS (1980). https://doi.org/10.1145/357084.357090

    work page doi:10.1145/357084.357090 1980

  21. [21]

    Equivalence

    Newman, M.H.A.: On Theories with a Combinatorial Definit ion of "Equivalence.". Journal of Symbolic Logic (1942). https://doi.org/10.2307/2269299

    work page doi:10.2307/2269299 1942

  22. [22]

    In: Handbook of Automated Reasonings

    Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theo rem Proving. In: Handbook of Automated Reasonings. Elsevier and MIT Press (2 001). https://doi.org/10.1016/B978-044450813-3/50009-6

    work page doi:10.1016/b978-044450813-3/50009-6

  23. [23]

    In: Krieg-Brückner, B

    Nieuwenhuis, R., Rubio, A.: Basic superposition is comp lete. In: Krieg-Brückner, B. (ed.) ESOP ’92 (1992). https://doi.org/10.1007/3-540-55253-7_22

    work page doi:10.1007/3-540-55253-7_22 1992

  24. [24]

    In : 4th Vampire Workshop (2018)

    Reger, G.: Revisiting Question Answering in Vampire. In : 4th Vampire Workshop (2018). https://doi.org/10.29007/fjc4

    work page doi:10.29007/fjc4 2018

  25. [25]

    In: T ACAS (2018)

    Reger, G., Suda, M., Voronkov, A.: Unification with Abstr action and Theory Instantiation in Saturation-Based Reasoning. In: T ACAS (2018). https://doi.org/10.1007/978-3-319-89960-2_1

    work page doi:10.1007/978-3-319-89960-2_1 2018

  26. [26]

    Formal Methods in System Design (201 9)

    Reynolds, A., Kuncak, V., Tinelli, C., Barrett, C., Dete rs, M.: Refutation- based Synthesis in SMT. Formal Methods in System Design (201 9). https://doi.org/10.1007/s10703-017-0270-2 18 Hajdu, Hozzová, Kovács, Wagner

    work page doi:10.1007/s10703-017-0270-2

  27. [27]

    Rietdijk, M.: Extracting programs from proofs using Fri edman’s A-translation and realizability (2018), https://repositum.tuwien.at/handle/20.500.12708/8452

    work page 2018

  28. [28]

    In: CA V (2012)

    Singh, R., Gulwani, S.: Synthesizing Number Transforma tions from Input-Output Examples. In: CA V (2012). https://doi.org/10.1007/978-3-642-31424-7_44

    work page doi:10.1007/978-3-642-31424-7_44 2012

  29. [29]

    In: CADE (1994)

    Stickel, M., Waldinger, R., Lowry, M., Pressburger, T., Underwood, I.: Deductive composition of astronomical software from subroutine libr aries. In: CADE (1994). https://doi.org/10.1007/3-540-58156-1_24

    work page doi:10.1007/3-540-58156-1_24 1994

  30. [30]

    In: Computer Science Logic (1995)

    Tammet, T.: Completeness of resolution for definite answ ers with case analysis. In: Computer Science Logic (1995). https://doi.org/10.1007/BFb0022265

    work page doi:10.1007/bfb0022265 1995

  31. [31]

    In: CADE (2015), 10.1007/978-3-319-21401-6_33

    Tiwari, A., Gascón, A., Dutertre, B.: Program Synthesis Using Dual Interpretation. In: CADE (2015), 10.1007/978-3-319-21401-6_33

    work page doi:10.1007/978-3-319-21401-6_33 2015

  32. [32]

    In: Computer Science Logic (1992)

    Voronkov, A.: On completeness of program synthesis syst ems. In: Computer Science Logic (1992). https://doi.org/10.1007/BFb0023785 Completeness of Synthesis under Realizability 19 Appendix A Proofs from Section 4 Theorem 1 (Soundness). The SUPRA calculus is sound with respect to the semantics of answer clauses. Proof. We prove soundness for the rules EqRe...

    work page doi:10.1007/bfb0023785 1992

  33. [33]

    Let s′ be smallest subterm of s such that s′≻ lpo t

    Assume by contradiction that s≻ lpo t. Let s′ be smallest subterm of s such that s′≻ lpo t. By definition top(t)≫ top(s′), neither case 2 nor 3 can hold, contradiction. Induction step. Let t = f (t1, ... t j− 1, t j , t j+1 ... , t n) where top(tj )∈ Σ u. Assume by contradiction that s≻ lpo t. Let s′ be smallest subterm of s such that s′≻ lpo t. Because s′...

    work page

  34. [34]

    We denote by w0 the smallest weight of constants

    We will refer to w(f ) as the weight of f . We denote by w0 the smallest weight of constants. For p∈ Σ∪V , we write |t|p to denote the number of occurrences of p in term t. For example,|f (x,x )|f = 1,|f (x,x )|x = 2 and|f (x,x )|y = 0. LetP(V) be the set of linear expressions overV with integer coefficients. The weight of a term t, denoted by|t|, is a line...

    work page

  35. [35]

    RS is a convergent rewrite system

    work page

  36. [36]

    RC S ⊨ C if and only if for all D≻ C we have RD S ⊨ C, if and only if RS ⊨ C. Proof. Towards the first property, first, we prove that the rewrite re lation of RS is terminating. RS terminates since l≻ r for all its rules l→ r by condition 5 of Definition 10. Second, we prove that the rewrite relation of RS is confluent. Newman’s lemma states that every termin...

    work page

  37. [37]

    For any answer clause C of the form C[x]/llbracketx/rrbracket, any uncomputable c-clause in iteNF(C,t ) is of the form C ▽L, whereL∈ ∆∪{ ǫ}

    work page

  38. [38]

    For any L∈ ∆∪{ ǫ}, there is a ground computable simple term tL such that for any answer clause C of the form C[x]/llbracketx/rrbracket, uncomputable C′ ▽L∈ iteNF(C,t ), and substitution θ such that Cθ = C′, it holds that xθ = tL or x is a variable not in C

    work page

  39. [39]

    If ǫ /∈ ∆ , then for any answer clause C of the form C[x]/llbracketx/rrbracket, uncomputable C′▼∈ iteNF(C,t ), and substitution θ such that Cθ = C′, it holds that x is a variable not in C

    work page

  40. [40]

    For any L,K∈ ∆ such thatL̸ =K,L andK contain a complementary literal. Proof. By induction on the structure of t. Case 1. t is of the form ite(L,s,s ′). By the induction hypothesis, there are clause setsS and S′ for program terms s and s′, respectively, that satisfy the four properties. We now pro ve that the following computable ground clause set ∆ satisfi...

    work page

  41. [41]

    It follows trivially for D ▽ ˆLL, too and we set t ˆL∨L = tL

    D ▽ ˆLL where D ▽L∈ iteNF(C,s ): by induction hypothesis there is a ground computable term tL for D ▽L such that xθ = tL or x is a variable not in C if C[x]θ = D. It follows trivially for D ▽ ˆLL, too and we set t ˆL∨L = tL

    work page

  42. [42]

    It follows trivially for D ▽ LL, too and we set tL∨L = tL

    D ▽ LL where D ▽L∈ iteNF(C,s ′): by induction hypothesis there is a ground computable term tL for D ▽L such that xθ = tL or x is a variable not in C if C[x]θ = D. It follows trivially for D ▽ LL, too and we set tL∨L = tL. Towards Item3, letC be an answer clause of the form C[x]/llbracketx/rrbracketand θ a substitution. Suppose that C does not contain x. T...

    work page

  43. [43]

    Any uncomputable C∈ Gr(S,t ) is of the form C ▽L whereL∈ ∆∪{ ǫ}

    work page

  44. [44]

    For any L∈ ∆∪{ ǫ}, there is a ground computable simple term tL such that for any uncomputable C′▽L∈ Gr(S,t ), substitution θ, and clause C/llbracketp/rrbracket∈ S such that Cθ = C′, it holds that p is a simple term and pθ = tL or p is a variable not in C

    work page

  45. [45]

    If ǫ /∈ ∆ , then for any uncomputable C′▼∈ Gr(S,t ), substitution θ, and clause C/llbracketp/rrbracket∈ S such that Cθ = C′, it holds that p is a variable not in C

    work page

  46. [46]

    28 Hajdu, Hozzová, Kovács, Wagner Proof

    For any L,K∈ ∆ such thatL̸ =K,L andK contain a complementary literal. 28 Hajdu, Hozzová, Kovács, Wagner Proof. Let ∆ be the set of ground literals obtained by applying Lemma 12 for the term t. Towards Item 1, let C∈ Gr(S, t ). We prove the property by induction on the derivation length of C. Case 1. C has a derivation length 0. By Item 1 of Definition 15, ...

    work page