Lecture 8: Completion

This code implements a backtracking interpreter with success and
failure continuations and explicit calls to unification.

The propositions and terms are "reified" instead of using the
underlying Prolog representation.  This is not an example of good
Prolog programming style, and there are many unnecessary
inefficiencies in order to make the implementation close to the
mathematical specification from the lectures notes.

We have

Clauses D ::= app(P,ts) | and(D1,D2) | top | implies(G,D) | forall(bd(N),D)
Goals   G ::= app(P,ts) | and(G1,G2) | top | or(G1,G2) | bot | equal(s,t)
               | exists(bd(N),G)
Terms       t ::= app(F,ts) | var(X)
Term Lists ts ::= [t1,...,ts]

Variables   X ::= bd(N)   % bound variables
                | N       % logic variables
                | arg(N)  % argument variables

Numbers     N ::= 1 | 2 | ...

reify.pl    -- Converting Prolog programs to reified form
unif.pl     -- Unification (with occurs-check)
meta.pl     -- Meta-interpreter
examples.pl -- Sample programs and top-level code

Load as

?- [reify,unif,meta,examples].
?- test2([perm/2,insert/3], perm([1,2,3], _), J).

should have 6 solutions (succeed 7 times, last time
indicates explicit failure).