Program Synthesis in Saturation

DOI10.1007/978-3-031-38499-8_18MaRDI QIDQ6492751zbMATH OpenFDO

Authors Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_18

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A Deductive Approach to Program Synthesis
• A Machine-Oriented Logic Based on the Resolution Principle
• A theory of formal synthesis via inductive learning
• An improved program-synthesizing algorithm and its correctness
• AVATAR: The Architecture for First-Order Theorem Provers
• Completeness of Resolution for Definite Answers
• From program verification to program synthesis
• scientific article; zbMATH DE number 3380160 (Why is no real title available?)
• Paramodulation-based theorem proving
• Program synthesis using dual interpretation
• The semantics of answer literals
• Unification with abstraction and theory instantiation in saturation-based reasoning

Cited in

(3)

• Synthesis benchmarks for automated reasoning
• SMT and functional equation solving over the reals: challenges from the IMO
• Synthesis of recursive programs in saturation

This page was built for publication: Program Synthesis in Saturation

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