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
Link To Document