|
Vol: 57(71) No: 4 / December 2012 Systematic Exploration of List Theory in Theorema Isabela Dramnesc Department of Computer Science, West University, Faculty of Mathematics and Informatics, Bd.V.Parvan 4, 300223 Timişoara, Romania, phone: (+40) 256-592195, e-mail: idramnesc@info.uvt.ro, web: http://www.info.uvt.ro/~idramnesc Tudor Jebelean Research Institute for Symbolic Computation, Johannes Kepler University, Altenberger Straße 69, A-4040 Linz, Austria, phone: (+43) 732-24689946, e-mail: Tudor.Jebelean@jku.at, web: http://www.risc.jku.at/home/tjebelea Keywords: lists, exploration, theory, Theorema Abstract We construct in a systematic way a collection of properties of lists which are used for synthesizing automatically several sorting algorithms. This is a novel case study in theory exploration which can also be used for teaching, in particular because it is completely supported by the Theorema system. The theory exploration process was carried out in parallel with the synthesis of some sorting algorithms in Theorema. Certain appropriate induction principles for lists are used in order to prove the properties which are stated and the conjectures corresponding to the synthesis problems. We use first order predicate logic (which is semi-decidable), in contrast with an older approach in the Theorema system which uses higher-order logic and sequence variables. This work demonstrates the effective and efficient automation of proving in the domain of lists, which is useful for the exploration of theories and for the synthesis of algorithms and may be generalized to other domains. References [1] B. Buchberger, “Theory Exploration with Theorema”, in Analele Universitatii de Vest din Timisoara, Ser. Matematica–Informatica, vol. XXXVIII, pp. 9 – 32, 2000. [2] B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa, 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. [3] B. Buchberger, “Algorithm Supported Mathematical Theory Exploration: A Personal View and Strategy”, in Proceedings of the 7th International Conference on Artificial Intelligence and Symbolic Computation AISC 2004, Linz, Austria, pp. 236 – 250, 2004. [4] I. Dramnesc and T. Jebelean, “Proof Techniques for Synthesis of Sorting Algorithms”, in Proceedings of the 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing SYNASC 2011, Timisoara, Romania, pp. 101 – 109, IEEE Computer Society, September 2011. [5] I. Dramnesc and T. Jebelean, Semi–automatic Synthesis of Some Sorting Programs in Theorema, Technical Report 12–01, RISC Report Series, University of Linz, Austria, 2012. [6] I. Dramnesc and T. Jebelean, Systematic Exploration of the Theory of Lists in Theorema, Technical Report 12–02, RISC Report Series, University of Linz, Austria, 2012. [7] M. Hodorog and A. Craciun, “Scheme–Based Systematic Exploration of Natural Numbers”, in Proceedings of the 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing SYNASC 2006, Timisoara, Romania, pp. 23 – 34, IEEE Computer Society, September 2006. [8] Z. Manna and R. Waldinger, The Logical Basis for Computer Programming, Volume 1: Deductive Reasoning, Addison Wesley, 1985. [9] S. Wolfram, The Mathematica Book, Wolfram Media Inc., 2003. |