[AlotOfReading]

    I don't recall Prolog ever being "sold" as pure logic.

One of the guides linked above describes it as:

    The core of Prolog is restricted to a Turing complete subset of first-order predicate logic called Horn clauses

[hackyhacky]

> The core of Prolog is restricted to a Turing complete subset of first-order predicate logic called Horn clauses

Does this sound to you like an attempt to deceive the reader into believing, as the GP comment stated, that the user can

> just write your first-order predicate logic and we'll solve it.

[AlotOfReading]

It absolutely does sound like "write your first order logic in this subset and we'll solve it". There's no reasonable expectation that it's going to do the impossible like solve decideability for first order logic.

[hackyhacky]

> It absolutely does sound like "write your first order logic in this subset and we'll solve it".

No it does not. Please read the words that you are citing, not the words that you imagine. I honestly can't tell if you are unable to parse that sentence or if you a cynically lying about your interpretation in order to "win" an internet argument.

All programming languages are restricted, at least, to a "Turing complete subset of first-order predicate logic." There is absolutely no implication or suggestion of automatically solving any, much less most, first order logic queries.

[davidgay]

Except it cannot decide all Horn clauses.