|
Vol: 60(74) No: 2 / June 2015 Proof Based Synthesis of Algorithms: A Case Study on Monotone Lists Isabela Dramnesc Department of Computer Science, West University, Faculty of Mathematics and Informatics, Timisoara, Romania, e-mail: idramnesc@info.uvt.ro, web: http://web.info.uvt.ro/~idramnesc Tudor Jebelean Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria, e-mail: Tudor.Jebelean@jku.at Keywords: automated, reasoning, algorithm, synthesis, theory Abstract The synthesis method introduced in our previous work is applied in order to synthesize from proofs certain algorithms operating on “monotone list” (sorted lists without duplications). The corresponding prover and algorithm extractor are implemented in the Theorema system. Three algorithms are automatically discovered from proofs: symmetrical difference (discovered from two different proofs), the Cartesian product and the cardinality. The larger context of this work is the manipulation of sets represented as monotone lists.We start from the set theory and we demonstrate how to automatically generate the necessary functions. The properties of sets and of monotone lists which are necessary for the proofs are collected systematically in a knowledge base which extends the one presented in our previous work. This process of theory exploration is supported by a special prover which is able to prove automatically all the statements which are logical consequences of the axioms. References [1] I. Dramnesc and T. Jebelean, “A Case Study in Proof Based Synthesis of Algorithms on Monotone Lists”, in Proceedings of SACI 2015: 10th Jubilee IEEE International Symposium on Applied Computational Intelligence and Informatics, pp. 483-488, 2015. [2] I. Dramnesc and T. Jebelean, “Automated Synthesis of Some Algorithms on Finite Sets”, in Proceedings of SYNASC 2012: The 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 143–151, IEEE Computer Society, 2012. [3] I. Dramnesc and T. Jebelean, “Theory Exploration of Sets Represented as Monotone Lists”,in Proceedings of SISY 2014: IEEE 12th International Symposium on Intelligent Systems and Informatics, pp. 163-168, IEEE Xplore, 2014. [4] B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakawa, F. Piroi, N. Popov, J. Robu, M. Rosenkranz, and W. Windsteiger, “Theorema: Towards Computer-Aided Mathematical Theory Exploration” Journal of Applied Logic, 4(4):470-504, 2006. [5] S. Wolfram, The Mathematica Book. Wolfram Media Inc., 2003. [6] B. Buchberger, “Theory Exploration with Theorema”, in Analele Universitatii din Timisoara, Ser. Matematica-Informatica, vol. XXXVIII, pp.9-32, 2000. [7] W. Windsteiger, “A Set Theory Prover in Theorema,” in Computer Aided Systems Theory, nb 2178 in LNCS, pp. 525-539, Springer, 2001. |