Since Hornclauses are a fragment of FOL, it also holds for pure Prolog.

Shouldn’t this be the opposite?

Horn clauses are a fragment, so they are pretty certain to not derive everything that is true in a Model (to speak not even about a conclusion being unreachable for practical reasons). Just let them be “don’t know” (or “pseudo-false” under Negation-as-Failure, what I like to call “no evidence for”)

(Completeness is overrated anyway. Who wants to derive everything that is considered true? What is important is soundness: Do not label statements as true using a proof mechanism when they are aren’t true in the model. That would be bad!)

Here is a good reference:

https://plato.stanford.edu/entries/reasoning-automated/

Soundness and completeness are two (metatheoretical) properties of a calculus that are particularly important for automated deduction. **Soundness** states that the rules of the calculus are truth-preserving. For a direct calculus this means that if Γ ⊢ α then Γ ⊨ α. For indirect calculi, soundness means that if Γ∪{~α} ⊢ ⊥ then Γ ⊨ α. **Completeness** in a direct calculus states that if Γ ⊨ α then Γ ⊢ α. For indirect calculi, the completeness property is expressed in terms of **refutations** since one establishes that Γ ⊨ α by showing the existence of a proof, not of α from Γ, but of ⊥ from Γ∪{~α}. Thus, an indirect calculus is **refutation complete** if Γ ⊨ α implies Γ∪{~α} ⊢ ⊥. Of the two properties, soundness is the most desirable. An incomplete calculus indicates that there are entailment relations that cannot be established within the calculus. For an automated reasoning program this means, informally, that there are true statements that the program cannot prove. Incompleteness may be an unfortunate affair but lack of soundness is a truly problematic situation since an unsound reasoning program would be able to generate false conclusions from perfectly true information.

And a bit further:

Last but not least, in order to improve their efficiency, many implementations of Prolog do not implement unification fully and bypass a time-consuming yet critical test—the so-called **occurs-check** —responsible for checking the suitability of the unifiers being computed. This results in an unsound calculus and may cause a goal to be entailed by a Prolog program (from a computational point of view) when in fact it should not (from a logical point of view).

There are variations of Prolog intended to extend its scope. By implementing a model elimination procedure, the Prolog Technology Theorem Prover (PTTP) (Stickel 1992) extends Prolog into full first-order logic. The implementation achieves both soundness and completeness. Moving beyond first-order logic, λProlog (Miller & Nadathur 1988) bases the language on higher-order constructive logic.