alt Hacker News> 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.
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.