Synthesising Logic Programs
This is work I carried out in the summer of 1998 with
Geraint Wiggins of the Edinburgh A.I. Department as part of my MSC.
This paper is concerned with the synthesize of logic programs from
first order logic specifications. That is taking a specification,
regarding it as a proposition, and attempting to prove it with proof
rules that build up a program, hence making a program and a proof of
it's correctness in a single go. Martin Lof introduced the idea of
proofs as programs in his original work on type theory. He show how to
synthesize function programs from there proofs. Wiggins in carried out
an adaptation of Martin Lof's ideas to logic programs, in the form of
horn clauses. Wiggins develops a logic based on Gentzen's sequent
calculus, which for reason that will remain obscure, is called
Whelk. This logic lacks a complete set of elimination rules and
therefore it is limited in power and scope. In this paper we add these
rules but this presents new and interesting problems which we will
address below.
Tom Chothia
Last modified: Wed Mar 10 16:50:19 GMT 1999