Practical Aspects of Logical Based Algorithm Synthesis

Description

We approach the problem of algorithm synthesis as logical proving the correctness property of the respective function. By choosing appropriate induction principles for the input domain and sometimes by making additional choices for the algorithm schema and for the proof structure, on can often find the algorithm details automatically, as witness terms during the proof. We demonstrate this approach on several case studies using the frame of the Theorema system (www.theorema.org), and we compare our practical approach with some of the existing approaches in logical based algorithm synthesis.

Period	17 Dec 2009
Event title	3rd International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2009)
Event type	Conference
Location	JapanShow on map