What is the computation model of Prolog? Several computation models have representative programming language counterparts, as, according to this answer, Snobol for rewriting systems, APL for combinators, Lisp/Scheme for lambda calculus, and off course the family of imperative languages for TMs (or more precisely RAMs). It seems to me that Prolog should also be a paradigmatic language for some model. Is this assumption true? If so, what is the name of that model?
I think the computation model of Prolog is the SLDNF resolution of Horn clauses.

Prolog is actually very procedural. Kowalski 1974: "The interpretation of predicate logic as a programming language is based upon the interpretation of implications [...] as procedure declarations [...]" (emphasis mine)

https://www.doc.ic.ac.uk/~rak/papers/IFIP%2074.pdf

(However, lambda calculus, theorem provers, and Turing machines are term rewriting systems indeed. What is a computational model then, if everything is a term rewriting system?)