You're right that it's hard. However, I think you're missing one significant point that, at least to some extent, justifies the hardness: computability. System

You're right that it's hard. However, I think you're missing one significant point that, at least to some extent, justifies the hardness: computability. Systems like Prolog are based on the idea of "proof search": given a logical statement, find a proof of that statement. Humans do this all the time with classical logic, you might say -- but then, there are very famous statements expressible purely in first-order logic that nobody has found a proof of. This is anathema to computing! We want an "effective method", a "decision procedure", that allows us to compute for finite time and terminate with a positive (or negative!) proof. And we know, thanks to Gödel, that no such procedure exists for first-order logic: any decision procedure will miss proofs for some first-order statements. In order to give ourselves more options for proof search, we need to enrich our logics somehow. This enrichment usually comes in the form of restrictions relative to classical logic. For example, Horn clauses are a fragment of classical logic that we _can_ assign a reasonable decision procedure to -- of which the most basic is probably SLD resolution. But these restrictions traditionally sacrifice more power than we'd like, so we add various things back in, trading computational difficulty (but not decidability!) for expressivity. This is a significant source of complexity, no doubt! Computational logic is hard because we're asking more of it. Classical logic has been around since at least Aristotle, so it's perhaps no surprise that it's been refined into such a simple, well-understood form. Even then, I think if you traveled into various classical modal logics, you'd find those just as inscrutable at first as the logics we use in logic programming. > Hoare logic Mmh... For the most part, Hoare logic is back on the "for humans" side of things, as it's about verifying software rather than implementing software. It brings to bear the full power of classical logic(1), but since you're applying it to programs, most of which have incredibly non-monotonic semantics, you have to consider truth at each point in the program. Most of the machinery in Hoare logic over classical logic is about relating all of those points -- all of those worlds, in a model-theoretic sense. I personally find Hoare logic easier from a mathematical reasoning perspective than any of the logic systems designed for implementation. I think that makes sense, though, because Hoare logic is not about automation. (1) You can instantiate Hoare logic over any particular logical system, so you could apply it for automated verification, but I don't think that's the case the parent was considering.