The visualizer is close to what I want, but my users never need to see the actual Prolog code, and I do need them to understand the context of where the options considered arise.
I’m also not sure of the utility of displaying things like “p(X) doesn’t unify with q(7)”, because in fact the reasoner never considers unifying unless the functor and arity are the same, and there would be no mystery as to why.
I need to do a lot of work to prototype what I’m imagining, and there are parts of it that I’m totally unclear about, like how to allow access to a natural language version of the clauses, without crowding the interface horribly.
But the animated aspect of the Prolog Visualizer, and the way it builds the tree, is similar to what I would want.