An approach to automatic deductive synthesis of functional programs

DOI10.1007/S10472-007-9079-9MaRDI QIDQ2457802zbMATH OpenOpenAlexFDO

Authors 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 reasoningDeductive program synthesisInductionProof planningRippling

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2090035
• Automated synthesis of functional programs with auxiliary functions
• Inductive synthesis of functional programs: an explanation based generalization approach
• Synthesis of functional programs with help of first-order intuitionistic logic
• An approach to the inductive synthesis of programs
• scientific article; zbMATH DE number 108494
• scientific article; zbMATH DE number 4113956
• Deductive and inductive synthesis of equational programs
• scientific article; zbMATH DE number 2079865

Cites work

• A calculus for and termination of rippling
• A Deductive Approach to Program Synthesis
• A higher-order interpretation of deductive tableau
• An improved program-synthesizing algorithm and its correctness
• Automatic Deductive Synthesis of Lisp Programs in the System ALISA
• Deductive synthesis of sorting programs
• Experiments with a Heuristic Compiler
• scientific article; zbMATH DE number 1389654 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Inductive synthesis of functional programs: an explanation based generalization approach
• Isabelle. A generic theorem prover
• Middle-out reasoning for synthesis and induction
• Rippling: A heuristic for guiding inductive proofs
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• The automation of proof by mathematical induction

Cited in

(13)

• An implementation of syntax directed functional programming on nested- stack machines
• Automated synthesis of recursive programs from a logical specification
• Deductive and inductive synthesis of equational programs
• Synthesis of sorting algorithms using multisets in \textit{Theorema}
• \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}
• Automatic synthesis of action programs for intelligent robots
• Automatic Deductive Synthesis of Lisp Programs in the System ALISA
• scientific article; zbMATH DE number 3963167 (Why is no real title available?)
• scientific article; zbMATH DE number 108494 (Why is no real title available?)
• scientific article; zbMATH DE number 2040721 (Why is no real title available?)
• Logics in Artificial Intelligence
• A higher-order interpretation of deductive tableau
• Automated synthesis of functional programs with auxiliary functions

Describes a project that uses

Uses Software

• CLAM
• Nuprl
• Isabelle
• ALISA
• Oyster

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

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