Abstract
We show here that meta-variables of Prolog admit a simple declarative interpretation. This allows us to extend the usual theory of SLD-resolution to the case of logic programs with meta-variables, and to establish soundness and strong completeness of the corresponding extension of the SLD-resolution. The key idea is the use of ambivalent syntax which allows us to use the same symbols as function and relation symbols. We also study the problem of absence of run-time errors in presence of meta-variables. We prove that this problem is undecidable. However, we also provide some sufficient and polynomial-time-decidable conditions which imply absence of run-time errors.