zlacker

>> What would be interesting, would be to replace depth-first search while remaining in the world of predicates and Horn clauses.

For that you want tabled Prolog, or in other words Prolog executed by SLG-Resolution. The paradigmatic implementation is XSB Prolog:

https://xsb.com/xsb-prolog/

SWI-Prolog also supports tabling but I think the XSB implementation is more mature.