Synthesis of recursive programs in saturation

DOI10.1007/978-3-031-63498-7_10MaRDI QIDQ7034870zbMATH OpenFDO

Authors Petra Hozzová, Daneshvar Amrollahi, Márton Hajdu, Laura Kovács, Andrei Voronkov, Eva Maria Wagner

Publication date 31 January 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-63498-7_10

zbMATH Keywords

inductionprogram synthesisrecursionsaturationsuperpositiontheorem proving

Mathematics Subject Classification ID

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

Cites work

• A decision procedure for term algebras with queues
• A Deductive Approach to Program Synthesis
• An improved program-synthesizing algorithm and its correctness
• Completeness of Resolution for Definite Answers
• From program verification to program synthesis
• scientific article; zbMATH DE number 1418280 (Why is no real title available?)
• scientific article; zbMATH DE number 3380160 (Why is no real title available?)
• Induction in saturation-based proof search
• Induction with generalization in superposition reasoning
• Integer induction in saturation
• On the interpretation of intuitionistic number theory
• Paramodulation-based theorem proving
• Program Synthesis in Saturation
• Programmable program synthesis
• Refutation-based synthesis in SMT
• Synthesis of recursive ADT transformations from reusable templates
• Synthesis of recursive programs in saturation

Cited in

(4)

• Synthesis benchmarks for automated reasoning
• SMT and functional equation solving over the reals: challenges from the IMO
• Synthesis of recursive programs in saturation
• Automating the derivation of unification algorithms. A case study in deductive program synthesis

This page was built for publication: Synthesis of recursive programs in saturation

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