> This gets to the heart of my problem with Prolog: it's sold as if it's logic programming - just write your first-order predicate logic and we'll solve it. But then to actually use it you have to understand how it's executed
Prolog is a logic-flavored programming language. I don't recall Prolog ever being "sold" as pure logic. More likely, an uninformed person simply assumed that Prolog used pure logic.
Complaining that Prolog logic doesn't match mathematical logic is like complaining that C++ objects don't accurately model real-life objects.
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.
> 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.
Prolog is a logic-flavored programming language. I don't recall Prolog ever being "sold" as pure logic. More likely, an uninformed person simply assumed that Prolog used pure logic.
Complaining that Prolog logic doesn't match mathematical logic is like complaining that C++ objects don't accurately model real-life objects.