Department of Computer Science

Roskilde University, P.O.Box 260, DK-4000 Roskilde, Denmark

In this paper, we consider the particular problems that arise for the primitive operations in the demo predicate when used "backwards" as a tool for generating programs. The binary proof predicate demo is specified as follows.

demo(P',Q') iff P' and Q' are names of program and query, P and Q, such that there exists substitution sigma with P |- Q sigmaA metavariable, say

useful(X), demo(... X ..., ...)

The 'useful' predicate may specify syntactic requirements to the program fragments sought, perhaps extended with additional calls to demo to express integrity constraints. As demonstrated elsewhere (Christiansen, 1994a, 1994b, 1995, 1996), this principle can be used for defining quite concisely a wide range of reasoning tasks such as abduction, induction, diagnosis, default reasoning, etc. The present paper concerns the methods that are necessary in order to achieve an implementation of demo providing this functionality. We use the structure of the so-called "instance-demo" predicate which has been studied by several other authors recently (Hill, Gallagher, 1994; Bowers, Gurr, 1995). It replicates SLD-resolution using the following primitive operations,

- instance(S', T', sigma')

--- S' and T' are names of terms S and T, sigma' name of a substitution \sigma with Ssigma=T. - member(C', P')

--- C' and P' are names of clause and program C and P with C a member of P.

- Uninstantiated variables in the first argument to an instance constraint can easily lead the programs of (Hill, Gallagher, 1994; Bowers, Gurr, 1995) into floundering states, so no answer is provided. This arise in the maintenance of substitution arguments.
- A subgoal instance(X,Y,Z), for variables X, Y, Z, will initiate by backtracking a generation process of all possible names of terms in the object language until one that meets the subsequent subgoals is reached.
- The representation of programs as lists
results in infinitely many equivalent
solutions produced for essentially
the same object program by permutation and
duplication of clauses and
by insertion of arbitrary numbers of new
variables. (To see this, consider the solutions
to the Prolog call
`member(a,L), member(b,L)`). Backtracking on failure is thus condemned to loop. - Satisfiability for sets of calls to 'instance' (allowing arbitrary use of uninstantiated variables) is closely related to the undecidable semiunification problem, so establishing termination result is problematic.

Metaprogramming and Metareasoning in Logic (META96), Tech. Repr. 127, Uppsala University, Compoure Science Dept., 1996, pp. 13-25.

See dvi, postscript.