Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema

  • Isabela DrămnescEmail author
  • Tudor Jebelean
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11989)


We demonstrate the automatic proof–based synthesis of merging and inserting algorithms for [sorted] binary trees, using the notion of multisets, in the Theorema system. Each algorithm is extracted from the proof of the conjecture based on the specification of the desired function, in the form of a list of [conditional] equalities, which can be directly executed. The proofs are performed in natural style, using general techniques, but most importantly efficient inference rules and strategies specific for the domains involved. In particular we present specific techniques for the construction of arbitrarily nested recursive algorithms by general Noetherian induction, as well as a systematic method for the generation of the conjectures and consequently of the algorithms for the auxiliary functions needed in the main function.


Algorithm synthesis Binary trees Multisets Theorema 


  1. 1.
    Blizard, W.D.: Multiset theory. Notre Dame J. Formal Logic 30(1), 36–66 (1989). Scholar
  2. 2.
    Buchberger, B.: Theory exploration with theorema. Analele Universitatii Din Timisoara, Seria Matematica-Informatica XXXVII(2), 9–32 (2000)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Buchberger, B.: Algorithm invention and verification by lazy thinking. Analele Universitatii din Timisoara, Seria Matematica - Informatica XLI, 41–70 (2003)MathSciNetzbMATHGoogle Scholar
  4. 4.
    Buchberger, B., Craciun, A.: Algorithm synthesis by lazy thinking: using problem schemes. In: Proceedings of SYNASC, pp. 90–106 (2004)Google Scholar
  5. 5.
    Buchberger, B., et al.: The theorema project: a progress report. In: Calculemus 2000, pp. 98–113. A.K. Peters, Natick (2000)Google Scholar
  6. 6.
    Buchberger, B., Jebelean, T., Kutsia, T., Maletzky, A., Windsteiger, W.: Theorema 2.0: computer-assisted natural-style mathematics. J. Formal. Reason. 9(1), 149–185 (2016). Scholar
  7. 7.
    Bundy, A., Dixon, L., Gow, J., Fleuriot, J.: Constructing induction rules for deductive synthesis proofs. Electron. Notes Theor. Comput. Sci. 153, 3–21 (2006). Scholar
  8. 8.
    Dramnesc, I., Jebelean, T.: Synthesis of list algorithms by mechanical proving. J. Symb. Comput. 68, 61–92 (2015). Scholar
  9. 9.
    Dramnesc, I., Jebelean, T.: Case studies on algorithm discovery from proofs: the delete function on lists and binary trees using multisets. In: SISY 2019, pp. 213–220. IEEE Xplore (2019)Google Scholar
  10. 10.
    Dramnesc, I., Jebelean, T.: Proof-based synthesis of sorting algorithms using multisets in theorema. In: FROM 2019, EPTCS 303, pp. 76–91 (2019).
  11. 11.
    Dramnesc, I., Jebelean, T., Stratulat, S.: Combinatorial techniques for proof-based synthesis of sorting algorithms. In: SYNASC 2015, pp. 137–144 (2015).
  12. 12.
    Dramnesc, I., Jebelean, T., Stratulat, S.: Theory exploration of binary trees. In: SISY 2015, pp. 139–144. IEEE (2015).
  13. 13.
    Dramnesc, I., Jebelean, T., Stratulat, S.: A case study on algorithm discovery from proofs: the insert function on binary trees. In: SACI 2016, pp. 231–236. IEEE (2016).
  14. 14.
    Drămnesc, I., Jebelean, T., Stratulat, S.: Proof–based synthesis of sorting algorithms for trees. In: Dediu, A.-H., Janoušek, J., Martín-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 562–575. Springer, Cham (2016). Scholar
  15. 15.
    Dramnesc, I., Jebelean, T., Stratulat, S.: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques. J. Symb. Comput. 90, 3–41 (2019). Scholar
  16. 16.
    Knuth, D.E.: The Art of Computer Programming, Volume 2: Seminumerical Algorithms, 3rd edn. Addison-Wesley, Boston (1998). Scholar
  17. 17.
    Korukhova, Y.: Automatic deductive synthesis of lisp programs in the system ALISA. In: Fisher, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds.) JELIA 2006. LNCS (LNAI), vol. 4160, pp. 242–252. Springer, Heidelberg (2006). Scholar
  18. 18.
    Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90–121 (1980). Scholar
  19. 19.
    Manna, Z., Waldinger, R.: The Logical Basis for Computer Programming, vol. 1: Deductive Reasoning. Addison-Wesley, Boston (1985). Scholar
  20. 20.
    Manna, Z., Waldinger, R.: Fundamentals of deductive program synthesis. IEEE Trans. Softw. Eng. 18(8), 674–704 (1992). Scholar
  21. 21.
    Radoaca, A.: Properties of multisets compared to sets. In: SYNASC 2015, pp. 187–188 (2015).
  22. 22.
    Smith, D.R.: Kids: a semiautomatic program development system. IEEE Trans. Softw. Eng. 16(9), 1024–1043 (1990). Scholar
  23. 23.
    Traugott, J.: Deductive synthesis of sorting programs. J. Symb. Comput. 7(6), 533–572 (1989). Scholar
  24. 24.
    Windsteiger, W.: Theorema 2.0: a system for mathematical theory exploration. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 49–52. Springer, Heidelberg (2014). Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.West UniversityTimişoaraRomania
  2. 2.Johannes Kepler UniversityLinzAustria

Personalised recommendations