> I'm pretty sure quantification exists implicitly, but I'm too rusty.

Indeed, as in most informal logic, all free variables are implicitly universally quantified. I think the thing that makes it seem like it's not so is that people see a clause like:

    p(X) :- q(X).

and think "oh, that X isn't really universally quantified, because p(X) isn't always true", but it really is universally quantified; what we're saying is:

    ∀X, p(X) ← q(X).

i.e., for all X values, in order to prove p(X), it suffices to prove q(X). See, for example, https://en.wikipedia.org/wiki/Horn_clause#Definition , which says

> In the non-propositional case, all variables[note 2] in a clause are implicitly universally quantified with the scope being the entire clause.

Prolog's resolution exactly follows this proof strategy; see, for example, https://en.wikipedia.org/wiki/SLD_resolution .