基于定理证明的多集排序算法综合
Proof-Based Synthesis of Sorting Algorithms Using Multisets in Theorema
摘要：
使用多集，我们开发了新的技术，机械化的证明列表排序算法的合成结构，我们证明了他们的定理系统。我们使用经典的原则提取算法作为一组重写规则的基础上发现的证人证明所需的功能（输入和输出条件）的规格产生的合成猜想。证明是自然的风格，使用标准规则，但最重要的是领域特定的推理规则和策略。特别是使用多集，使我们能够开发强大的战略合成任意结构的递归算法一般诺特归纳，以及自动生成的规格的所有必要的辅助功能（插入，合并，分裂），其合成是使用相同的方法。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
