nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

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

verfasst von : Isabela Drămnesc, Tudor Jebelean

Erschienen in: Mathematical Aspects of Computer and Information Sciences

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel On the Chordality of Simple Decomposition in Top-Down Style

Nächstes Kapitel Algebraic Analysis of Bifurcations and Chaos for Discrete Dynamical Systems

For binary functions one may use simultaneous induction on both arguments.

The construction of the object desired for the synthesis uses only the objects which are already present in the proof, and does not try to decompose some of them.

We use LHS for left hand side and RHS for right hand side.

https://isabelle.in.tum.de/library/HOL/HOL-Library/Sorting_Algorithms.html.

Note that this introduces exceptions to antisymmetry and transitivity when the empty composite object is involved.

This means that the input condition is the logical constant True and the implication from the synthesis conjecture reduces to O[X, Y, Z].

Blizard, W.D.: Multiset theory. Notre Dame J. Formal Logic 30(1), 36–66 (1989). https://doi.org/10.1305/ndjfl/1093634995MathSciNetCrossRefMATH

Buchberger, B.: Theory exploration with theorema. Analele Universitatii Din Timisoara, Seria Matematica-Informatica XXXVII(2), 9–32 (2000)MathSciNetMATH

Buchberger, B.: Algorithm invention and verification by lazy thinking. Analele Universitatii din Timisoara, Seria Matematica - Informatica XLI, 41–70 (2003)MathSciNetMATH

Buchberger, B., Craciun, A.: Algorithm synthesis by lazy thinking: using problem schemes. In: Proceedings of SYNASC, pp. 90–106 (2004)

Buchberger, B., et al.: The theorema project: a progress report. In: Calculemus 2000, pp. 98–113. A.K. Peters, Natick (2000)

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). https://doi.org/10.6092/issn.1972-5787/4568MathSciNetCrossRefMATH

Bundy, A., Dixon, L., Gow, J., Fleuriot, J.: Constructing induction rules for deductive synthesis proofs. Electron. Notes Theor. Comput. Sci. 153, 3–21 (2006). https://doi.org/10.1016/j.entcs.2005.08.003CrossRef

Dramnesc, I., Jebelean, T.: Synthesis of list algorithms by mechanical proving. J. Symb. Comput. 68, 61–92 (2015). https://doi.org/10.1016/j.jsc.2014.09.030MathSciNetCrossRefMATH

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)

10.

Dramnesc, I., Jebelean, T.: Proof-based synthesis of sorting algorithms using multisets in theorema. In: FROM 2019, EPTCS 303, pp. 76–91 (2019). https://doi.org/10.4204/EPTCS.303.6

11.

Dramnesc, I., Jebelean, T., Stratulat, S.: Combinatorial techniques for proof-based synthesis of sorting algorithms. In: SYNASC 2015, pp. 137–144 (2015). https://doi.org/10.1109/SYNASC.2015.30

12.

Dramnesc, I., Jebelean, T., Stratulat, S.: Theory exploration of binary trees. In: SISY 2015, pp. 139–144. IEEE (2015). https://doi.org/10.1109/SISY.2015.7325367

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). https://doi.org/10.1109/SACI.2016.7507376

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). https://doi.org/10.1007/978-3-319-30000-9_43CrossRef

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). https://doi.org/10.1016/j.jsc.2018.04.002MathSciNetCrossRefMATH

16.

Knuth, D.E.: The Art of Computer Programming, Volume 2: Seminumerical Algorithms, 3rd edn. Addison-Wesley, Boston (1998). https://doi.org/10.1137/1012065CrossRefMATH

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). https://doi.org/10.1007/11853886_21CrossRefMATH

18.

Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90–121 (1980). https://doi.org/10.1145/357084.357090CrossRefMATH

19.

Manna, Z., Waldinger, R.: The Logical Basis for Computer Programming, vol. 1: Deductive Reasoning. Addison-Wesley, Boston (1985). https://doi.org/10.2307/2275898CrossRefMATH

20.

Manna, Z., Waldinger, R.: Fundamentals of deductive program synthesis. IEEE Trans. Softw. Eng. 18(8), 674–704 (1992). https://doi.org/10.1109/32.153379CrossRef

21.

Radoaca, A.: Properties of multisets compared to sets. In: SYNASC 2015, pp. 187–188 (2015). https://doi.org/10.1109/SYNASC.2015.37

22.

Smith, D.R.: Kids: a semiautomatic program development system. IEEE Trans. Softw. Eng. 16(9), 1024–1043 (1990). https://doi.org/10.1109/32.578788CrossRef

23.

Traugott, J.: Deductive synthesis of sorting programs. J. Symb. Comput. 7(6), 533–572 (1989). https://doi.org/10.1016/S0747-7171(89)80040-9CrossRefMATH

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). https://doi.org/10.1007/978-3-662-44199-2_9CrossRefMATH

Titel: Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema
verfasst von: Isabela Drămnesc
Tudor Jebelean
Verlag: Springer International Publishing
Buch: Mathematical Aspects of Computer and Information Sciences
Print ISBN: 978-3-030-43119-8

Electronic ISBN: 978-3-030-43120-4

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-43120-4_13

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"