Practical Aspects of Logical Based Algorithm Synthesis
Sprache des Vortragstitels:
3rd International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2009)
Sprache des Tagungstitel:
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.