Synthesis of list algorithms by mechanical proving
From MaRDI portal
Publication:485837
DOI10.1016/J.JSC.2014.09.030zbMATH Open1315.68263OpenAlexW1988598795MaRDI QIDQ485837FDOQ485837
Authors: Isabela Drămnesc, Tudor Jebelean 
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
Recommendations
- Proof-based synthesis of sorting algorithms for trees
- Synthesis of sorting algorithms using multisets in \textit{Theorema}
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Deductive synthesis of sorting programs
- scientific article; zbMATH DE number 108494
Data structures (68P05) Searching and sorting (68P10) General topics in the theory of algorithms (68W01)
Cites Work
- Title not available (Why is that?)
- Linear resolution with selection function
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- A synthesis of several sorting algorithms
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- A Deductive Approach to Program Synthesis
- Proving Properties of Programs by Structural Induction
- Title not available (Why is that?)
- Programs as proofs: A synopsis
- A note on synthesis and classification of sorting algorithms
- Remarks on A synthesis of several sorting algorithms
- Middle-out reasoning for synthesis and induction
- The TH\(\exists\)OREM\(\forall\) project: A progress report
- Algorithm synthesis by lazy thinking: examples and implementation in Theorema
- Synthesis: Dreams → Programs
- Proofs as programs
- Algorithm synthesis by lazy thinking: using problem schemes
- Algorithm classification through synthesis
- Logic program synthesis
- Title not available (Why is that?)
- Mathematical Knowledge Management
- Title not available (Why is that?)
- Program Development in Computational Logic
- The design of divide and conquer algorithms
Cited In (11)
- Synthesis of sorting algorithms using multisets in \textit{Theorema}
- \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}
- Algorithm synthesis by lazy thinking: examples and implementation in Theorema
- Proof pearl: A mechanized proof of GHC's mergesort
- Deductive synthesis of sorting programs
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Proof-based synthesis of sorting algorithms for trees
- Proving Properties about Lists Using Containers
- Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema
- Title not available (Why is that?)
- Algorithm synthesis by lazy thinking: using problem schemes
Uses Software
This page was built for publication: Synthesis of list algorithms by mechanical proving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q485837)
