Some of your points are taken seriously! Think of purifying Prolog such that cuts and the like are (for many cases) no longer needed, yet you get comparable eff

Some of your points are taken seriously! Think of purifying Prolog such that cuts and the like are (for many cases) no longer needed, yet you get comparable efficiency. See library(reif), library(pio), ... Think about implication in propositional logic. Take two entirely unrelated propositions a and b. According to this logic either a → b or b → a is true. This, btw, cannot happen in Prolog.