Question

Let $\sigma$ denote an independent simultaneous substitution. Now I wonder if the following holds:

If $\Gamma \vartriangleright (A\ (\sigma\ \tau))\ \rho$ then there are $\psi$, $\phi$ such that $\Gamma \vartriangleright (A\ \sigma)\ \psi$ and $\psi\ \phi = \tau\ \rho$.

Is this true in Prolog?

Best Regards

Answer 1

OK, so $\Gamma$ is a set of universal Horn sentences, and $A\sigma$ is a conjunction of atomic formulas. In theory, Prolog is supposed to find substitutions $\rho$ which make the query provable from $\Gamma$, and moreover, such that any other such substitution is less general than one of those which are output. (Essentially, for each admissible propositional skeleton of a resolution proof, it outputs the most general unifier that makes it a proof.)

In this model, the property holds: since $(A\sigma\tau)\rho=(A\sigma)(\tau\rho)$ is entailed by $\Gamma$, $\tau\rho$ must factor through one of the substitutions, call it $\psi$, output for $A\sigma$.

However, this model does not describe actual Prolog, which is neither sound nor complete from the logical point of view. It is not sound, because due to the lack of “occurs check”, most implementations will happily unify terms that are not unifiable, thereby proving formulas that are not provable. I will ignore this problem, as any Prolog program whose result depends on the presence or absence of occurs check is invalid (not conforming to the language standard). Prolog is also incomplete, as it uses a deterministic proof search strategy which may get lost in a cycle before having a chance of finding a valid proof, or the substitution we are looking for. This makes the “de-lifting” property fail.

Here’s an example (using the notation from the comments): $\sigma=[\ ]$, $A=p(X)$, $\tau=[X=a]$, $\rho=[\ ]$

?- listing(p).


p(f(A)) :-
        p(f(A)).
p(a).

Yes
?- X=a, p(X).

X = a

Yes
?- p(X).

(The second query enters an infinite loop.) Here is another example, where the query is answered, but the needed substitution is never output:

?- listing(p).


p(b).
p(f(A)) :-
        p(A).
p(a).

Yes
?- X=a, p(X).

X = a

Yes
?- p(X).

X = b ;

X = f(b) ;

X = f(f(b)) ;

X = f(f(f(b))) ;

X = f(f(f(f(b)))) ;

X = f(f(f(f(f(b))))) ;

...