caa a22 4500 463187032 CHVBK 20180406164857.0 cr unu---uuuuu 170326e20070801xx s 000 0 eng 10.1007/s10472-007-9079-9 doi (NATIONALLICENCE)springer-10.1007/s10472-007-9079-9 Korukhova Yulia Computational Mathematics and Cybernetics Faculty, Lomonosov Moscow State University, GSP-1, Leninskie Gory, 119991, Moscow, Russia aut An approach to automatic deductive synthesis of functional programs [Elektronische Daten] [Yulia Korukhova] The work deals with automatic deductive synthesis of functional programs. Formal specification of a program is taken as a mathematical existence theorem and while proving it, we derive a program and simultaneously prove that this program corresponds to given specification. Several problems have to be resolved for automatic synthesis: the choice of synthesis rules that allows us to derive the basic constructions of a functional program, order of rule application and choice of a particular induction rule. The method proposed here is based on the deductive tableau method. The basic method gives rules for functional program construction. To determine the proof strategy we use some external heuristics, including rippling. And for the induction hypothesis formation the combination of rippling and the deductive tableau method became very useful. The proposed techniques are implemented in the system ALISA (Automatic Lisp Synthesizer) and used for automatic synthesis of several functions in the Lisp language. Springer Science+Business Media B.V., 2007 Deductive program synthesis nationallicence Automated reasoning nationallicence Proof planning nationallicence Rippling nationallicence Induction nationallicence Annals of Mathematics and Artificial Intelligence Springer Netherlands 50/3-4(2007-08-01), 255-271 1012-2443 50:3-4<255 2007 50 10472 https://doi.org/10.1007/s10472-007-9079-9 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10472-007-9079-9 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Korukhova Yulia Computational Mathematics and Cybernetics Faculty, Lomonosov Moscow State University, GSP-1, Leninskie Gory, 119991, Moscow, Russia aut NATIONALLICENCE 773 0- Annals of Mathematics and Artificial Intelligence Springer Netherlands 50/3-4(2007-08-01), 255-271 1012-2443 50:3-4<255 2007 50 10472 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer