An approach to automatic deductive synthesis of functional programs

DOI10.1007/s10472-007-9079-9zbMath1125.68030OpenAlexW2042550236MaRDI QIDQ2457802

Yulia Korukhova

Publication date: 23 October 2007

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-007-9079-9

zbMATH Keywords

Automated reasoningInductionRipplingDeductive program synthesisProof planning

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

\textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema} ⋮ Automatic synthesis of action programs for intelligent robots ⋮ Synthesis of sorting algorithms using multisets in \textit{Theorema}

Uses Software

• Isabelle
• ALISA
• Nuprl
• CLAM
• Oyster

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Rippling: A heuristic for guiding inductive proofs
• Isabelle. A generic theorem prover
• Deductive synthesis of sorting programs
• Middle-out reasoning for synthesis and induction
• A calculus for and termination of rippling
• Automatic Deductive Synthesis of Lisp Programs in the System ALISA
• A Deductive Approach to Program Synthesis
• An improved program-synthesizing algorithm and its correctness
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Experiments with a Heuristic Compiler
• A higher-order interpretation of deductive tableau

This page was built for publication: An approach to automatic deductive synthesis of functional programs