• DocumentCode
    3689568
  • Title

    Theory exploration of binary trees

  • Author

    Isabela Drâmnesc;Tudor Jebelean;Sorin Stratulat

  • Author_Institution
    Department of Computer Science, West University, Timiş
  • fYear
    2015
  • Firstpage
    139
  • Lastpage
    144
  • Abstract
    The construction of a theory for binary trees is presented, based on the systematic exploration of the properties necessary for the proof-based synthesis and certification of sorting algorithms for binary trees. The process is computer supported, being realised in the frame of the Theorema system, with some additional proofs in Coq required for algorithm certification. The result of the exploration consists in 11 definitions, 3 axioms, and more than 200 properties. Also, more than 5 algorithms for sorting binary trees are generated.
  • Keywords
    "Binary trees","Sorting","Yttrium","Knowledge based systems","Cognition","Context","Intelligent systems"
  • Publisher
    ieee
  • Conference_Titel
    Intelligent Systems and Informatics (SISY), 2015 IEEE 13th International Symposium on
  • Type

    conf

  • DOI
    10.1109/SISY.2015.7325367
  • Filename
    7325367