A broader interpretation of logic in logic programming

摘要: We argue that the restriction of logic programs to sets Horn clauses, even with negation as failure, is an unacceptable inhibition programmers' expressiveness and forces them make premature procedural commitments. Programmers should be permitted use cull power when specifying programs. In particular, we give examples need for functions, quantification, disjunction predicate variables. Unfortunately, direct interpretation written in such broader logics presents severe difficulties. One route solving this problem treat specifications refine into before executing them. clauses might target programming language. Some refinement techniques can borrowed from formal methods software engineering. This suggests a modification Kowaiski's famous slogan eAl gorithm = Refined(Logic) + Control". illustrate these ideas by describing Nuprl system program synthesis work are doing guide process proof plans.