Synthesis of list algorithms by mechanical proving

DOI10.1016/j.jsc.2014.09.030zbMath1315.68263MaRDI QIDQ485837

Tudor Jebelean, Isabela Drămnesc

Publication date: 14 January 2015

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2014.09.030

zbMATH Keywords

list; algorithm synthesis; Theorema

Mathematics Subject Classification ID

68P10: Searching and sorting

68P05: Data structures

68W01: General topics in the theory of algorithms

Related Items

Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema, Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques, Synthesis of sorting algorithms using multisets in \textit{Theorema}, \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}

Uses Software

• Mathematica
• Theorema

Cites Work

• The design of divide and conquer algorithms
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Programs as proofs: A synopsis
• A note on synthesis and classification of sorting algorithms
• A synthesis of several sorting algorithms
• Remarks on A synthesis of several sorting algorithms
• Middle-out reasoning for synthesis and induction
• Linear resolution with selection function
• Synthesis: Dreams → Programs
• Proofs as programs
• Algorithm classification through synthesis
• A Deductive Approach to Program Synthesis
• Logic program synthesis
• Mathematical Knowledge Management
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Proving Properties of Programs by Structural Induction
• Program Development in Computational Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item