Completeness of synthesis under realizability assumptions using superposition

DOI10.1007/978-3-032-32589-1_2MaRDI QIDQ7411150zbMATH OpenFDO

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

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32589-1_2

zbMATH Keywords

program synthesissaturationsuperpositiontheorem proving

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A Deductive Approach to Program Synthesis
• An improved program-synthesizing algorithm and its correctness
• Automating string processing in spreadsheets using input-output examples
• Computing witnesses using the SCAN algorithm
• scientific article; zbMATH DE number 408816 (Why is no real title available?)
• scientific article; zbMATH DE number 2079036 (Why is no real title available?)
• scientific article; zbMATH DE number 3380160 (Why is no real title available?)
• Paramodulation-based theorem proving
• Program Synthesis in Saturation
• Program synthesis using dual interpretation
• Refutation-based synthesis in SMT
• Refutational theorem proving for hierarchic first-order theories
• Superposition with Delayed Unification
• Synthesis of recursive programs in saturation
• System description: GAPT 2.0
• Unification with abstraction and theory instantiation in saturation-based reasoning

This page was built for publication: Completeness of synthesis under realizability assumptions using superposition

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7411150)