A broader interpretation of logic in logic programming
Alan Bundy · Edinburgh Research Explorer (University of Edinburgh) · 1988
We argue that the restriction of logic programs to sets of Horn clauses, even with negation as failure, is an unacceptable inhibition to programmers' expressiveness and forces them to make premature procedural commitments.Programmers should be permitted to use the cull power of logic when specifying logic programs.In particular, we give examples of the need for functions, quantification, disjunction and predicate variables.Unfortunately, direct interpretation of programs written in such broader logics presents severe difficulties.One route to solving this problem is to treat the broader logic programs as specifications and to refine them into programs before executing them.Horn clauses might be the target programming language.Some refinement techniques can be borrowed from formal methods in software engineering.This suggests a modification of Kowaiski's famous slogan to eAl gorithm = Refined(Logic) + Control".We illustrate these ideas by describing the Nuprl system for program synthesis and the work we are doing to guide the process of synthesis by the use of proof plans.Key words and phrases.Logic programming, logic, non-Horn clauses, constructive logic, program synthesis, Nuprl, proof plans. The Vision of Logic ProgrammingIn his missionary works introducing logic programming to the world, eg [Kowalski 79b,Kowalski 79a], Kowaiski used the slogan "Algorithm = Logic + Control".The normal interpretation of this slogan is that people can describe their problems in the language of predicate logic, without regard to how this description might be used to solve their problem, and then a clever interpreter will run their logical description as an algorithm to solve their problem.This is a wonderful vision.It frees users from thinking in terms of their solution and permits them merely to describe their problem, thus making the power of computing available to the nonprogrammer.The computer is left to construe the problem description as a computer program.Unfortunately, we all know that life is not as simple as this.