Most systems of (first-order) logic differentiate between function letters (aka, symbols) and predicate letters (symbols). The former are used to build terms; the latter build atomic formulas (which can later be combined in more complex formulas using negation, conjunction, disjunction, and quantification): http://plato.stanford.edu/entries/logic-classical/ Formulas like Even (succ zero) can be interpreted to be `true' or `false' (alternatively: succeed or fail). In the atomic formula above, Even is a predicate symbol. OTH, terms like `succ zero' (an application of a function symbol succ to a constant zero) is not interpreted as true or false: it just is. In Prolog, there is likewise distinction between terms (which can be compared and unified, but cannot 'fail') and goals. The following gives a good introduction in the typed setting: http://www.cs.mu.oz.au/research/mercury/information/doc-release/reference_ma... Incidentally, many Prolog systems also permit declarations of goals and of terms (because it helps produce better code). Lambda-Prolog, like Mercury, insists on declarations. The distinction between terms and goals is a bit blurred in Prolog, due to its reflection facilities: one can add a new term as a rule or a fact (e.g., using assert), one can examine the rules or facts, etc. In Haskell type-level programming: type -> term type constructor -> function symbol class name -> predicate symbol class constraint -> atomic formula (atomic goal) There is a subset of Prolog called Datalog, which is commonly defined as Prolog without function symbols. Logic without function symbols is equivalent to logic with function symbols, _provided_ we have the infinite supply of constants. For example, Foo(f(x),g(x)) can be represented as exists y y'. F(x,y) & G(x,y') & Foo(y,y') So, each function symbol f of arity n is represented as a predicate F of arity n+1. That predicate is a functional predicate: for each combination of the first n arguments, there exists exactly one object (for the last argument) that makes the predicate hold. Since terms in logic are finite, the infinitely countable supply of constants is enough. In Datalog however, the extensional database is finite. There is a finite number of facts and hence the finite number of constants. That breaks the above correspondence, and so terms like f(f(f(... x))) can no longer be emulated as the corresponding F predicate is finite (its domain is finite). That's why in pure Datalog (without negation or with stratified negation), termination is assured. This is not the case in pure Prolog because of the possibility to construct longer and longer terms like succ(succ(x)). Regarding termination, minimal models, and the correspondence between logic formulas (and pure, positive, stratified, etc. Datalogs) and P-complete etc. programs, please see http://www.csupomona.edu/~jrfisher/www/logic_topics/positive/positive.html