Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
From MaRDI portal
Publication:1640636
DOI10.1016/j.jsc.2018.04.002zbMath1395.68246OpenAlexW2805273157WikidataQ129701038 ScholiaQ129701038MaRDI QIDQ1640636
Isabela Drămnesc, Tudor Jebelean, Sorin Stratulat
Publication date: 14 June 2018
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jsc.2018.04.002
Related Items
\textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}, Experiments with automated reasoning in the class, 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
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Conjecture synthesis for inductive theories
- Synthesis of list algorithms by mechanical proving
- Mechanically certifying formula-based Noetherian induction reasoning
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- Linear resolution with selection function
- Proof–Based Synthesis of Sorting Algorithms for Trees
- Fiat
- Refinements for Free!
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- Logic program synthesis
- Refinement Calculus
- Automating Inductive Proofs Using Theory Exploration
- Theorema 2.0: Computer-Assisted Natural-Style Mathematics
- Artificial Intelligence and Symbolic Computation
- Program development by stepwise refinement
- Program Development in Computational Logic
