Let's say we work on the "reverse list" function. A few tests I could write are that the following clauses are true:

    rev([1], [1])
    rev([1, 2, 3], [3, 2, 1])

And maybe also that the following clauses are false:

    rev([1, 2], [1, 2])
    rev([], [1])
    rev([1, 1], [1])

Is Prolog able to infer, from the above, that rev([4, 5], [5, 4]) ? Or to synthesize the general form rev([H|T],R) :- rev(T, RT), concat(RT,[H],R) ?

Sounds like NN training that could be achievable. The problem comes with unit testing, because the minimal testable unit could be more complex than a function.

Yeah. I've often seen TDD where you act both as the logic programmer writing the tests and the imperative programmer writing the implementation.

No. Not even a little bit.

Could... could you enlighten me please?