Efficient and complete demo predicates for definite clause languages

Henning Christiansen
Department of Computer Science
Roskilde University, P.O.Box 260, DK-4000 Roskilde, Denmark

By means of constraint logic programming, we obtain an implementation of the binary demo predicate which is logically complete. The specification of the predicate is that a call

demo( prog-repr, query-repr)

is true whenever its arguments represent (ground names of) a program and query, respectively, such that the query is provable from the program.

Completeness implies that the predicate is equally well suited for executing programs as well as for generating them. A variable in the first argument represents, thus, an unknown program fragment and, if possible, the complete demo predicate produces an answer for it which makes the query provable.

A formal derivation system as well as an implemented system is presented. Examples indicate that demo combined with other meta-level conditions may serve as a general problem solving tool for abduction, induction and other kinds of knowledge discovery or program synthesis tasks.

Keywords: demo predicate, meta-programming, meta-interpreter, program synthesis, completeness, constraints, reflection.

Datalogiske skrifter 51, Roskilde University, 1994.
See pdf.