I do like Prolog though.
BNF provided a formal grammar allowing the declaration of precise and iterative constructs without additional complexity of algorithmic content. Original spec @ https://www.softwarepreservation.org/projects/ALGOL/paper/Ba...
BNF was created by Naur, the guy who invented FORTRAN, and was critical to both many early RFCs (the most important standards that facilitated the growth of the internet) and man pages in Unix. The syntax:
executable <required-arg> [optional-arg]
Now, Greibach normal form is useful, but its use is to avoid left-recursions. That's not to say it improves performance: Prolog's SLDNF-Resolution just can't handle left-recursion and it will often "go infinite" with it (although many staple Prolog programs like member/2, append/3, reverse/2 etc. are left-recursive).
DCGs are not the pinnacle of performance, sure, but that's not because of left-recursion. It's because a Definite Clause Grammar evaluated by SLDNF-Resolution is a left-right descent parser, and those are just not very efficient. I think it's O(n^3) to parse a CFG with an LR descent parser? So if you want better performance out of a DCG, parse it with a chart parser.
I would argue that this can attract users better than the additional formalism you can obtain through logic programming, because once you have determined the validity and class (roughly "set membership") of something, you can potentially generalize about it more easily and you have a clear cognitive boundary.
Speaking from experience, in practice, I often rigidly define one layer of a system and then implement algorithms less rigidly using a less formal approach. This seems standard across the industry. Think about UUIDs, network addresses, etc.
I believe this type of tradeoff is ultimately what killed logic programming. If you really want to do maths, do maths. If you want to define something, do so succinctly. And if you are here to implement an algorithm, use the right tool. Don't pretend the code will write itself. Logic programming always seemed to me a sort of allusion to mathematical inference that didn't transfer well to real world programming problems.
Just my opinion.
There is an algebraic similarity between Horn clauses, BNF grammar clauses (if you consider concatenation and choice to be operators) and sum types. After working in logic programming, functional programming and imperative styles I would agree that the rigid definition part makes it easier to write the code that will sit on top, even if that code is far less rigid.