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?

  • 2
    $\begingroup$ Logic programming. $\endgroup$ Commented Apr 8, 2018 at 18:57
  • 1
    $\begingroup$ I mean something like "lambda calculus" for which there is a formal proof showing it's equivalent to a TM. $\endgroup$ Commented Apr 8, 2018 at 19:04
  • $\begingroup$ I would say inference systems (a. k. a. formal systems, deduction systems, proof systems (a special case)). $\endgroup$
    – beroal
    Commented Apr 13, 2018 at 18:49

1 Answer 1


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)


(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?)


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.