\textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}

DOI10.1007/978-3-030-85315-0_18OpenAlexW3193303649MaRDI QIDQ2119984

Isabela Drămnesc, Tudor Jebelean

Publication date: 31 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-85315-0_18

zbMATH Keywords

sortingbinary treesmultisetslistsNoetherian inductiondeductive synthesis

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• Theorema
• ALISA
• KIDS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Synthesis of list algorithms by mechanical proving
• Multiset theory
• A synthesis of several sorting algorithms
• Remarks on A synthesis of several sorting algorithms
• Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
• Deductive synthesis of sorting programs
• Synthesis of sorting algorithms using multisets in \textit{Theorema}
• An approach to automatic deductive synthesis of functional programs
• Theorema 2.0: A System for Mathematical Theory Exploration
• Automatic Deductive Synthesis of Lisp Programs in the System ALISA
• Derivation of Sorting Algorithms from a Specification
• A Deductive Approach to Program Synthesis
• Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema
• Theorema 2.0: Computer-Assisted Natural-Style Mathematics
• From program verification to program synthesis
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• A general framework to build contextual cover set induction provers
• Automated synthesis of functional programs with auxiliary functions

This page was built for publication: \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}