Deductive synthesis of sorting programs

DOI10.1016/S0747-7171(89)80040-9MaRDI QIDQ1822927zbMATH OpenFDO

Authors Jonathan Traugott

Publication date 1989

Published in Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

derivationsautomatic programmingprogram constructiondeductive synthesisrecursive sorting programs

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Searching and sorting (68P10) Artificial intelligence (68T99) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Synthesis of list algorithms by mechanical proving
• A higher-order interpretation of deductive tableau
• From program verification to program synthesis
• Deductive and inductive synthesis of equational programs
• Proof-based synthesis of sorting algorithms for trees

Cites work

• scientific article; zbMATH DE number 3589703 (Why is no real title available?)
• A Deductive Approach to Program Synthesis
• A mechanical solution of Schubert's steamroller by many-sorted resolution
• A synthesis of several sorting algorithms
• Algorithm classification through synthesis
• Completely non-clausal theorem proving
• Special relations in automated deduction
• Top-down synthesis of divide-and-conquer algorithms

Cited in

(16)

• Synthesis of sorting algorithms using multisets in \textit{Theorema}
• An approach to automatic deductive synthesis of functional programs
• The origin of a binary-search paradigm
• Top-down synthesis of divide-and-conquer algorithms
• \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema}
• Program construction by verifying specification
• A theory for deductive synthesis of algorithms in the computing milieu
• Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
• Proof-based synthesis of sorting algorithms for trees
• scientific article; zbMATH DE number 512377 (Why is no real title available?)
• scientific article; zbMATH DE number 7444023 (Why is no real title available?)
• Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema
• Synthesis of list algorithms by mechanical proving
• scientific article; zbMATH DE number 3845028 (Why is no real title available?)
• A note on synthesis and classification of sorting algorithms
• A higher-order interpretation of deductive tableau

This page was built for publication: Deductive synthesis of sorting programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1822927)