Synthesis of list algorithms by mechanical proving

DOI10.1016/j.jsc.2014.09.030zbMath1315.68263OpenAlexW1988598795MaRDI 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

listalgorithm synthesisTheorema

Mathematics Subject Classification ID

Related Items (4)

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

Uses Software

• Mathematica
• Theorema

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: Synthesis of list algorithms by mechanical proving