[YeGoblynQueenne]

>> "forall X: P"

That is not a First Order Logic statement. I think perhaps you mean "forall X, P(X)" or "∀x: P(x)". This can be expressed in Prolog as "p(X)", where X is an implicitly universally quantified variable.

Do you mean something else? For example, is P meant to be a second-order variable? In that case you can always reprsent it as m(P) in Prolog. Or as m('$P') or some other syntax chosen to denote an existentially quantified second-order term.

In general, could you please clarify what you mean by "true logic engine" and "true logic language"? I'm afraid I'm not familiar with the terms.

>> Prolog isn't based on first-order logic or anything.

Yes, Prolog isn't "based" on FOL. It's an automated theorem-prover for FOL theories that uses SLDNF resolution as an inference rule. You could say it's "based on SLDNF resolution" I guess.

[colanderman]

> That is not a First Order Logic statement. I think perhaps you mean "forall X, P(X)" or "∀x: P(x)".

You seem to have had no trouble understanding what I wrote. What's the point of this comment?