Synthesis of sorting algorithms using multisets in \textit{Theorema}
From MaRDI portal
Publication:1996870
Abstract: Using multisets, we develop novel techniques for mechanizing the proofs of the synthesis conjectures for list-sorting algorithms, and we demonstrate them in the Theorema system. We use the classical principle of extracting the algorithm as a set of rewrite rules based on the witnesses found in the proof of the synthesis conjecture produced from the specification of the desired function (input and output conditions). The proofs are in natural style, using standard rules, but most importantly domain specific inference rules and strategies. In particular the use of multisets allows us to develop powerful strategies for the synthesis of arbitrarily structured recursive algorithms by general Noetherian induction, as well as for the automatic generation of the specifications of all necessary auxiliary functions (insert, merge, split), whose synthesis is performed using the same method.
Recommendations
- Synthesis of list algorithms by mechanical proving
- Proof-based synthesis of sorting algorithms for trees
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Deductive synthesis of sorting programs
- Algorithm synthesis by lazy thinking: examples and implementation in Theorema
Cites work
- A Deductive Approach to Program Synthesis
- A synthesis of several sorting algorithms
- Algorithm synthesis by lazy thinking: using problem schemes
- An approach to automatic deductive synthesis of functional programs
- Automatic Deductive Synthesis of Lisp Programs in the System ALISA
- Deductive synthesis of sorting programs
- Derivation of Sorting Algorithms from a Specification
- From program verification to program synthesis
- scientific article; zbMATH DE number 3913652 (Why is no real title available?)
- scientific article; zbMATH DE number 1052006 (Why is no real title available?)
- scientific article; zbMATH DE number 2217734 (Why is no real title available?)
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Multiset theory
- Proof-based synthesis of sorting algorithms for trees
- Remarks on A synthesis of several sorting algorithms
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Synthesis of list algorithms by mechanical proving
- The THOREM project: A progress report
- Theorema 2.0: A System for Mathematical Theory Exploration
- Theorema 2.0: computer-assisted natural-style mathematics
Cited in
(9)- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Reflections on and of minor-closed classes of multisorted operations
- \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}
- A theoretical look at \textsc{Electre Tri}-nB and related sorting models
- Proof-based synthesis of sorting algorithms for trees
- Synthesis of list algorithms by mechanical proving
- Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema
- Sorting multisets stably in minimum space
- Experiments with automated reasoning in the class
This page was built for publication: Synthesis of sorting algorithms using multisets in \textit{Theorema}
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1996870)
