[weinzierl]

Which is strange considering how old and limited Prolog in a sense is. I wonder why no superset ever gained traction and what it would look like. I imagine it fitting somewhere in the hierarchy

Theorem Prover ⊃ SMT Solver ⊃ SAT Solver

since

Theorem Prover ⊃ Prolog

[Epa095]

The post in OP has the following hyphothesis:

> Why Prolog? [...] Due to it's declarative nature it might be a bit easier for LLMs to generate code, because LLM doesn't need to generate precise control flow.

This is an interesting point, and my guess is that prolog is the declarative programming language with most example code out there for it to learn on(excluding SQL). Alternatively it could try to create some problem description for an automated theorem prover. My (absolute ignorant) guess is that the prolog aproach works better for two reasons:

- The amount of prolog code in the training set is higher

- It is still only able to create code for problems easy enough that prolog can handle them.

[Byamarro]

Learning curve perhaps? There doesn't have to be an overlap between people working on this and the tools you have mentioned

[knome]

limited in what sense?

prolog is turing complete.

[Epa095]

He might be thinking about the SLDNF resolution happening. But yes, you can implement any prover in prolog. This distinction is discussed a bit here: https://www.metalevel.at/prolog/theoremproving

[sixfiveotwo]

Indeed, you can get a lot more from dependent types than Damas-Hindley-Milner inference, yet does it mean that you should use the former everywhere?

[dsabanin]

Another attractive feature of Prolog is that it’s homoiconic, like lisp.