@techreport{RISC6206,author = {Isabela Dramnesc and Tudor Jebelean},
title = {{Synthesis of Delete on Lists and Binary Trees Using Multisets in Theorema}},
language = {English},
abstract = {We demonstrate the deduction based synthesis of element deletion algorithms for
[sorted] lists and [sorted] binary trees, by first developing the necessary theory which is
multi–type: basic ordered elements, multisets, lists, and trees. The generated algorithms are
“pattern matching”, namely sets of conditional equalities, and we also demonstrate their
transformation into functional algorithms and, for lists, into tail recursive algorithms. This
work constitutes a case study first in theory exploration and second in automated synthesis
and transformation of algorithms synthesized on the basis of natural style proofs, which
allows to investigate the heuristics of theory construction on multiple types, as well as the
natural style inferences and strategies for constructing human readable synthesis proofs. The
experiments are performed in the frame of the Theorema system.},
number = {20-15},
year = {2020},
month = {September},
keywords = {automated reasoning; algorithm synthesis; lists; binary trees; multisets; Theorema},
length = {22},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}