An Incompleteness Result for Deductive Synthesis of Logic Programs

Kung-Kiu Lau
Department of Computer Science, University of Manchester
Oxford Road, Manchester M13 9PL, United Kingdom
kung-kiu@cs.man.ac.uk

Mario Ornaghi
Dipartimento di Scienze dell'Informazione
Universita' degli studi di Milano
Via Comelico 39/41, Milano, Italy
ornaghi@dsi.unimi.it

Abstract:
We formalise the derivation of logic programs from their specifications by
deductive synthesis, and introduce the notion of uniform equivalence between
logical systems. This enables us to present an incompleteness result for
deductive synthesis of logic programs from first-order logic specifications.